Roberto Sebastiani - automated reasoning and verification software
The following is a list of automated reasoning software
whose development I've been involved with.
- PyWMI,
a tool tool for weighted model integration for probabilistic
reasoning, as described in [Morettin et al, AIJ 2019]
- PyLMT,
a tool for Learning Modulo Theories for Hybrid
Machine Learning, as described in [Teso et al, AIJ 2017]
- CGM-Tool, a tool for modeling and reasoning on constrained
goal models for requirement engineering, as described in [Nguyen et al,
RE 2017]
- Verilog2SMV , a FV
tool which converting Verilog designs to a model checking RTL
problems, as described in [Cimatti et al. DATE 2016]
- OptiMathSAT,
an Optimization Modulo Theories (OMT) procedure, as described in [Sebastiani and
Trentin, JAR 2018]
- MathSAT,
a state-of-the-art SMT solver, presented in
[Cimatti at al, TACAS'13]
- 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]
(The following systems, whose development I've been involved with, are no more available/maintained).
- Gr-Tool,
a forward-and-backward reasoner for Goal Models in the TROPOS methodology, presented in
[Giorgini et al., ER'02]
- EL2SAT,
a SAT&SMT-based tool for debugging Medical Ontologies based on
EL+ description logic, described in
[Sebastiani and Vescovi, CADE'09]
- 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]
- 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.
Back to
Roberto Sebastiani's home page.