Roberto Sebastiani

Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani: The MathSAT5 SMT Solver. TACAS 2013: 93-107

Roberto Sebastiani, Silvia Tomasi: Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions. IJCAR 2012: 484-498

Alessandro Cimatti, Roberto Sebastiani (Eds.): Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings. Lecture Notes in Computer Science 7317, Springer 2012, isbn 978-3-642-31611-1

Roberto Sebastiani, Silvia Tomasi: Optimization in SMT with LA(Q) Cost Functions. CoRR abs/1202.1409 (2012)

Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani: Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. J. Artif. Intell. Res. (JAIR) 40: 701-728 (2011)

Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi: Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking. STTT 13(4): 319-335 (2011)

Volker Haarslev, Roberto Sebastiani, Michele Vescovi: Automated Reasoning in ALCQ\mathcal{ALCQ} via SMT. CADE 2011: 283-298

Alberto Griggio, Quoc-Sang Phan, Roberto Sebastiani, Silvia Tomasi: Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT. FroCoS 2011: 163-178

Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani: Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. TACAS 2011: 143-157

Peter F. Patel-Schneider, Roberto Sebastiani: A New General Method to Generate Random Modal Formulae for Testing Decision Procedures. CoRR abs/1106.5261 (2011)

Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani: Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. Logical Methods in Computer Science 8(3) (2010)

Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani: Efficient generation of craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. 12(1): 7 (2010)

Anders Franzén, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev: Applying SMT in symbolic execution of microcode. FMCAD 2010: 121-128

Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani, Cristian Stenico: Satisfiability Modulo the Theory of Costs: Foundations and Applications. TACAS 2010: 99-113

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Ann. Math. Artif. Intell. 55(1-2): 63-99 (2009)

Roberto Sebastiani, Michele Vescovi: Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability. J. Artif. Intell. Res. (JAIR) 35: 343-389 (2009)

Roberto Sebastiani, Michele Vescovi: Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis. CADE 2009: 84-99

Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani: Interpolant Generation for UTVPI. CADE 2009: 167-182

Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani: Software model checking via large-block encoding. FMCAD 2009: 25-32

Roberto Sebastiani, Armando Tacchella: SAT Techniques for Modal and Description Logics. Handbook of Satisfiability 2009: 781-824

Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli: Satisfiability Modulo Theories. Handbook of Satisfiability 2009: 825-885

Silvio Ghilardi, Roberto Sebastiani (Eds.): Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009. Proceedings. Lecture Notes in Computer Science 5749, Springer 2009, isbn 978-3-642-04221-8

Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani: Software Model Checking via Large-Block Encoding. CoRR abs/0904.4709 (2009)

Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani: Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories. CoRR abs/0906.4492 (2009)

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani: The MathSAT 4SMT Solver. CAV 2008: 299-303

Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani: Efficient Interpolant Generation in Satisfiability Modulo Theories. TACAS 2008: 397-412

Byron Cook, Roberto Sebastiani: Preface and Foreword. Electr. Notes Theor. Comput. Sci. 174(8): 3-6 (2007)

Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi: GSTE is partitioned model checking. Formal Methods in System Design 31(2): 177-196 (2007)

Byron Cook, Roberto Sebastiani: Preface. JSAT 3(1-2) (2007)

Roberto Sebastiani: Lazy Satisability Modulo Theories. JSAT 3(3-4): 141-224 (2007)

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani: A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. CAV 2007: 547-560

Roberto Sebastiani: From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain. FroCoS 2007: 28-46

Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani: A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. SAT 2007: 334-339

Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi: Property-Driven Partitioning for Abstraction Refinement. TACAS 2007: 389-404

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani: Encoding RTL Constructs for MathSAT: a Preliminary Report. Electr. Notes Theor. Comput. Sci. 144(2): 3-14 (2006)

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani: Efficient theory combination via boolean search. Inf. Comput. 204(10): 1493-1525 (2006)

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani: Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis. LPAR 2006: 527-541

Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani: To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT). LPAR 2006: 557-571

Roberto Sebastiani, Michele Vescovi: Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ALC. SAT 2006: 130-135

Alessandro Cimatti, Roberto Sebastiani: Building Efficient Decision Procedures on Top of SAT Solvers. SFM 2006: 144-175

Paolo Giorgini, John Mylopoulos, Roberto Sebastiani: Goal-oriented requirements analysis and reasoning in the Tropos methodology. Eng. Appl. of AI 18(2): 159-171 (2005)

Gilles Audemard, Marco Bozzano, Alessandro Cimatti, Roberto Sebastiani: Verifying Industrial Hybrid Systems with MathSAT. Electr. Notes Theor. Comput. Sci. 119(2): 17-32 (2005)

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. J. Autom. Reasoning 35(1-3): 265-293 (2005)

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: The MathSAT 3 System. CADE 2005: 315-321

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani: Efficient Satisfiability Modulo Theories via Delayed Theory Combination. CAV 2005: 335-349

Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi: Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking. CAV 2005: 350-363

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. TACAS 2005: 317-333

