Roberto Sebastiani

162 papers A* 11A 37B 10C 1Misc 4Journal 71Unranked 22

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT. CoRR Emanuele Civini, Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani
2026	J	`jnl`	The Theory and Practice of MAP Inference over Non-Convex Constraints. CoRR Leander Kurscheidt, Gabriele Masina, Roberto Sebastiani, Antonio Vergari
2026	J	`jnl`	d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries. CoRR Gabriele Masina, Emanuele Civini, Massimo Michelutti, Giuseppe Spallitta, Roberto Sebastiani
2025	A	`conf`	A Probabilistic Neuro-symbolic Layer for Algebraic Constraint Satisfaction. UAI Leander Kurscheidt, Paolo Morettin, Roberto Sebastiani, Andrea Passerini, Antonio Vergari
2025	J	`jnl`	A Probabilistic Neuro-symbolic Layer for Algebraic Constraint Satisfaction. CoRR Leander Kurscheidt, Paolo Morettin, Roberto Sebastiani, Andrea Passerini, Antonio Vergari
2025	J	`jnl`	Disjoint projected enumeration for SAT and SMT without blocking clauses. Artif. Intell. Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
2025	A	`conf`	Entailment vs. Verification for Partial-Assignment Satisfiability and Enumeration. CADE Roberto Sebastiani
2025	J	`jnl`	Entailment vs. Verification for Partial-assignment Satisfiability and Enumeration. CoRR Roberto Sebastiani
2025	J	`jnl`	Exploiting Partial Assignments in Optimization Modulo Theories. CoRR Gabriele Masina, Roberto Sebastiani
2025	—	`conf`	Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories. FroCoS Gabriele Masina, Roberto Sebastiani
2025	J	`jnl`	On CNF Conversion for SAT and SMT Enumeration. J. Artif. Intell. Res. Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani
2025	J	`jnl`	On enumerating short projected models. Discret. Appl. Math. Sibylle Möhle, Roberto Sebastiani, Armin Biere
2024	J	`jnl`	A Unified Framework for Probabilistic Verification of AI Systems via Weighted Model Integration. CoRR Paolo Morettin, Andrea Passerini, Roberto Sebastiani
2024	A	`conf`	Canonical Decision Diagrams Modulo Theories. ECAI Massimo Michelutti, Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani
2024	J	`jnl`	Canonical Decision Diagrams Modulo Theories. CoRR Massimo Michelutti, Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani
2024	A*	`conf`	Disjoint Partial Enumeration without Blocking Clauses. AAAI Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
2024	J	`jnl`	Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses. CoRR Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
2024	J	`jnl`	Enhancing SMT-based Weighted Model Integration by structure awareness. Artif. Intell. Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, Roberto Sebastiani
2024	A	`conf`	Entailing Generalization Boosts Enumeration. SAT Dror Fried, Alexander Nadel, Roberto Sebastiani, Yogev Shalmon
2024	J	`jnl`	Experimenting with D-Wave Quantum Annealers on Prime Factorization problems. CoRR Jingwen Ding, Giuseppe Spallitta, Roberto Sebastiani
2024	J	`jnl`	Experimenting with D-Wave quantum annealers on prime factorization problems. Frontiers Comput. Sci. Jingwen Ding, Giuseppe Spallitta, Roberto Sebastiani
2023	J	`jnl`	Effective Prime Factorization via Quantum Annealing by Modular Locally-structured Embedding. CoRR Jingwen Ding, Giuseppe Spallitta, Roberto Sebastiani
2023	J	`jnl`	Enhancing SMT-based Weighted Model Integration by Structure Awareness. CoRR Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, Roberto Sebastiani
2023	J	`jnl`	Enumerating Disjoint Partial Models without Blocking Clauses. CoRR Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
2023	A	`conf`	On CNF Conversion for Disjoint SAT Enumeration. SAT Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani
2023	J	`jnl`	On CNF Conversion for SAT Enumeration. CoRR Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani
2022	B	`conf`	Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test. ATVA Alessandro Cimatti, Alberto Griggio, Enrico Lipparini, Roberto Sebastiani
2022	J	`jnl`	SMT-based Weighted Model Integration with Structure Awareness. CoRR Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, Roberto Sebastiani
2022	A	`conf`	SMT-based weighted model integration with structure awareness. UAI Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, Roberto Sebastiani
2021	J	`jnl`	On Enumerating Short Projected Models. CoRR Sibylle Möhle, Roberto Sebastiani, Armin Biere
2021	—	`conf`	Optimization Modulo Non-linear Arithmetic via Incremental Linearization. FroCoS Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Martin Jonás, Marco Roveri, Roberto Sebastiani, Patrick Trentin
2021	J	`jnl`	Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers. J. Autom. Reason. Patrick Trentin, Roberto Sebastiani
2021	—	`ch.`	SAT Techniques for Modal and Description Logics. Handbook of Satisfiability Roberto Sebastiani, Armando Tacchella
2021	—	`ch.`	Satisfiability Modulo Theories. Handbook of Satisfiability Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli
2020	J	`jnl`	Are You Satisfied by This Partial Assignment? CoRR Roberto Sebastiani
2020	A	`conf`	Four Flavors of Entailment. SAT Sibylle Möhle, Roberto Sebastiani, Armin Biere
2020	B	`conf`	From MiniZinc to Optimization Modulo Theories, and Back. CPAIOR Francesco Contaldo, Patrick Trentin, Roberto Sebastiani
2020	J	`jnl`	OptiMathSAT: A Tool for Optimization Modulo Theories. J. Autom. Reason. Roberto Sebastiani, Patrick Trentin
2020	J	`jnl`	Preface: Special Issue of Selected Extended Papers from IJCAR 2018. J. Autom. Reason. Didier Galmiche, Stephan Schulz, Roberto Sebastiani
2020	J	`jnl`	Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results. Inf. Comput. Zhengbing Bian, Fabián A. Chudak, William G. Macready, Aidan Roy, Roberto Sebastiani, Stefano Varotti
2019	J	`jnl`	Advanced SMT techniques for weighted model integration. Artif. Intell. Paolo Morettin, Andrea Passerini, Roberto Sebastiani
2019	J	`jnl`	From MiniZinc to Optimization Modulo Theories, and Back (Extended Version). CoRR Francesco Contaldo, Patrick Trentin, Roberto Sebastiani
2019	—	`conf`	Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization. SC-square@SIAM AG Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani
2019	J	`jnl`	Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers. CoRR Patrick Trentin, Roberto Sebastiani
2019	A	`conf`	Optimization Modulo the Theory of Floating-Point Numbers. CADE Patrick Trentin, Roberto Sebastiani
2019	A*	`conf`	The pywmi Framework and Toolbox for Probabilistic Inference using Weighted Model Integration. IJCAI Samuel Kolb, Paolo Morettin, Pedro Zuidberg Dos Martires, Francesco Sommavilla, Andrea Passerini, Roberto Sebastiani, Luc De Raedt
2018	A	`ed.`	Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings IJCAR Didier Galmiche, Stephan Schulz, Roberto Sebastiani
2018	A	`conf`	Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. SAT Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2018	J	`jnl`	Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. ACM Trans. Comput. Log. Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2018	Misc	`conf`	Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions. SYNASC Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2018	J	`jnl`	Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. CoRR Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2018	J	`jnl`	Multi-objective reasoning with constrained goal models. Requir. Eng. Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
2018	J	`jnl`	OpenMath and SMT-LIB. CoRR James H. Davenport, Matthew England, Roberto Sebastiani, Patrick Trentin
2018	B	`conf`	Planning with Strategic Goals. EDOC Evellin Cristine Souza Cardoso, Jennifer Horkoff, Roberto Sebastiani, John Mylopoulos
2018	J	`jnl`	Satisfiability Modulo Transcendental Functions via Incremental Linearization. CoRR Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2018	J	`jnl`	Solving SAT and MaxSAT with a Quantum Annealer: Foundations, Encodings, and Preliminary Results. CoRR Zhengbing Bian, Fabián A. Chudak, William G. Macready, Aidan Roy, Roberto Sebastiani, Stefano Varotti
2017	A*	`conf`	Efficient Weighted Model Integration via SMT-Based Predicate Abstraction. IJCAI Paolo Morettin, Andrea Passerini, Roberto Sebastiani
2017	—	`conf`	Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. TACAS (1) Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2017	B	`conf`	Modeling and Reasoning on Requirements Evolution with Constrained Goal Models. SEFM Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
2017	—	`conf`	On Optimization Modulo Theories, MaxSMT and Sorting Networks. TACAS (2) Roberto Sebastiani, Patrick Trentin
2017	J	`jnl`	On Optimization Modulo Theories, MaxSMT and Sorting Networks. CoRR Roberto Sebastiani, Patrick Trentin
2017	A	`conf`	Satisfiability Modulo Transcendental Functions via Incremental Linearization. CADE Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2017	—	`conf`	Solving SAT and MaxSAT with a Quantum Annealer: Foundations and a Preliminary Report. FroCoS Zhengbing Bian, Fabián A. Chudak, William G. Macready, Aidan Roy, Roberto Sebastiani, Stefano Varotti
2017	J	`jnl`	Structured learning modulo theories. Artif. Intell. Stefano Teso, Roberto Sebastiani, Andrea Passerini
2016	A	`conf`	Colors Make Theories Hard. IJCAR Roberto Sebastiani
2016	J	`jnl`	Multi Object Reasoning with Constrained Goal Model. CoRR Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
2016	—	`conf`	On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT. SMT@IJCAR Roberto Sebastiani, Patrick Trentin
2016	A	`conf`	Requirements Evolution and Evolution Requirements with Constrained Goal Models. ER Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
2016	J	`jnl`	Requirements Evolution and Evolution Requirements with Constrained Goal Models. CoRR Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
2016	A	`conf`	Verilog2SMV: A tool for word-level verification. DATE Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani
2015	—	`conf`	OptiMathSAT: A Tool for Optimization Modulo Theories. CAV (1) Roberto Sebastiani, Patrick Trentin
2015	J	`jnl`	Optimization Modulo Theories with Linear Rational Costs. ACM Trans. Comput. Log. Roberto Sebastiani, Silvia Tomasi
2015	A	`conf`	Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions. TACAS Roberto Sebastiani, Patrick Trentin
2014	J	`jnl`	Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability. CoRR Roberto Sebastiani, Michele Vescovi
2014	J	`jnl`	Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. CoRR Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2014	J	`jnl`	Hybrid SRL with Optimization Modulo Theories. CoRR Stefano Teso, Roberto Sebastiani, Andrea Passerini
2014	J	`jnl`	Optimization Modulo Theories with Linear Rational Costs. CoRR Roberto Sebastiani, Silvia Tomasi
2014	J	`jnl`	Pushing the envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions. CoRR Roberto Sebastiani, Patrick Trentin
2014	J	`jnl`	Structured Learning Modulo Theories. CoRR Stefano Teso, Roberto Sebastiani, Andrea Passerini
2013	A	`conf`	A Modular Approach to MaxSAT Modulo Theories. SAT Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani
2013	A	`conf`	The MathSAT5 SMT Solver. TACAS Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani
2012	A	`conf`	Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions. IJCAR Roberto Sebastiani, Silvia Tomasi
2012	J	`jnl`	Optimization in SMT with LA(Q) Cost Functions CoRR Roberto Sebastiani, Silvia Tomasi
2012	A	`ed.`	Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings SAT Alessandro Cimatti, Roberto Sebastiani
2011	J	`jnl`	A New General Method to Generate Random Modal Formulae for Testing Decision Procedures CoRR Peter F. Patel-Schneider, Roberto Sebastiani
2011	A	`conf`	Automated Reasoning in CADE Volker Haarslev, Roberto Sebastiani, Michele Vescovi
2011	J	`jnl`	Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. J. Artif. Intell. Res. Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2011	A	`conf`	Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. TACAS Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani
2011	—	`ch.`	Goal Modeling and Reasoning in Tropos. Social Modeling for Requirements Engineering Paolo Giorgini, John Mylopoulos, Roberto Sebastiani
2011	—	`conf`	Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT. FroCoS Alberto Griggio, Quoc-Sang Phan, Roberto Sebastiani, Silvia Tomasi
2011	J	`jnl`	Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking. Int. J. Softw. Tools Technol. Transf. Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi
2010	B	`conf`	Applying SMT in symbolic execution of microcode. FMCAD Anders Franzén, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev
2010	J	`jnl`	Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic Log. Methods Comput. Sci. Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani
2010	J	`jnl`	Efficient generation of craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2010	A	`conf`	Satisfiability Modulo the Theory of Costs: Foundations and Applications. TACAS Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani, Cristian Stenico
2009	J	`jnl`	Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability. J. Artif. Intell. Res. Roberto Sebastiani, Michele Vescovi
2009	A	`conf`	Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis. CADE Roberto Sebastiani, Michele Vescovi
2009	J	`jnl`	Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Ann. Math. Artif. Intell. Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
2009	J	`jnl`	Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories CoRR Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2009	—	`ed.`	Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009. Proceedings FroCoS Silvio Ghilardi, Roberto Sebastiani
2009	A	`conf`	Interpolant Generation for UTVPI. CADE Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2009	—	`ch.`	SAT Techniques for Modal and Description Logics. Handbook of Satisfiability Roberto Sebastiani, Armando Tacchella
2009	—	`ch.`	Satisfiability Modulo Theories. Handbook of Satisfiability Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli
2009	J	`jnl`	Software Model Checking via Large-Block Encoding CoRR Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani
2009	B	`conf`	Software model checking via large-block encoding. FMCAD Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani
2008	A	`conf`	Efficient Interpolant Generation in Satisfiability Modulo Theories. TACAS Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2008	A*	`conf`	The MathSAT 4SMT Solver. CAV Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
2007	A*	`conf`	A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. CAV Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani
2007	A	`conf`	A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. SAT Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2007	—	`conf`	From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain. FroCoS Roberto Sebastiani
2007	J	`jnl`	GSTE is partitioned model checking. Formal Methods Syst. Des. Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi
2007	J	`jnl`	Lazy Satisability Modulo Theories. J. Satisf. Boolean Model. Comput. Roberto Sebastiani
2007	J	`jnl`	Preface to Special Issue on Satisfiability Modulo Theories. J. Satisf. Boolean Model. Comput. Byron Cook, Roberto Sebastiani
2007	A	`conf`	Property-Driven Partitioning for Abstraction Refinement. TACAS Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi
2006	—	`conf`	Building Efficient Decision Procedures on Top of SAT Solvers. SFM Alessandro Cimatti, Roberto Sebastiani
2006	B	`conf`	Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis. LPAR Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
2006	J	`jnl`	Efficient theory combination via boolean search. Inf. Comput. Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani
2006	A	`conf`	Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ALC. SAT Roberto Sebastiani, Michele Vescovi
2006	—	`conf`	Preface and Foreword. PDPAR/PaUL@FLoC Byron Cook, Roberto Sebastiani
2006	B	`conf`	To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in LPAR Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani
2005	A	`conf`	An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. TACAS Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
2005	A*	`conf`	Efficient Satisfiability Modulo Theories via Delayed Theory Combination. CAV Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani
2005	—	`conf`	Encoding RTL Constructs for MathSAT: a Preliminary Report. PDPAR@CAV Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani
2005	J	`jnl`	Goal-oriented requirements analysis and reasoning in the Tropos methodology. Eng. Appl. Artif. Intell. Paolo Giorgini, John Mylopoulos, Roberto Sebastiani
2005	J	`jnl`	MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. J. Autom. Reason. Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
2005	A*	`conf`	Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking. CAV Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi
2005	A	`conf`	The MathSAT 3 System. CADE Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
2004	A*	`conf`	GSTE Is Partitioned Model Checking. CAV Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi
2004	A	`conf`	Simple and Minimum-Cost Satisfiability for Goal Models. CAiSE Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
2004	—	`conf`	Verifying Industrial Hybrid Systems with MathSAT. BMC@CAV Gilles Audemard, Marco Bozzano, Alessandro Cimatti, Roberto Sebastiani
2003	—	`conf`	"More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking. CHARME Roberto Sebastiani, Stefano Tonetta
2003	J	`jnl`	A New General Method to Generate Random Modal Formulae for Testing Decision Procedures. J. Artif. Intell. Res. Peter F. Patel-Schneider, Roberto Sebastiani
2003	J	`jnl`	Formal Reasoning Techniques for Goal Models. J. Data Semant. Paolo Giorgini, John Mylopoulos, Eleonora Nicchiarelli, Roberto Sebastiani
2002	A	`conf`	A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. CADE Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani
2002	C	`conf`	Bounded Model Checking for Timed Systems. FORTE Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani
2002	J	`jnl`	Editorial: The Integration of Automated Reasoning and Computer Algebra Systems. J. Symb. Comput. Steve Linton, Roberto Sebastiani
2002	B	`conf`	Improving the Encoding of LTL Model Checking into SAT. VMCAI Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani
2002	—	`conf`	Integrating BDD-Based and SAT-Based Symbolic Model Checking. FroCoS Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella
2002	Misc	`conf`	Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements. AISC Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani
2002	A*	`conf`	NuSMV 2: An OpenSource Tool for Symbolic Model Checking. CAV Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella
2002	A	`conf`	Reasoning with Goal Models. ER Paolo Giorgini, John Mylopoulos, Eleonora Nicchiarelli, Roberto Sebastiani
2001	A	`conf`	A New System and Methodology for Generating Random Modal Formulae. IJCAR Peter F. Patel-Schneider, Roberto Sebastiani
2001	A	`conf`	Model Checking Syllabi and Student Carreers. TACAS Roberto Sebastiani, Alessandro Tomasi, Fausto Giunchiglia
2000	J	`jnl`	An Analysis of Empirical Testing for Modal Decision Procedures. Log. J. IGPL Ian Horrocks, Peter F. Patel-Schneider, Roberto Sebastiani
2000	J	`jnl`	Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m). Inf. Comput. Fausto Giunchiglia, Roberto Sebastiani
2000	J	`jnl`	SAT vs. translation based decision procedures for modal logics: a comparative evaluation. J. Appl. Non Class. Logics Enrico Giunchiglia, Fausto Giunchiglia, Roberto Sebastiani, Armando Tacchella
1999	—	`conf`	Applying the Davis-Putnam Procedure to Non-clausal Formulas. AI*IA Enrico Giunchiglia, Roberto Sebastiani
1999	B	`conf`	Formal Specification and Development of a Safety-Critical Train Management System. SAFECOMP Angelo Chiappini, Alessandro Cimatti, Carmen Porzia, G. Rotondo, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita
1999	—	`conf`	Formal Specification and Validation of a Vital Communication Protocol. World Congress on Formal Methods Alessandro Cimatti, P. L. Pieraccini, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita
1998	—	`conf`	Act, and the Rest Will Follow: Exploiting Determinism in Planning as Satisfiability. AAAI/IAAI Enrico Giunchiglia, Alessandro Massarotto, Roberto Sebastiani
1998	A*	`conf`	More Evaluation of Decision Procedures for Modal Logics. KR Enrico Giunchiglia, Fausto Giunchiglia, Roberto Sebastiani, Armando Tacchella
1998	Misc	`conf`	SAT-Based Decision Procedures for Normal Modal Logics: A Theoretical Framework. AIMSA Roberto Sebastiani, Adolfo Villafiorita
1997	A	`conf`	A New Method for Testing Decision Procedures in Modal Logics. CADE Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani
1996	Misc	`conf`	A General Purpose Reasoner for Abstraction. AI Fausto Giunchiglia, Roberto Sebastiani, Adolfo Villafiorita, Toby Walsh
1996	—	`conf`	A New Method for Testing Decision Procedures in Modal and Terminological Logics. Description Logics Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani
1996	A*	`conf`	A SAT-based Decision Procedure for ALC. KR Fausto Giunchiglia, Roberto Sebastiani
1996	—	`conf`	An SAT-based Decision Procedure for ALC. Description Logics Fausto Giunchiglia, Roberto Sebastiani
1996	A	`conf`	Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K. CADE Fausto Giunchiglia, Roberto Sebastiani
1996	J	`jnl`	Calculating Criticalities. Artif. Intell. Alan Bundy, Fausto Giunchiglia, Roberto Sebastiani, Toby Walsh
1996	—	`conf`	Computing Abstraction Hierarchies by Numerical Simulation. AAAI/IAAI, Vol. 1 Alan Bundy, Fausto Giunchiglia, Roberto Sebastiani, Toby Walsh
1994	J	`jnl`	Applying GSAT to Non-Clausal Formulas (Research Note). J. Artif. Intell. Res. Roberto Sebastiani
1994	J	`jnl`	Applying GSAT to Non-Clausal Formulas. CoRR Roberto Sebastiani