Roberto Sebastiani

ORCID

Publication Activity (10 Years)

Years Active: 1994-2024
Publications (10 Years): 56

Top Venues

Publications

Dror Fried, Alexander Nadel, Roberto Sebastiani, Yogev Shalmon
Entailing Generalization Boosts Enumeration. SAT (2024)
Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, Roberto Sebastiani
Enhancing SMT-based Weighted Model Integration by structure awareness. Artif. Intell. 328 (2024)
Paolo Morettin, Andrea Passerini, Roberto Sebastiani
A Unified Framework for Probabilistic Verification of AI Systems via Weighted Model Integration. CoRR (2024)
Jingwen Ding, Giuseppe Spallitta, Roberto Sebastiani
Experimenting with D-Wave Quantum Annealers on Prime Factorization problems. CoRR (2024)
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
Disjoint Partial Enumeration without Blocking Clauses. AAAI (2024)
Massimo Michelutti, Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani
Canonical Decision Diagrams Modulo Theories. CoRR (2024)
Jingwen Ding, Giuseppe Spallitta, Roberto Sebastiani
Experimenting with D-Wave quantum annealers on prime factorization problems. Frontiers Comput. Sci. 6 (2024)
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
Enumerating Disjoint Partial Models without Blocking Clauses. CoRR (2023)
Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani
On CNF Conversion for SAT Enumeration. CoRR (2023)
Jingwen Ding, Giuseppe Spallitta, Roberto Sebastiani
Effective Prime Factorization via Quantum Annealing by Modular Locally-structured Embedding. CoRR (2023)
Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani
On CNF Conversion for Disjoint SAT Enumeration. SAT (2023)
Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, Roberto Sebastiani
Enhancing SMT-based Weighted Model Integration by Structure Awareness. CoRR (2023)
Alessandro Cimatti, Alberto Griggio, Enrico Lipparini, Roberto Sebastiani
Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test. ATVA (2022)
Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, Roberto Sebastiani
SMT-based Weighted Model Integration with Structure Awareness. CoRR (2022)
Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, Roberto Sebastiani
SMT-based weighted model integration with structure awareness. UAI (2022)
Patrick Trentin, Roberto Sebastiani
Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers. J. Autom. Reason. 65 (7) (2021)
Sibylle Möhle, Roberto Sebastiani, Armin Biere
On Enumerating Short Projected Models. CoRR (2021)
Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Martin Jonás, Marco Roveri, Roberto Sebastiani, Patrick Trentin
Optimization Modulo Non-linear Arithmetic via Incremental Linearization. FroCoS (2021)
Francesco Contaldo, Patrick Trentin, Roberto Sebastiani
From MiniZinc to Optimization Modulo Theories, and Back. CPAIOR (2020)
Roberto Sebastiani, Patrick Trentin
OptiMathSAT: A Tool for Optimization Modulo Theories. J. Autom. Reason. 64 (3) (2020)
Didier Galmiche, Stephan Schulz, Roberto Sebastiani
Preface: Special Issue of Selected Extended Papers from IJCAR 2018. J. Autom. Reason. 64 (7) (2020)
Zhengbing Bian, Fabián A. Chudak, William G. Macready, Aidan Roy, Roberto Sebastiani, Stefano Varotti
Solving SAT (and MaxSAT) with a quantum annealer: Foundations, encodings, and preliminary results. Inf. Comput. 275 (2020)
Sibylle Möhle, Roberto Sebastiani, Armin Biere
Four Flavors of Entailment. SAT (2020)
Roberto Sebastiani
Are You Satisfied by This Partial Assignment? CoRR (2020)
Francesco Contaldo, Patrick Trentin, Roberto Sebastiani
From MiniZinc to Optimization Modulo Theories, and Back (Extended Version). CoRR (2019)
Patrick Trentin, Roberto Sebastiani
Optimization Modulo the Theories of Signed Bit-Vectors and Floating-Point Numbers. CoRR (2019)
Patrick Trentin, Roberto Sebastiani
Optimization Modulo the Theory of Floating-Point Numbers. CADE (2019)
Paolo Morettin, Andrea Passerini, Roberto Sebastiani
Advanced SMT techniques for weighted model integration. Artif. Intell. 275 (2019)
Samuel Kolb, Paolo Morettin, Pedro Zuidberg Dos Martires, Francesco Sommavilla, Andrea Passerini, Roberto Sebastiani, Luc De Raedt
The pywmi Framework and Toolbox for Probabilistic Inference using Weighted Model Integration. IJCAI (2019)
Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani
Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization. SC-square@SIAM AG (2019)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. CoRR (2018)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. SAT (2018)
Evellin Cristine Souza Cardoso, Jennifer Horkoff, Roberto Sebastiani, John Mylopoulos
Planning with Strategic Goals. EDOC (2018)
Zhengbing Bian, Fabián A. Chudak, William G. Macready, Aidan Roy, Roberto Sebastiani, Stefano Varotti
Solving SAT and MaxSAT with a Quantum Annealer: Foundations, Encodings, and Preliminary Results. CoRR (2018)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. ACM Trans. Comput. Log. 19 (3) (2018)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Satisfiability Modulo Transcendental Functions via Incremental Linearization. CoRR (2018)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions. SYNASC (2018)
James H. Davenport, Matthew England, Roberto Sebastiani, Patrick Trentin
OpenMath and SMT-LIB. CoRR (2018)
Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
Multi-objective reasoning with constrained goal models. Requir. Eng. 23 (2) (2018)
Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
Modeling and Reasoning on Requirements Evolution with Constrained Goal Models. SEFM (2017)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. TACAS (1) (2017)
Roberto Sebastiani, Patrick Trentin
On Optimization Modulo Theories, MaxSMT and Sorting Networks. CoRR (2017)
Zhengbing Bian, Fabián A. Chudak, William G. Macready, Aidan Roy, Roberto Sebastiani, Stefano Varotti
Solving SAT and MaxSAT with a Quantum Annealer: Foundations and a Preliminary Report. FroCoS (2017)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Satisfiability Modulo Transcendental Functions via Incremental Linearization. CADE (2017)
Roberto Sebastiani, Patrick Trentin
On Optimization Modulo Theories, MaxSMT and Sorting Networks. TACAS (2) (2017)
Paolo Morettin, Andrea Passerini, Roberto Sebastiani
Efficient Weighted Model Integration via SMT-Based Predicate Abstraction. IJCAI (2017)
Stefano Teso, Roberto Sebastiani, Andrea Passerini
Structured learning modulo theories. Artif. Intell. 244 (2017)
Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
Requirements Evolution and Evolution Requirements with Constrained Goal Models. ER (2016)
Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
Multi Object Reasoning with Constrained Goal Model. CoRR (2016)
Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani
Verilog2SMV: A tool for word-level verification. DATE (2016)
Roberto Sebastiani, Patrick Trentin
On the Benefits of Enhancing Optimization Modulo Theories with Sorting Networks for MaxSMT. SMT@IJCAR (2016)
Roberto Sebastiani
Colors Make Theories Hard. IJCAR (2016)
Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
Requirements Evolution and Evolution Requirements with Constrained Goal Models. CoRR (2016)
Roberto Sebastiani, Patrick Trentin
OptiMathSAT: A Tool for Optimization Modulo Theories. CAV (1) (2015)
Roberto Sebastiani, Patrick Trentin
Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions. TACAS (2015)
Roberto Sebastiani, Silvia Tomasi
Optimization Modulo Theories with Linear Rational Costs. ACM Trans. Comput. Log. 16 (2) (2015)
Stefano Teso, Roberto Sebastiani, Andrea Passerini
Hybrid SRL with Optimization Modulo Theories. CoRR (2014)
Roberto Sebastiani, Patrick Trentin
Pushing the envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions. CoRR (2014)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. CoRR (2014)
Stefano Teso, Roberto Sebastiani, Andrea Passerini
Structured Learning Modulo Theories. CoRR (2014)
Roberto Sebastiani, Silvia Tomasi
Optimization Modulo Theories with Linear Rational Costs. CoRR (2014)
Roberto Sebastiani, Michele Vescovi
Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability. CoRR (2014)
Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani
The MathSAT5 SMT Solver. TACAS (2013)
Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani
A Modular Approach to MaxSAT Modulo Theories. SAT (2013)
Roberto Sebastiani, Silvia Tomasi
Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions. IJCAR (2012)
Roberto Sebastiani, Silvia Tomasi
Optimization in SMT with LA(Q) Cost Functions CoRR (2012)
Volker Haarslev, Roberto Sebastiani, Michele Vescovi
\mathcal{ALCQ} via SMT. CADE (2011)
Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. TACAS (2011)
Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi
Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking. Int. J. Softw. Tools Technol. Transf. 13 (4) (2011)
Peter F. Patel-Schneider, Roberto Sebastiani
A New General Method to Generate Random Modal Formulae for Testing Decision Procedures CoRR (2011)
Alberto Griggio, Quoc-Sang Phan, Roberto Sebastiani, Silvia Tomasi
Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT. FroCoS (2011)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. J. Artif. Intell. Res. 40 (2011)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Efficient generation of craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. 12 (1) (2010)
Anders Franzén, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev
Applying SMT in symbolic execution of microcode. FMCAD (2010)
Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic Log. Methods Comput. Sci. 8 (3) (2010)
Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani, Cristian Stenico
Satisfiability Modulo the Theory of Costs: Foundations and Applications. TACAS (2010)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Interpolant Generation for UTVPI. CADE (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. 35 (2009)
Roberto Sebastiani, Michele Vescovi
Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis. CADE (2009)
Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani
Software Model Checking via Large-Block Encoding CoRR (2009)
Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani
Software model checking via large-block encoding. FMCAD (2009)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories CoRR (2009)
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) (2009)
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
The MathSAT 4SMT Solver. CAV (2008)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Efficient Interpolant Generation in Satisfiability Modulo Theories. TACAS (2008)
Byron Cook, Roberto Sebastiani
Preface and Foreword. Electron. Notes Theor. Comput. Sci. 174 (8) (2007)
Roberto Sebastiani
Lazy Satisability Modulo Theories. J. Satisf. Boolean Model. Comput. 3 (3-4) (2007)
Byron Cook, Roberto Sebastiani
Preface to Special Issue on Satisfiability Modulo Theories. J. Satisf. Boolean Model. Comput. 3 (1-2) (2007)
Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi
Property-Driven Partitioning for Abstraction Refinement. TACAS (2007)
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. SAT (2007)
Roberto Sebastiani
From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain. FroCoS (2007)
Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi
GSTE is partitioned model checking. Formal Methods Syst. Des. 31 (2) (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)
Alessandro Cimatti, Roberto Sebastiani
Building Efficient Decision Procedures on Top of SAT Solvers. SFM (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)
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani
). LPAR (2006)
Roberto Sebastiani, Michele Vescovi
Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ALC. SAT (2006)
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. Electron. Notes Theor. Comput. Sci. 144 (2) (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) (2006)
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
The MathSAT 3 System. CADE (2005)

Roberto Sebastiani.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Roberto Sebastiani