Roberto Sebastiani - automated reasoning and verification software

• MoDeLLA, 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]

• MathSAT, a SAT based tool for solving boolean formulas over boolean atoms and linear mathematical expressions over the reals, presented in [Audemard et al., CADE02 and Calculemus02]

• NuSMV2, a OBBD based and SAT based symbolic Model Checker, presented in [Cimatti at al, CAV02]

• *SAT, an efficient platform for experimenting with SAT-based decision procedures, presented in [Giunchiglia et al., JAR, 2002]

• TABLEAU*, an "ad hoc" SAT procedure for SAT-encoded planning presented in [Giunchiglia, Massarotto & Sebastiani; AAAI98] (to be interfaced with the SAT-based planner medic.)

• KsatC, the improved C version of the KSAT procedure, as presented in [Giunchiglia, Giunchiglia, Sebastiani & Tacchella; KR98, JANCL2000].

• Ksat, 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 planner AbTweak.)

• NCGSAT, a straightforward LISP implementation of the algorithm presented in [Sebastiani; JAIR94] (to be interfaced with the GETFOL system)

• GETFOL, an interactive theorem prover.