Roberto Sebastiani
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
70
Venues
27
Active years
1996–2026
Best venue rank
A*
Where they publish
- ACADE14 papers
- ATACAS10 papers
- ASAT8 papers
- A*CAV7 papers
- A*AAAI3 papers
- AUAI2 papers
- A*IJCAI2 papers
- AER2 papers
- BFMCAD2 papers
- BLPAR2 papers
- A*KR2 papers
- AIJCAR1 paper
- AECAI1 paper
- BATVA1 paper
- BCPAIOR1 paper
- BEDOC1 paper
- NationalSYNASC1 paper
- BSEFM1 paper
- ADATE1 paper
- ACaiSE1 paper
- AustralasianAISC1 paper
- CFORTE1 paper
- BVMCAI1 paper
- BFM1 paper
- BSAFECOMP1 paper
- NationalAIMSA1 paper
- AustralasianAI1 paper
Papers
70 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | IJCAR | Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT. | Emanuele Civini, Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani |
| 2026 | SAT | d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries. | Gabriele Masina, Emanuele Civini, Massimo Michelutti, Giuseppe Spallitta, Roberto Sebastiani |
| 2025 | CADE | Entailment vs. Verification for Partial-Assignment Satisfiability and Enumeration. | Roberto Sebastiani |
| 2025 | UAI | A Probabilistic Neuro-symbolic Layer for Algebraic Constraint Satisfaction. | Leander Kurscheidt, Paolo Morettin, Roberto Sebastiani, Andrea Passerini, Antonio Vergari |
| 2024 | AAAI | Disjoint Partial Enumeration without Blocking Clauses. | Giuseppe Spallitta, Roberto Sebastiani, Armin Biere |
| 2024 | ECAI | Canonical Decision Diagrams Modulo Theories. | Massimo Michelutti, Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani |
| 2024 | SAT | Entailing Generalization Boosts Enumeration. | Dror Fried, Alexander Nadel, Roberto Sebastiani, Yogev Shalmon |
| 2023 | SAT | On CNF Conversion for Disjoint SAT Enumeration. | Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani |
| 2022 | ATVA | Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test. | Alessandro Cimatti, Alberto Griggio, Enrico Lipparini, Roberto Sebastiani |
| 2022 | UAI | SMT-based weighted model integration with structure awareness. | Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, Roberto Sebastiani |
| 2020 | CPAIOR | From MiniZinc to Optimization Modulo Theories, and Back. | Francesco Contaldo, Patrick Trentin, Roberto Sebastiani |
| 2020 | SAT | Four Flavors of Entailment. | Sibylle Mhle, Roberto Sebastiani, Armin Biere |
| 2019 | CADE | Optimization Modulo the Theory of Floating-Point Numbers. | Patrick Trentin, Roberto Sebastiani |
| 2019 | IJCAI | The pywmi Framework and Toolbox for Probabilistic Inference using Weighted Model Integration. | Samuel Kolb, Paolo Morettin, Pedro Zuidberg Dos Martires, Francesco Sommavilla, Andrea Passerini, Roberto Sebastiani, Luc De Raedt |
| 2018 | EDOC | Planning with Strategic Goals. | Evellin Cristine Souza Cardoso, Jennifer Horkoff, Roberto Sebastiani, John Mylopoulos |
| 2018 | SAT | Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. | Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani |
| 2018 | SYNASC | Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions. | Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani |
| 2017 | CADE | Satisfiability Modulo Transcendental Functions via Incremental Linearization. | Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani |
| 2017 | IJCAI | Efficient Weighted Model Integration via SMT-Based Predicate Abstraction. | Paolo Morettin, Andrea Passerini, Roberto Sebastiani |
| 2017 | SEFM | Modeling and Reasoning on Requirements Evolution with Constrained Goal Models. | Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos |
| 2017 | TACAS | Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. | Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani |
| 2017 | TACAS | On Optimization Modulo Theories, MaxSMT and Sorting Networks. | Roberto Sebastiani, Patrick Trentin |
| 2016 | CADE | Colors Make Theories Hard. | Roberto Sebastiani |
| 2016 | CADE | On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT. | Roberto Sebastiani, Patrick Trentin |
| 2016 | DATE | Verilog2SMV: A tool for word-level verification. | Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani |
| 2016 | ER | Requirements Evolution and Evolution Requirements with Constrained Goal Models. | Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos |
| 2015 | CAV | OptiMathSAT: A Tool for Optimization Modulo Theories. | Roberto Sebastiani, Patrick Trentin |
| 2015 | TACAS | Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions. | Roberto Sebastiani, Patrick Trentin |
| 2013 | SAT | A Modular Approach to MaxSAT Modulo Theories. | Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani |
| 2013 | TACAS | The MathSAT5 SMT Solver. | Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani |
| 2012 | CADE | Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions. | Roberto Sebastiani, Silvia Tomasi |
| 2011 | CADE | Automated Reasoning in | Volker Haarslev, Roberto Sebastiani, Michele Vescovi |
| 2011 | TACAS | Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. | Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani |
| 2010 | FMCAD | Applying SMT in symbolic execution of microcode. | Anders Franzn, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev |
| 2010 | TACAS | Satisfiability Modulo the Theory of Costs: Foundations and Applications. | Alessandro Cimatti, Anders Franzn, Alberto Griggio, Roberto Sebastiani, Cristian Stenico |
| 2009 | CADE | Interpolant Generation for UTVPI. | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
| 2009 | CADE | Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis. | Roberto Sebastiani, Michele Vescovi |
| 2009 | FMCAD | Software model checking via large-block encoding. | Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani |
| 2008 | CAV | The MathSAT 4SMT Solver. | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzn, Alberto Griggio, Roberto Sebastiani |
| 2008 | TACAS | Efficient Interpolant Generation in Satisfiability Modulo Theories. | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
| 2007 | CAV | A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzn, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani |
| 2007 | SAT | A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
| 2007 | TACAS | Property-Driven Partitioning for Abstraction Refinement. | Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi |
| 2006 | LPAR | Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis. | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzn, Alberto Griggio, Roberto Sebastiani |
| 2006 | LPAR | To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzn, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani |
| 2006 | SAT | Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ALC. | Roberto Sebastiani, Michele Vescovi |
| 2005 | CADE | The MathSAT 3 System. | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani |
| 2005 | CAV | Efficient Satisfiability Modulo Theories via Delayed Theory Combination. | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani |
| 2005 | CAV | Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking. | Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi |
| 2005 | TACAS | An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani |
| 2004 | CaiSE | Simple and Minimum-Cost Satisfiability for Goal Models. | Roberto Sebastiani, Paolo Giorgini, John Mylopoulos |
| 2004 | CAV | GSTE Is Partitioned Model Checking. | Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi |
| 2002 | AISC | Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements. | Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani |
| 2002 | CADE | A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. | Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani |
| 2002 | CAV | NuSMV 2: An OpenSource Tool for Symbolic Model Checking. | Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella |
| 2002 | ER | Reasoning with Goal Models. | Paolo Giorgini, John Mylopoulos, Eleonora Nicchiarelli, Roberto Sebastiani |
| 2002 | FORTE | Bounded Model Checking for Timed Systems. | Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani |
| 2002 | VMCAI | Improving the Encoding of LTL Model Checking into SAT. | Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani |
| 2001 | CADE | A New System and Methodology for Generating Random Modal Formulae. | Peter F. Patel-Schneider, Roberto Sebastiani |
| 2001 | TACAS | Model Checking Syllabi and Student Carreers. | Roberto Sebastiani, Alessandro Tomasi, Fausto Giunchiglia |
| 1999 | FM | Formal Specification and Validation of a Vital Communication Protocol. | Alessandro Cimatti, P. L. Pieraccini, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita |
| 1999 | SAFECOMP | Formal Specification and Development of a Safety-Critical Train Management System. | Angelo Chiappini, Alessandro Cimatti, Carmen Porzia, G. Rotondo, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita |
| 1998 | AAAI | Act, and the Rest Will Follow: Exploiting Determinism in Planning as Satisfiability. | Enrico Giunchiglia, Alessandro Massarotto, Roberto Sebastiani |
| 1998 | AIMSA | SAT-Based Decision Procedures for Normal Modal Logics: A Theoretical Framework. | Roberto Sebastiani, Adolfo Villafiorita |
| 1998 | KR | More Evaluation of Decision Procedures for Modal Logics. | Enrico Giunchiglia, Fausto Giunchiglia, Roberto Sebastiani, Armando Tacchella |
| 1997 | CADE | A New Method for Testing Decision Procedures in Modal Logics. | Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani |
| 1996 | AAAI | Computing Abstraction Hierarchies by Numerical Simulation. | Alan Bundy, Fausto Giunchiglia, Roberto Sebastiani, Toby Walsh |
| 1996 | AI | A General Purpose Reasoner for Abstraction. | Fausto Giunchiglia, Roberto Sebastiani, Adolfo Villafiorita, Toby Walsh |
| 1996 | CADE | Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K. | Fausto Giunchiglia, Roberto Sebastiani |
| 1996 | KR | A SAT-based Decision Procedure for ALC. | Fausto Giunchiglia, Roberto Sebastiani |