Roberto Sebastiani - publication list
Here you can get pdf versions of my publications. Inside each group,
the papers are listed in reverse chronological order.
See also
my personal pages at Google
Scholar Citations,
or at
Scopus,
or at
Microsoft Academic Search,
or at
DBLP,
or at
Research.com
Edited Journal Special Issues:
Papers in Journals:
- Jingwen Ding, Giuseppe Spallitta, Roberto Sebastiani.
"Effective Prime Factorization via Quantum Annealing by Modular Locally-structured Embedding"
.
Nature Scientific Reports. Vol. 14, n. 3518. February 2024.
DOI:https://doi.org/10.1038/s41598-024-53708-7
Tejasri Gururaj, a scientific
journalist of
Phys.org, dedicated to this paper the article
"Quantum annealers and the future of prime factorization".
- Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea
Passerini, Roberto Sebastiani.
"Enhancing SMT-based Weighted Model Integration by Structure Awarenes"
.
Artificial Intelligence. In print. Published online as vol 328, 2024.
DOI: https://doi.org/10.1016/j.artint.2024.104067.
-
Patrick Trentin, Roberto Sebastiani
"Optimization Modulo the Theories of Signed Bit-Vectors and
Floating-Point
Numbers".
Journal of Automated Reasoning -
JAR, 65(7), p. 1071-1096, September 2021.
DOI: https://doi.org/10.1007/s10817-021-09600-4
-
Zhengbing Bian, Fabian Chudak, William Macready, Aidan Roy, Roberto Sebastiani, Stefano Varotti
"Solving SAT (and MaxSAT) with a Quantum Annealer: Foundations, Encodings, and a
Preliminary Report".
Information and Computation, vol 275, December 2020.
Available online at https://doi.org/10.1016/j.ic.2020.104609
-
Roberto Sebastiani, Patrick Trentin
"OptiMathSAT: A Tool for Optimization Modulo Theories".
Journal of Automated Reasoning -
JAR, 2018. Springer.
Issue 3, 2020.
DOI:
https://doi.org/10.1007/s10817-018-09508-6
-
Paolo Morettin, Andrea Passerini, Roberto Sebastiani
"Advanced SMT Techniques for
Weighted Model Integration".
Artificial Intelligence. Volume 275, October 2019.
DOI:
https://doi.org/10.1016/j.artint.2019.04.003
-
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri,
Roberto Sebastiani
"Incremental Linearization for Satisfiability and Verification Modulo Nonlinear
Arithmetic and Transcendental Functions".
ACM Transactions on Computational Logics.
Volume 19 Issue 3, Article 19. August 2018
-
Mai Chi Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
"Multi-Objective Reasoning with Constrained Goal Models".
Requirements Engineering. Volume 23, Issue 2, pp 189-225, 2018.
-
Stefano Teso, Roberto Sebastiani, Andrea Passerini
"Structured Learning Modulo Theories".
Artificial Intelligence. Vol 244, March 2017, P. 166-187.
-
Roberto Sebastiani and Silvia Tomasi
"Optimization Modulo Theories with Linear Rational Costs".
ACM Transactions on Computational Logics (TOCL).
Volume 16, Issue 2, March 2015.
-
Alberto Griggio, Thi Thieu Hoa Le, and Roberto Sebastiani
"Efficient Interpolant Generation in Satisfiability Modulo Linear
Integer Arithmetic".
Logical Methods in Computer Science, Volume 8, Issue 3, 2012.
-
Alessandro Cimatti, Alberto Griggio and Roberto Sebastiani
"Computing Small Unsatisfiable Cores in Satisfiability Modulo
Theories".
Journal of Artificial Intelligence Research, JAIR. Volume 40, pages
701-728, April 2011.
-
Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi
"Symbolic Systems, Explicit Properties: on Hybrid Approaches for
LTL Symbolic Model Checking".
International Journal on Software Tools for Technology Transfer (STTT)
© Springer. 2011.
Volume 13, Number 4, 319-335, DOI:
10.1007/s10009-010-0168-4. Available at
Springerlink
-
Alessandro Cimatti, Alberto Griggio and Roberto Sebastiani
"Efficient Interpolant Generation in Satisfiability Modulo
Theories".
ACM Transaction on Computational Logics, TOCL, vol. 12, number 1, October 2010.
Available from
ACM
Digital Library
-
Roberto Sebastiani and Michele Vescovi
"Automated Reasoning
in Modal and Description Logics via SAT Encoding: the Case Study of
K(m)/ALC-Satisfiability".
Journal of Artificial Intelligence Research, JAIR.
Volume 35, June 2009
-
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio, Roberto Sebastiani
"Delayed Theory Combination vs. Nelson-Oppen
for Satisfiability Modulo Theories:
a Comparative Analysis.".
Annals of Mathematics and Artificial Intelligence, 55(1-2), pp. 63-99,
February 2009.
Ed. Springer.
-
Roberto Sebastiani
"Lazy Satisfiability Modulo Theories".
Journal on Satisfiability, Boolean Modeling and Computation, JSAT.
Vol. 3, Number 3-4, 2007. Pag 141--224, © IOS Press.
DOI: 10.3233/SAT190034
-
Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Vardi
"GSTE is partitioned Model Checking".
Formal Methods in System Design. 31, 2007. pp. 177--196
© Kluwer.
-
Marco Bozzano,
Roberto Bruttomesso,
Alessandro Cimatti,
Tommi Junttila,
Peter van Rossum,
Silvio Ranise,
Roberto Sebastiani
"Efficient Theory Combination via Boolean Search".
Information and Computation. 204(10), 2006. © Elsevier.
-
Marco Bozzano,
Roberto Bruttomesso,
Alessandro Cimatti,
Tommi Junttila,
Peter van Rossum,
Stephan Schulz,
Roberto Sebastiani
"MathSAT: A Tight Integration of SAT and Mathematical Decision Procedure".
Journal of Automated Reasoning. © Kluwer.
Volume 35, Numbers 1-3 / October, 2005.
-
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Zyiad Hanna, Amit Palti,
Zurab Kashidashvili, Roberto Sebastiani
"Encoding RTL Constructs for MathSAT: a Preliminary Report".
Electronic Notes on Theoretical Computer Science, Volume 144, issue 2,
2006. Ed. Elsevier.
- Paolo Giorgini, John Mylopoulous, Roberto Sebastiani
"Goal-Oriented Requirements Analysis and Reasoning in the Tropos
Methodology".
Engineering Application of Artificial Intelligence Journal (EAAI)). Volume
18/2, March 2005.
©
Elsevier.
Awarded by Elsevier "EAAI Top-Cited Article 2005-2010".
-
Gilles Audemard, Marco Bozzano, Roberto Sebastiani, Alessandro Cimatti .
"Verifying Industrial Hybrid Systems with MathSAT."
Electronic Notes on Theoretical Computer Science, Volume 119, issue 4,
2004. Ed. Elsevier.
-
Paolo Giorgini, Eleonora Nicchiarelli, John Mylopoulous, Roberto Sebastiani
"Formal Reasoning Techniques for Goal
Models".
Journal of Data Semantics. Vol 1,
October 2003.
©
Springer.
-
Peter F. Patel-Schneider, Roberto Sebastiani
"A New General Method to Generate Random Modal Formulae for Testing
Decision Procedures".
Journal of Artificial Intelligence Research, (JAIR), Vol. 18, p. 351-389,
May 2003. © Morgan Kaufmann.
-
Fausto Giunchiglia, Roberto Sebastiani
"Building decision procedures for modal logics from propositional
decision procedures - the case study of modal K(m)".
Information
and Computation. Vol 162 (1/2), pages. 158--178,
October/November 2000, © Academic Press.
A longer version is published as
ITC-IRST Technical Report 9611-06, 1996.
-
Ian Horrocks, Peter F. Patel-Schneider, Roberto Sebastiani
"An Analysis of Empirical Testing for Modal Decision
Procedures".
"Logic Journal of the IGPL".
Volume 8, Issue 3: May 2000. pp. 293--323. © Oxford Press.
-
Enrico Giunchiglia,
Fausto Giunchiglia,
Roberto Sebastiani,
Armando Tacchella
"SAT vs. Translation Based decision procedures for modal logics:
a comparative evaluation". ITC-IRST technical report 9812-65.
December 1998.
Published on
"Journal of Applied Non-Classical Logics". , vol. 10, n. 2, 2000,
pages 145--172.
© Hermes International, Oxford.
-
Alan Bundy, Fausto Giunchiglia, Roberto Sebastiani, Toby Walsh
"Calculating Criticalities".
Artificial Intelligence. Volume 88, Issue 1-2, pages 39-67.
December 1996. © Elsevier.
-
Roberto Sebastiani
"Applying GSAT To Non-Clausal Formulas".
Journal of
Artificial Intelligence Research (JAIR), Vol. 1 p. 309-314, January 1994.
© Morgan Kaufmann.
-
Roberto Sebastiani
"Astrazione: dalla Teoria alla Realizzazione di un
Abstract Proof Checker".
(Abstraction: from the theory to the
mechanization of an Abstract Proof Checker). In "AI*IA
Notizie", 2:41-53, June 1993. © Seiss-Romoli. In italian.
Book Chapters:
-
Paolo Giorgini, John Mylopoulous, Roberto Sebastiani
"Goal Modelling and Reasoning in TROPOS".
Social Modeling for Requirements Engineering. January 2011.
MIT press.
-
Roberto Sebastiani, Armando Tacchella
"SAT Techniques for Modal and Description Logics".
Part II, Chapter 32,
The Handbook of Satisfiability , Second Edition, 2021.
IOS press.
-
Clark Barrett, Roberto Sebastiani, Sanjit Seshia, Cesare Tinelli
"Satisfiability Modulo Theories".
Part II, Chapter 33,
The Handbook of Satisfiability, Second Edition, 2021.
IOS press.
-
Alessandro Cimatti, Roberto Sebastiani.
"Building Efficient Decision Procedures on top of SAT
solvers."
In 6th International School on Formal Methods for the Design of
Computer, Communication and Software Systems: Hardware
Verification, 2006.
LNCS, No 3965 © Springer.
Edited Archival Conference Proceedings:
-
Didier Galmiche, Stephan Schulz, Roberto Sebastiani, Editors
9th International Joint Conference on Automated Reasoning, IJCAR 2018
,
Held as Part of the Federated Logic Conference, FloC 2018; Oxford; United Kingdom, Vol. 10900, LNAI/LNCS series,
July 2018. © Springer.
-
Alessandro Cimatti, Roberto Sebastiani, Editors
Theory and Applications of Satisfiability Testing - SAT 2012,
15th International Conference. Vol. 5749, LNCS series,
July 2012. © 7317, Springer.
-
Silvio Ghilardi, Roberto Sebastiani, Editors
Frontiers of Combining Systems Proc. of 7th
International Symposium - FroCoS'09. Vol. 5749, LNCS/LNAI series,
September 2009. © Springer.
-
Byron Cook, Roberto Sebastiani, Editors
"Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006) ".
Electronic Notes
in Theoretical Computer Science, Vol 174, (8)
June 1007, © Elsevier.
Papers in Archival Conference Proceedings:
-
Giuseppe Spallitta, Roberto Sebastiani, Armin Biere
"Disjoint Partial Enumeration Without Blocking
clauses".
In proc. 38th AAAI Conference on Artificial Intelligence
(AAAI-24). February 2024.
-
Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani
"On CNF Conversion for Disjoint SAT Enumeration".
26th International Conference on Theory and
Applications of Satisfiability Testing -- SAT'23. 2023.
LIPICS Series, Dagstuhl Publishing.
-
Enrico Lipparini, Alessandro Cimatti, Alberto Griggio and Roberto
Sebastiani
"Handling Polynomial and Transcendental Functions in SMT via
Unconstrained
Optimisation and Topological Degree Test"
.
Proc. of 20th International
Symposium on Automated Technology for Verification and Analysis -
ATVA22.
LNCS , © Springer.
- Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea
Passerini, Roberto Sebastiani.
"SMT-based Weighted Model Integration with Structure Awareness"
.
Proc 38th Conference on Uncertainty in Artificial
Intelligence (UAI 2022)
LNCS .
-
Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan,
Martin Jonas, Marco Roveri, Roberto Sebastiani, Patrick Trentin
"Optimization Modulo Non-Linear Arithmetic via Incremental Linearization"
.
In proc. FroCoS 2021 - The 13th International Symposium on Frontiers
of Combining Systems
LNCS , © Springer.
-
Sibylle Moehle, Roberto Sebastiani, Armin Biere
"Four Flavors of Entailment".
23rd International Conference on Theory and
Applications of Satisfiability Testing -- SAT'20. 2020.
-
Francesco Contaldo, Patrick Trentin, Roberto Sebastiani
"From MiniZinc to Optimization Modulo Theories, and Back".
17th International
Conference on the Integration of Constraint Programming, Artificial
Intelligence, and Operations Research -- CPAIOR'20. 2020.
-
Samuel Kolb, Paolo Morettin, Pedro Zuidberg, Francesco Sommavilla, Andrea
Passerini, Roberto Sebastiani, Luc De Raedt
"The pywmi Framework and Toolbox for Probabilistic Inference using Weighted
Model Integration".
Proc. International Joint Conference on
Artificial Intelligence. Macao, China, July 2019.
-
Patrick Trentin, Roberto Sebastiani
"Optimization Modulo the Theory of Floating-Point Numbers".
In proc.
he 27th International Conference on Automated Deduction - CADE-27. 2019. LNAI/LNCS, Springer.
-
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri,
Roberto Sebastiani
"Incremental Linearization: A practical approach to
Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions".
In proc.
20th International Symposium on Symbolic and Numeric Algorithms for
Scientific Computing, SYNASC'18. Invited paper.
-
Evellin Cardoso, Jennifer Horkoff, Roberto Sebastiani and John Mylopoulos
"Planning with Strategic Goals".
In proc. 22nd IEEE Enterprise Distributed Object Computing Conference, EDOC 2018.
© IEEE.
-
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri,
Roberto Sebastiani
"Experimenting on Solving Nonlinear Integer Arithmetic with
Incremental Linearization".
In proc. Int. Conference on Theory and Applications of Satisfiability Testing - SAT 2018.
LNCS, © Springer.
-
Zhengbing Bian, Fabian Chudak, William Macready, Aidan Roy, Roberto Sebastiani, Stefano Varotti
"Solving SAT and MaxSAT with a Quantum Annealer: Foundations and a
Preliminary Report".
In proc. FroCoS 2017 - The 11th International Symposium on Frontiers
of Combining Systems
LNCS , © Springer.
-
Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
"Modeling and Reasoning on Requirements Evolution with Constrained
Goal Models".
In proc. SEFM 2017 - The 15th International Conference on Software
Engineering and Formal Methods
LNCS , © Springer.
-
Paolo Morettin, Andrea Passerini, Roberto Sebastiani
"Efficient Weighted Model
Integration via SMT-Based Predicate Abstraction".
In proc. Int. Joint Conference on Artificial Intelligence, IJCAI,
2017.
-
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri,
Roberto Sebastiani
"Satisfiability Modulo Transcendental Functions via Incremental
Linearization".
In proc. Int. Conference on Automated Deduction, CADE, 2017.
LNCS, © Springer.
-
Roberto Sebastiani, Patrick Trentin
"On Optimization Modulo Theories, MaxSMT and Sorting Networks".
In proc. Tools and Algorithms for the Construction and
Analysis of
Systems, TACAS'17, 2017.
LNCS, volume 10205, © Springer.
-
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri,
Roberto Sebastiani
"Invariant Checking of NRA Transition Systems via Incremental Reduction to
LRA with EUF".
In proc. Tools and Algorithms for the Construction and
Analysis of
Systems, TACAS'17, 2017.
LNCS, volume 10205, © Springer.
-
Chi Mai Nguyen, Roberto Sebastiani, Paolo Giorgini, John Mylopoulos
"Requirements Evolution and Evolution Requirements with Constrained Goal Models".
In proc. ER 2016 - International Conference on Conceptual Modeling.
2016.
LNAI , © Springer.
-
Roberto Sebastiani
"Colors Make Theories Hard".
In proc. IJCAR 2016 - International Joint Conference on Automated Reasoning.
2016.
LNCS , volume 9706, © Springer.
-
Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri,
Roberto Sebastiani
"Verilog2SMV: A Tool for Word-level Verification".
In proc. Design, Automation and Test in Europe, DATE 2016.
-
Roberto Sebastiani, Patrick Trentin
"OptiMathSAT: A Tool for Optimization Modulo Theories".
In proc. International Conference on Computer-Aided
Verification, CAV 2015. Part I, LNCS, volume 9206, Springer.
(extended
versi\
on)
-
Roberto Sebastiani and Patrick Trentin
"Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions.".
In proc. Tools and Algorithms for the Construction and
Analysis of
Systems, TACAS'15, 2015. London, UK, April 2015. LNCS, volume 9035, Springer.
(extended
version)
-
Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani
"A Modular Approach to MaxSAT Modulo Theories".
In proc. International Conference on Theory and Applications of
Satisfiability Testing, SAT 2013. Helsinki, Finland, July 2013.
LNCS, volume 7962, © Springer.
-
Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani
"The MathSAT 5 SMT Solver".
In proc. Tools and Algorithms for the Construction and
Analysis of
Systems, TACAS'13. 2013.
LNCS , volume 7795 © Springer.
-
Roberto Sebastiani and Silvia Tomasi
"Optimization in SMT with LA(Q) Cost Functions".
In proc. IJCAR 2012 - International Joint Conference on Automated Reasoning.
2012.
LNAI , volume 7795 © Springer.
-
Alberto Griggio, Quoc-Sang Phan, Silvia Tomasi, and Roberto Sebastiani
"Stochastic Local Search for SMT: Combining
Theory Solvers with WalkSAT".
In proc. FroCoS 2011 - 8th International Symposium on Frontiers of
Combining Systems.
2011.
LNAI 6989, © Springer.
-
Volker Haarslev, Roberto Sebastiani and Michele Vescovi
"Automated Reasoning in ALCQ via SMT".
In proc. International Conference on Automated Deduction,
CADE'11.
2011.
, © Springer.
-
Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani
"Efficient Interpolant Generation in Satisfiability Modulo Linear Integer
Arithmetic".
In proc. Tools and Algorithms for the Construction and
Analysis of
Systems, TACAS'11. 2011.
LNCS 6605, © Springer.
Nominated for the
Best Paper Award at TACAS'11.
-
Anders Franzen, Alessandro Cimatti, Alexander Nadel, Roberto
Sebastiani, Jonathan Shalev
"Applying SMT in Symbolic Execution of Microcode"
In proc. Int. Conference on Formal Methods in Computer Aided Design
(FMCAD'10). Lugano, Switzerland, October 2010.
Winner of the
Best Paper Award at FMCAD'10
(motivations)
-
Alessandro Cimatti, Anders Franzen, Alberto Griggio,
Roberto Sebastiani, and Cristian Stenico
"Satisfiability Modulo the Theory of Costs:
Foundations and Applications"
In proc. Tools and Algorithms for the Construction and
Analysis of
Systems, TACAS'10. 2010.
Remark
The
extended version of the paper contains the proofs of the statements.
-
Dirk Beyer, Alessandro Cimatti, Alberto Griggio, Erkan Keremoglu,
Roberto Sebastiani
"Software Model Checking via Large-Block Encoding."
In proc. Int. Conference on Formal Methods in Computer Aided Design
(FMCAD'09). Austin, TX, USA, November 2009.
-
Alessandro Cimatti, Alberto Griggio,
Roberto Sebastiani
"Interpolant Generation for UTVPI".
In proc. International Conference on Automated Deduction,
CADE'09. Montreal, Canada, August 2009.
LNAI 5663, © Springer.
-
Roberto Sebastiani, Michele Vescovi
"Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis".
In proc. International Conference on Automated Deduction,
CADE'09. Montreal, Canada, August 2009.
LNAI 5663, © Springer.
-
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio,
Roberto Sebastiani
"The MathSAT 4 SMT solver".
In proc. International Conference on
Computer-Aided Verification, CAV 2008. July 2008, Princeton, USA.
LNCS, © Springer.
-
Alessandro Cimatti, Alberto Griggio and Roberto Sebastiani
"Efficient Interpolant Generation in Satisfiability Modulo Theories".
In proc. Tools and Algorithms for the Construction and Analysis of
Systems, TACAS'08.
29 March-6 April, 2008, Budapest, Hungary.
LNCS 4963, © Springer.
An extended version is
DIT technical report DIT-07-075.
-
Roberto Sebastiani
"From KSAT to Delayed Theory Combination:
Exploiting DPLL Outside the SAT Domain".
Invited Lecture.
In proc. FroCoS 2007 - 6th International Symposium on Frontiers of Combining Systems
Liverpool, UK, September 10-12 2007.
LNAI, volume 4720, © Springer.
-
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen,
Alberto Griggio, Zyiad Hanna, Alexander Nadel, Amit Palti and Roberto Sebastiani
"A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification
Problems".
In proc. International Conference on
Computer-Aided Verification, CAV 2007. July 2007, Berlin.
LNCS, volume 4590, © Springer.
-
Alessandro Cimatti, Alberto Griggio and Roberto Sebastiani
"A Simple and Flexible Way of Computing Small Unsatifiable Cores in Satisfiability Modulo Theories".
In proc. Tenth International Conference on
Theory and Applications of Satisfiability Testing, SAT 2007.
May 28 - 31 2007, Lisbon, Portugal.
LNCS, volume 4501, © Springer.
-
Roberto Sebastiani, Stefano Tonetta, and Moshe Y. Vardi
"Property-Driven Partitioning for Abstraction Refinement".
In proc. Thirteenth International Conference on
Tools and Algorithms for the Construction
and Analysis of Systems - TACAS'07.
LNCS n. 4424, © Springer.
-
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio,
Roberto Sebastiani
"Delayed Theory Combination vs. Nelson-Oppen
for Satisfiability Modulo Theories:
a Comparative Analysis.".
In proc. 13th Int. Conference on Logics in Programming, Artificial Intelligence and Reasoning
(LPAR'06).
Phnom Pehn, Cambodia, 2006
LNAI , volume 4246. © Springer.
-
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio,
Alessandro Santuari, Roberto Sebastiani
"To Ackermann-ize or not to Ackermann-ize?
On Efficiently Handling
Uninterpreted Function Symbols in
SMT(EUF U T )".
In proc. 13th Int. Conference on Logics in Programming, Artificial Intelligence and Reasoning
(LPAR'06).
Phnom Pehn, Cambodia, 2006
LNAI , volume 4246. © Springer.
-
Roberto Sebastiani and Michele Vescovi
"Encoding the satisfiability of modal and description logics into SAT:
the case study of K(m)/ALC".
Short paper.
Proc. 9th International Conference on Theory and Applications of
Satisfiability Testing (SAT'06). Seattle, August 2006.
LNCS , volume 4121. © Springer.
Extended version is
DIT
technical report 1011, June 2006.
-
Marco Bozzano,
Roberto Bruttomesso,
Alessandro Cimatti,
Tommi Junttila,
Peter van Rossum,
Stephan Schulz,
Roberto Sebastiani
"The MathSAT 3 System".
In proc. CADE-20, Int. Conference on Automated Deduction, 2005,
Tallin, Estonia, July 2005.
LNCS, No 3632 © Springer.
-
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, T. Junttila, P. van
Rossum, Silvio Ranise, Roberto Sebastiani
"Efficient Satisfiability Modulo Theories
via Delayed Theory Combination".
In proc. Int. Conf. on Computer-Aided Verification, CAV 2005.
LNCS, No 3576. © Springer.
-
Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi
"Symbolic Systems, Explicit Properties: on Hybrid Approaches for LTL Symbolic Model Checking".
In proc. Int. Conf. on Computer-Aided Verification, CAV 2005.
LNCSS, No 3576 © Springer.
-
Marco Bozzano,
Roberto Bruttomesso,
Alessandro Cimatti,
Tommi Junttila,
Peter van Rossum,
Stephan Schulz,
Roberto Sebastiani
"An Incremental and Layered Procedure for the Satisfiability of Linear
Arithmetic Logic".
In proc. TACAS2005, Tools and Algorithms for the Construction and Analysis of
Systems. Edinburgh, Scotland, April 2005.
LNCS, No 3440. © Springer.
-
Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Vardi
"GSTE is partitioned Model Checking".
In proc. Int. Conf. on Computer Aided Verification, CAV'04.
LNCS No. 3114, 2004. © Springer.
-
Roberto Sebastiani, Paolo Giorgini, John Mylopoulous
"Simple and Minimum-Cost Satisfiability for Goal Models".
June 2004. Proc. Int. conference on Advanced Information Systems
Engineering, CAISE'04
LNCS No.3084. © Springer.
-
Roberto Sebastiani, Stefano Tonetta
"``More Deterministic" vs. ``Smaller'' Buechi Automata
for Efficient LTL Model Checking"
In proc. of the 12th Advanced Research Working Conference
on Correct Hardware Design and Verification Methods (CHARME'03).
L'Aquila, Italy, October 2003.
LNCS No. 2860
©
Springer.
-
Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani
"Bounded Model Checking for Timed Systems."
In Proc. 22nd Joint International Conference on Formal
Techniques for Networked and Distributed Systems (FORTE 2002).
Houston, TX, USA, November 2002.
.
LNCS
©
Springer. Also ITC-IRST Technical report 0201-05.
January 2002.
-
Paolo Giorgini, Eleonora Nicchiarelli, John Mylopoulous, Roberto Sebastiani
"Reasoning with Goal Models".
In Proc. "Int. Conference of Conceptual Modeling -- ER2002"
Tampere, Finland, October 2002.
.
LNCS n. 2503 ©
Springer.
-
Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore,
Marco Roveri, Roberto Sebastiani, Armando Tacchella
"NuSMV 2: An OpenSource Tool for Symbolic Model Checking".
In Proc. "Int. Conference of Computer-Aided verification, CAV'02"
Copenhagen, Denmark, 2002.
.
LNCS N.2404 ©
Springer.
-
Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani
"A SAT Based Approach for Solving Formulas over
Boolean and Linear Mathematical Propositions".
In Proc. 18th "Int. Conference of Automated Deduction, CADE'02."
LNAI N.2392 ©
Springer.
Also ITC-IRST technical report n. 0205-03.
-
Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani
"Integrating Boolean and Mathematical Solving:
Foundations, Basic Algorithms and Requirements".
In "Artificial Intelligence, Automated Reasoning, and Symbolic Computation. Proc.
of Joint AISC 2002 and Calculemus 2002." Marseille, France, 2002.
LNAI N.2385 ©
Springer.
-
Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco
Roveri, Roberto Sebastiani, Armando Tacchella
"Integrating BDD-based and SAT-based Symbolic Model Checking".
In Proc. ``Frontiers of
Combining Systems, FROCOS'02''.
Santa Margherita, Italy, 2002.
LNAI , N.2309 © Springer.
-
Alessandro Cimatti, Marco Pistore, Marco
Roveri, Roberto Sebastiani
"Improving the Encoding of LTL Model Checking into SAT".
In Proc. "3rd International Workshop on Verification, Model Checking, and Abstract
Interpretation, VMCAI'02". Venice, Italy, 2002.
LNCS , N.2294 © Springer.
-
Peter F. Patel-Schneider, Roberto Sebastiani
"A System and Methodology for Generating Random Modal Formulae".
IJCAR-2001, International Joint Conference on Automated reasoning.
Siena, Italy, July 2001.
LNAI , N.2083 © Springer
-
Roberto Sebastiani, Alessandro Tomasi, Fausto Giunchiglia
"Model Checking Syllabi and Student Careers".
TACAS2001, Tools and Algorithms for the Construction and Analysis of
Systems
Genova, Italy, April 2001.
LNCS , N. 2031 © Springer
-
Fausto Giunchiglia, Roberto Sebastiani, Paolo Traverso
"Integrating SAT solvers with domain-specific reasoners".
Symbolic Computation and Automated Reasoning, St. Andrews, Scotland, UK, August 2000.
© A.K. Peters Eds.
-
Enrico Giunchiglia, Roberto Sebastiani
"Applying the Davis-Putnam procedure to non-clausal formulas".
AI*IA'99, Italian National Conference on Artificial
Intelligence. Bologna, Italy, September 1999.
LNAI , N.1792 © Springer
Also IRST Technical Report 9904-09, Istituto Trentino di Cultura,
April 1999.
-
Alessandro Cimatti,
Pierluigi Pieraccini,
Roberto Sebastiani,
Paolo Traverso,
Adolfo Villafiorita
"Formal specification and validation of a vital protocol".
FM'99 -- World Congress on Formal Methods. Toulouse, France, September 1999.
LNCS, N.1709, © Springer ed.
-
Angelo Chiappini,
Alessandro Cimatti,
Carmen Porzia,
Giovanni Rotondo,
Roberto Sebastiani,
Paolo Traverso,
Adolfo Villafiorita.
"Formal Specification and Development of a Safety-Critical Train Management System".
International Conference Computer Safety, Reliablity
ans Security - SAFECOMP'99. Toulouse, France, September
1999. LNCS, N. 1698, © Springer ed.
-
Roberto Sebastiani, Adolfo Villafiorita
"SAT-based decision procedures for normal modal logics:
a theoretical framework".
"6th International Conference on
Artificial Intelligence: Methodology, Systems, Applications - AIMSA'98"
LNAI N. 1480, © Springer ed.
Sozopol, Bulgaria, September 1998.
-
Enrico Giunchiglia, Alessandro Massarotto, Roberto Sebastiani
"Act, and the rest will follow: exploiting determinism in planning as
satisfiability".
"15th National Conference on Artificial Intelligence" - AAAI98.
Madison, Wisconsin, USA, July 1998.
© AAAI Press ed.
-
Enrico Giunchiglia, Fausto Giunchiglia, Roberto Sebastiani, Armando Tacchella
"More evaluation of decision procedures for modal logics".
"6th International Conference on Principles of Knowledge Representation and Reasoning - KR'98".
© Morgan Kauffman ed.
Trento, Italy, June 1998.
-
Fausto Giunchiglia, Marco Roveri, Roberto Sebastiani
"A new method for testing decision procedures
in modal logics".
"14th International Conference on Automated Deduction"
- CADE14.
LNAI , N.1249, © Springer ed.
Townsville, Australia, July 1997.
-
Fausto Giunchiglia, Roberto Sebastiani
"A SAT-based decision procedure for ALC".
"5th International Conference on Principles of Knowledge Representation and Reasoning - KR'96".
© AAAI Press ed.
Boston, MA, USA, November 1996.
-
Alan Bundy, Fausto Giunchiglia, Roberto Sebastiani, Toby Walsh.
"Computing Abstraction Hierarchies by Numerical Simulation".
"14th National Conference on Artificial Intelligence" - AAAI96. Portland, Oregon, USA, 1996.
AAAI Press ed.
-
Fausto Giunchiglia, Roberto Sebastiani.
"Building decision procedures for modal logics from propositional
decision procedures - the case study of modal K".
"13th International Conference on Automated Deduction"
- CADE13.
LNAI , N.1104, © Springer ed.
New Brunswick, New Jersey, USA, 1996.
-
Fausto Giunchiglia, Roberto Sebastiani, Adolfo Villafiorita, Toby Walsh.
"A General Purpose Reasoner for Abstraction".
"Canadian Conference on Artificial Intelligence" - AI96.
LNAI , N.1081, © Springer ed. Toronto, Canada, 1996.
-
Roberto Sebastiani, Adolfo Villafiorita and Fausto Giunchiglia
"Proving Theorems by Using Abstraction Interactively".
In "Trends in Theoretical Informatics", Innsbruk, 1996.
© Die Deutsche Bibliothek Ed.
Edited Non-Archival Conference Proceedings:
Theses:
DISCLAIMER:
The documents distributed in this page have been provided by the
contributing authors as a means to ensure timely
dissemination of scholarly and technical work on a noncommercial
basis. Copyright and all rights therein are maintained by the
authors or by other copyright holders, notwithstanding that they have
offered their works here electronically. It is understood that
all persons copying this information will adhere to the terms and
constraints invoked by each author's copyright. These works may
not be reposted without the explicit permission of the copyright holder.
The copyright holder of papers published either on journals or on conference
proceedings is the
publisher of the journal/proceedings.
The documents distributed by this server are the author's personal
copies of pre-prints of such papers.
Back to
Roberto Sebastiani's home page.