Roberto Sebastiani - automated reasoning and verification software
The following is a list of automated reasoning software
whose development I've been involved with.
(The following systems, whose development I've been involved with, are no more available/maintained).
an Optimization Modulo Theories (OMT) procedure
a state-of-the-art SMT solver
a OBBD based and SAT based symbolic Model Checker, presented in
[Cimatti at al, CAV02]
a forward-and-backward reasoner for Goal Models in the TROPOS methodology, presented in
[Giorgini et al., ER'02]
a SAT&SMT-based tool for debugging Medical Ontologies based on
EL+ description logic, described in
[Sebastiani and Vescovi, CADE'09]
an efficient platform for experimenting with SAT-based decision
presented in [Giunchiglia et al., JAR, 2002]
the LTL to Buechi Automata translator described in the paper
"More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking
[Sebastiani and Tonetta, CHARME'03]
an "ad hoc" SAT procedure for SAT-encoded planning presented in [Giunchiglia, Massarotto &
Sebastiani; AAAI98] (to be interfaced with the
SAT-based planner medic.)
the improved C version of the KSAT procedure, as
presented in [Giunchiglia, Giunchiglia, Sebastiani & Tacchella; KR98, JANCL2000].
the original LISP implementation of the KSAT procedure
presented in [Giunchiglia & Sebastiani; CADE96, KR96, INFO&COMP2000].
- RESISTOR & PROBABILITY,
a LISP software for authomatic calculation of abstraction hierarchies in
ABSTRIPS-like planners, presented in [Bundy, Giunchiglia, Sebastiani
& Walsh; AAAI96, AIJ97] (to be interfaced with the
a straightforward LISP implementation of the algorithm
presented in [Sebastiani; JAIR94] (to be interfaced with the GETFOL system)
an interactive theorem prover.
Roberto Sebastiani's home page.