Roberto Sebastiani, Paolo Giorgini, John Mylopoulos: Simple and Minimum-Cost Satisfiability for Goal Models. CAiSE 2004: 20-35

Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi: GSTE Is Partitioned Model Checking. CAV 2004: 229-241

Peter F. Patel-Schneider, Roberto Sebastiani: A New General Method to Generate Random Modal Formulae for Testing Decision Procedures. J. Artif. Intell. Res. (JAIR) 18: 351-389 (2003)

Paolo Giorgini, John Mylopoulos, Eleonora Nicchiarelli, Roberto Sebastiani: Formal Reasoning Techniques for Goal Models. J. Data Semantics 1: 1-20 (2003)

Roberto Sebastiani, Stefano Tonetta: "More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking. CHARME 2003: 126-140

Steve Linton, Roberto Sebastiani: Editorial: The Integration of Automated Reasoning and Computer Algebra Systems. J. Symb. Comput. 34(4): 239 (2002)

Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani: Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements. AISC 2002: 231-245

Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani: A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. CADE 2002: 195-210

Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. CAV 2002: 359-364

Paolo Giorgini, John Mylopoulos, Eleonora Nicchiarelli, Roberto Sebastiani: Reasoning with Goal Models. ER 2002: 167-181

Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani: Bounded Model Checking for Timed Systems. FORTE 2002: 243-259

Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella: Integrating BDD-Based and SAT-Based Symbolic Model Checking. FroCoS 2002: 49-56

Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani: Improving the Encoding of LTL Model Checking into SAT. VMCAI 2002: 196-207

Peter F. Patel-Schneider, Roberto Sebastiani: A New System and Methodology for Generating Random Modal Formulae. IJCAR 2001: 464-468

Roberto Sebastiani, Alessandro Tomasi, Fausto Giunchiglia: Model Checking Syllabi and Student Carreers. TACAS 2001: 128-142

Fausto Giunchiglia, Roberto Sebastiani: Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m). Inf. Comput. 162(1-2): 158-178 (2000)

Ian Horrocks, Peter F. Patel-Schneider, Roberto Sebastiani: An Analysis of Empirical Testing for Modal Decision Procedures. Logic Journal of the IGPL 8(3): 293-323 (2000)

Enrico Giunchiglia, Fausto Giunchiglia, Roberto Sebastiani, Armando Tacchella: SAT vs. translation based decision procedures for modal logics: a comparative evaluation. Journal of Applied Non-Classical Logics 10(2): 145-172 (2000)

Enrico Giunchiglia, Roberto Sebastiani: Applying the Davis-Putnam Procedure to Non-clausal Formulas. AI*IA 1999: 84-94

Alessandro Cimatti, P. L. Pieraccini, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita: Formal Specification and Validation of a Vital Communication Protocol. World Congress on Formal Methods 1999: 1584-1604

Angelo Chiappini, Alessandro Cimatti, Carmen Porzia, G. Rotondo, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita: Formal Specification and Development of a Safety-Critical Train Management System. SAFECOMP 1999: 410-419

Enrico Giunchiglia, Alessandro Massarotto, Roberto Sebastiani: Act, and the Rest Will Follow: Exploiting Determinism in Planning as Satisfiability. AAAI/IAAI 1998: 948-953

Roberto Sebastiani, Adolfo Villafiorita: SAT-Based Decision Procedures for Normal Modal Logics: A Theoretical Framework. AIMSA 1998: 377-388

Enrico Giunchiglia, Fausto Giunchiglia, Roberto Sebastiani, Armando Tacchella: More Evaluation of Decision Procedures for Modal Logics. KR 1998: 626-635

Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani: A New Method for Testing Decision Procedures in Modal Logics. CADE 1997: 264-267

Alan Bundy, Fausto Giunchiglia, Roberto Sebastiani, Toby Walsh: Calculating Criticalities. Artif. Intell. 88(1-2): 39-67 (1996)

Alan Bundy, Fausto Giunchiglia, Roberto Sebastiani, Toby Walsh: Computing Abstraction Hierarchies by Numerical Simulation. AAAI/IAAI, Vol. 1 1996: 523-529

Fausto Giunchiglia, Roberto Sebastiani, Adolfo Villafiorita, Toby Walsh: A General Purpose Reasoner for Abstraction. Canadian Conference on AI 1996: 323-335

Fausto Giunchiglia, Roberto Sebastiani: Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K. CADE 1996: 583-597

Fausto Giunchiglia, Roberto Sebastiani: An SAT-based Decision Procedure for ALC. Description Logics 1996: 49-59

Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani: A New Method for Testing Decision Procedures in Modal and Terminological Logics. Description Logics 1996: 119-123

Fausto Giunchiglia, Roberto Sebastiani: A SAT-based Decision Procedure for ALC. KR 1996: 304-314

Roberto Sebastiani: Applying GSAT to Non-Clausal Formulas (Research Note). J. Artif. Intell. Res. (JAIR) 1: 309-314 (1994)