Research interests

My current research focuses on the following topics:

  • Artificial Intelligence Techniques for the Diagnosis of Complex Systems.
    (j.w.w. Anahì Balbi)
    I am interested in applying automated reasoning techniques, including inductive ones such as learning and data mining, to the problem of identifying the primary causes of failures in complex systems. Currently, I am investigating the possibility of extracting diagnostic rules (e.g., as decision trees, or as relational predicates) using a history of diagnostic messages and a record of the components that needed replacement. This research is partially supported by a grant from Bombardier Transportation Italy, which is also providing us with the case study of railway vehicles fault diagnosis.
  • Empirical Evaluation of Automated Reasoning Systems.
    (j.w.w. Massimo Narizzano and Luca Pulina)
    I am co-organizing QBFEVAL 2006, the first competitive evaluation of QBF solvers. More in general, I am interested in the problem of assessing the perfomances of automated resoning systems using sound empirical techniques, with an emphasis on controlled experiment generation and statistical correctness of the experiments including design, confidence and reproducibility issues. To learn more about this activity in the context of QBF reasoning please visit the QBF evaluation web pages. Strictly related to the problem of evaluation is the problem of building a collection of benchmarks and a reference library for developers of QBF solvers. The site www.qbflib.org is the result of a joint effort with E. Giunchiglia and M. Narizzano, and has the purpose of collecting references for the QBF community at large. Currently, QBFLIB contains more than 5000 benchmarks in a standard format, several links to on-line literature and a comprehensive list of QBF tools and developers.
  • Sustainable Verification and Validation Techniques
    (j.w.w. Marco De Luca and Cristiano Ghersi)
    I am interested in automated techniques based on formal and structured methods that can be applied in the context of industry-scale software engineeering projects. In most cases, there is a fundamental tension between (i) the accuracy of the software models, on which, e.g., the generation of testing vectors is based, and (ii) the feasibility of structured and/or formal approaches to software design, particularly in the case of legacy/IP components. This tension usually boils down to the need of generating a (possibly large) number of test vectors manually, or leaving untested the parts of code that could not be modelled thoroughly. This research is partially supported by the consulting firm Medservice.com, which is also providing us with the case study of automating the generation of testing sequences for control software to be deployed in safety-critical systems.

Other interests include/have included:

  • Innovative Approaches to Solve Hard Combinatorial Problems. You can download a set of slides (in pdf) that describe what I believe as a viable approach to solve hard combinatorial problems in a robust and efficient way. The slides contain a general introduction to the P vs. NP issue and then delve into the details of a case study about propositional satisfiability (SAT), the prototypical NP-complete problem.
  • Oracle-driven Design of Automated Reasoning Tools (joint work with E. Giunchiglia and M. Maratea). Download a technical report where we show that complex look-ahead techniques do not pay off in state-of-the-art SAT solvers with the aid of a proof-of-concept implementation and a technique that simulates the execution of ideal versions of the SAT solver.

Traditionally, my research has focused on the development of effective software tools for automated reasoning (see the STAR pages). As such I have been co-developer of several systems (listed in reverse chronological order):

  • QuBE (webpage | reference paper | BibEntry), the new and improved version of QuBE developed in C++. I have been working for some time now on upgrades to the original QuBE 1.x architecture (see below) together with E.Giunchiglia and M. Narizzano.
  • SIMO (webpage | reference paper | BibEntry), a C++ sibling of SIM, featuring efficient data structures, state-of-the-art heuristics and optimizations (joint work with E. Giunchiglia and M. Maratea). The system is currently maintained by M. Maratea.
  • QuBE 1.x (webpage | reference paper | BibEntry), (Quantified Boolean formulas Evaluator), an effective implementation of a decision procedure for Quantified Boolean Formulas (QBFs) (joint work with E. Giunchiglia and M. Narizzano). For problems with QuBE send an e-mail to the current maintainer.
  • C-Plan (webpage | reference paper | BibEntry), a planning architecture based on SIM (joint work with C. Castellini and E. Giunchiglia). C. Castellini is in charge of maintaining the system.
  • SIM (webpage | reference paper | BibEntry), a library for the experimentation of heuristics and optimizations techniques to solve propositional satisfiability (SAT) problems (joint work with E. Giunchiglia, M. Maratea, and D. Zambonin). For problems with SIM send an e-mail to the current maintainer.
  • *SAT (webpage | reference paper | BibEntry), a framework for the development of decision procedures in modal logics (joint work with E. Giunchiglia). Notice:*SAT is not maintained any longer.

See my publications page for more resources about my research and my studies.