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.
|