Research Outputs Roberto Sebastiani


  • Morettin, Paolo; Passerini, Andrea; Sebastiani, Roberto, "Efficient Weighted Model Integration via SMT-Based Predicate Abstraction" in Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, Melbourne: International Joint Conferences on Artificial Intelligence, 2017, p. 720-728. - ISBN: 9780999241103. Proceedings of: IJCAI, Melbourne, August 2017. - DOI: 10.24963/ijcai.2017/100
  • Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto, "Invariant checking of NRA transition systems via incremental reduction to LRA with EUF" in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Uppsala: Springer Verlag, 2017, p. 58-75. - (LECTURE NOTES IN COMPUTER SCIENCE). - ISBN: 9783662545768. Proceedings of: 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, swe, 2017. - URL: http://springerlink.com/content/0302-9743/copyright/2005/ . - DOI: 10.1007/978-3-662-54577-5_4
  • Nguyen, Chi Mai; Sebastiani, Roberto; Giorgini, Paolo; Mylopoulos, John, "Modeling and reasoning on requirements evolution with constrained goal models" in Software Engineering and Formal Methods, Svizzera: Springer Verlag, 2017, p. 70-86. - ISBN: 978-3-319-66196-4. Proceedings of: 15th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2017, Trento, Italy, 2017. - URL: http://springerlink.com/content/0302-9743/copyright/2005/ . - DOI: 10.1007/978-3-319-66197-1_5
  • Sebastiani, Roberto; Trentin, Patrick, "On Optimization Modulo Theories, MaxSMT and Sorting Networks" in Tools and Algorithms for the Construction and Analysis of Systems, Berlin: Springer, 2017. - (LECTURE NOTES IN COMPUTER SCIENCE). Proceedings of: TACAS, Uppsala, Sweden, 22-29 / 04 / 2017. - URL: https://arxiv.org/abs/1702.02385
  • Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto, "Satisfiability Modulo Transcendental Functions via Incremental Linearization" in Automated Deduction – CADE 26, Berlin, Germany: Springer, 2017, p. 95-113. - ISBN: 978-3-319-63045-8. Proceedings of: International Conference on Automated Deduction (CADE), Gothenburg, 8-11 August 2017. - DOI: 10.1007/978-3-319-63046-5_7
  • Bian, Zhengbing; Chudak, Fabian; Macready, William; Roy, Aidan; Sebastiani, Roberto; Varotti, Stefano, "Solving SAT and MaxSAT with a quantum annealer: Foundations and a preliminary report" in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Svizzera: Springer Verlag, 2017, p. 153-171. - (lecture notes in computer science; 10483). - ISBN: 9783319661667. Proceedings of: 11th International Symposium on Frontiers of Combining Systems, FroCoS 2017, Brasilia, 2017. - URL: http://springerlink.com/content/0302-9743/copyright/2005/ . - DOI: 10.1007/978-3-319-66167-4_9
  • Sebastiani, Roberto, "Colors make theories hard" in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), London: Springer Verlag, 2016, p. 152-170. - (LECTURE NOTES IN COMPUTER SCIENCE). - ISBN: 9783319402284. Proceedings of: 8th International Joint Conference on Automated Reasoning, IJCAR 2016, Coimbra, Portugal, 2016. - URL: http://springerlink.com/content/0302-9743/copyright/2005/ . - DOI: 10.1007/978-3-319-40229-1_11
  • Nguyen, Chi Mai; Sebastiani, Roberto; Giorgini, Paolo; Mylopoulos, John, "Multi-objective reasoning with constrained goal models" in REQUIREMENTS ENGINEERING, v. 2016, (2016), p. 1-37. - URL: http://www.springeronline.com/sgw/cda/frontpage/0,11855,5-40007-70-1116135-0,00.html . - DOI: 10.1007/s00766-016-0263-5
  • Nguyen, Chi Mai; Sebastiani, Roberto; Giorgini, Paolo; Mylopoulos, John, "Requirements evolution and evolution requirements with constrained goal models" in Conceptual Modeling, London: Springer International Publishing, 2016, p. 544-552. - (LECTURE NOTES IN COMPUTER SCIENCE). Proceedings of: Conceptual Modeling ER 2016, 2016, Gifu, Japan, November 14-17. - URL: http://springerlink.com/content/0302-9743/copyright/2005/ . - DOI: 10.1007/978-3-319-46397-1_42
  • Irfan, Ahmed; Cimatti, Alessandro; Griggio, Alberto; Roveri, Marco; Sebastiani, Roberto, "Verilog2SMV: A tool for word-level verification" in Proceedings of the 2016 Design, Automation and Test in Europe Conference and Exhibition, DATE 2016, Dresden: Institute of Electrical and Electronics Engineers Inc., 2016, p. 1156-1159. - ISBN: 9783981537062. Proceedings of: 19th Design, Automation and Test in Europe Conference and Exhibition, DATE 2016, International Congress Centre Dresden (ICC), deu, 2016
  • Teso, Stefano; Sebastiani, Roberto; Passerini, Andrea, "Constructive Learning Modulo Theories" in ICML Workshop on Constructive Machine Learning, Arxiv: Arxiv, 2015. Proceedings of: ICML Workshop on Constructive Machine Learning, Lille, France, July 10, 2015. - URL: papers/cml2015lmt.pdf
  • Sebastiani, Roberto; Trentin, Patrick, "OptiMathSAT: A Tool for Optimization Modulo Theories" in Proceedings International Conference on Computer-Aided Verification, CAV 2015, Berlin: Springer, 2015, p. 447-454. - (LECTURE NOTES IN COMPUTER SCIENCE). - ISBN: 978-3-319-21689-8. Proceedings of: International Conference on Computer-Aided Verification, CAV, San Francisco, CA, USA, July 18-24, 2015. - DOI: 10.1007/978-3-319-21690-4_27
  • R. Sebastiani;S. Tomasi, "Optimization Modulo Theories with Linear Rational Costs" in ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, v. 2015, n. 16, 2 (2015), p. 1-12:1. - URL: http://dl.acm.org/citation.cfm?doid=2699915 . - DOI: 10.1145/2699915
  • Sebastiani, Roberto; Trentin, Patrick, "Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions" in In proc. Tools and Algorithms for the Construction and Analysis of Systems, Berlin: Berlin: Springer-Verlag, 2015, p. 335-349. - (LECTURE NOTES IN COMPUTER SCIENCE). Proceedings of: TACAS 2015, London, UK, Apr 11, 2015 - Apr 19, 2015. - DOI: 10.1007/978-3-662-46681-0_27
  • Teso, Stefano; Sebastiani, Roberto; Passerini, Andrea, "Structured learning modulo theories" in ARTIFICIAL INTELLIGENCE, v. 2015, (2015). - URL: http://www.sciencedirect.com . - DOI: 10.1016/j.artint.2015.04.002
  • A. Cimatti; A. Griggio; B. Joost Schaafsma; R. Sebastiani, "A Modular Approach to MaxSAT Modulo Theories" in Theory and Applications of Satisfiability Testing – SAT 2013, Berlin: Springer: Berlin, Heidelberg, 2013, p. 150-165. - ISBN: 9783642390708. Proceedings of: SAT 2013, Helsinki, 8-12 July 2013. - DOI: 10.1007/978-3-642-39071-5_12
  • A. Cimatti; A. Griggio; B. Joost Schaafsma; R. Sebastiani, "The MathSAT 5 SMT Solver" in Tools and Algorithms for the Construction and Analysis of Systems, Berlin: Berlin: Springer-Verlag, 2013, p. 93-107. - ISBN: 9783642367410. Proceedings of: TACAS'13. 2013, ROME, 16-24 March 2013. - DOI: 10.1007/978-3-642-36742-7_7
  • A. Griggio; T. T. H. Le; R. Sebastiani, "Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic" in LOGICAL METHODS IN COMPUTER SCIENCE, v. 8, n. 3 (2012), p. 1-31. - DOI: 10.2168/LMCS-8 (3:03) 2012
  • R. Sebastiani; S. Tomasi, "Optimization in SMT with LA(Q) Cost Functions" in Proceeding IJCAR'12, Berlin: Springer-Verlag, 2012, p. 484-498. - ISBN: 9783642313646. Proceedings of: IJCAR'12, Manchester, June 26th to July 1st, 2012. - DOI: 10.1007/978-3-642-31365-3_38
  • A. Cimatti; R. Sebastiani (edited by), "Theory and Applications of Satisfiability Testing - SAT 2012- 15th International Conference.", by A. Cimatti, R. Sebastiani, Berlin: Springer, 2012, 364 p. - (LNCS). - ISBN: 9783642316111. - DOI: 10.1007/978-3-642-31612-8
  • V. Haarslev; R. Sebastiani; M. Vescovi, "Automated Reasoning in ALCQ via SMT" in In proc. International Conference on Automated Deduction, Berlin: Springer, 2011, p. 283-298. - (LNCS). Proceedings of: CADE 2011, WROCLAW, 31 JULY - 5 AUGUST. - DOI: 10.1007/978-3-642-22438-6_22
  • A. Cimatti; A. Griggio; R. Sebastiani, "Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories" in THE JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, v. Volume 40, April 2011, (2011), p. 701-728. - DOI: 10.1613/jair.3196
  • A. Griggio; T.T.H. Le; R. Sebastiani, "Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic" in Tools and Algorithms for the Construction and Analysis of Systems: 17th International Conference: TACAS 2011: Held as Part of the Joint European Conferences on Theory and Practice of Software: ETAPS 2011: Proceedings, Berlin: Springer, 2011, p. 143-157. - (Lecture Notes in Computer Science). - ISBN: 9783642198342. Proceedings of: TACAS 2010, Saarbrücken, 26th March-3rd April 2011. - DOI: 10.1007/978-3-642-19835-9
  • A. Griggio; Q.S. Phan; S. Tomasi; R. Sebastiani, "Stochastic Local Search for SMT: Combining Theory Solvers withWalkSAT" in In proc. FroCoS 2011 - 8th International Symposium on Frontiers of Combining Systems, BERLIN: SPRINGER, 2011, p. 163-178. - (LNCS). Proceedings of: FROCOS, Saarbrücken, 5-7 OCTOBER 2011. - DOI: 10.1007/978-3-642-24364-6_12
  • R. Sebastiani; S. Tonetta; M. Y. Vardi, "Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking" in INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, v. Vol. 13, n. N. 4 (2011), p. 319-335. - DOI: 10.1007/s10009-010-0168-4
  • A. Franzen; A. Cimatti; A. Nadel; R. Sebastiani; J. Shalev, "Applying SMT in Symbolic Execution of Microcode" in Formal Methods in Computer Aided Design: FMCAD 2010, Piscataway, NJ: IEEE, 2010, p. 121-128. - ISBN: 9781457707346. Proceedings of: FMCAD 2010, Lugano, 20th-23rd October 2010. - URL: http://fmcad10.iaik.tugraz.at/
  • A. Cimatti; A. Griggio; R. Sebastiani;, "Efficient Interpolant Generation in Satisfiability Modulo Theories" in ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, v. vol. 12, n. 1 (2010), p. 397-412. - URL: http://dl.acm.org/citation.cfm?doid=1838552.1838559 . - DOI: 10.1145/1838552.1838559
  • A. Cimatti, A. Franzen; A. Griggio, R. Sebastiani, C. Stenico, "Satisfiability Modulo the Theory of Costs: Foundations and Applications" in Tools and Algorithms for the Construction and Analysis of Systems, Berlin: Springer, 2010, p. 99-113. - (Lecture Notes in Computer Science). - ISBN: 9783642120015. Proceedings of: 16th International Conference TACAS 2010, Paphos, Cyprus, 20th-28th March 2010. - DOI: 10.1007/978-3-642-12002-2_8
  • R. Sebastiani; Mi. Vescovi, "Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability" in THE JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, v. 35, n. 1 (2009), p. 343-389. - DOI: 10.1613/jair.2675
  • R. Sebastiani; M. Vescovi, "Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis" in Automated Deduction – CADE-22, BERLIN: Springer, 2009, p. 84-99. - (LNCS). - ISBN: 9783642029585. Proceedings of: International Conference on Automated Deduction, CADE-22., Montreal, Canada, August 2009. - DOI: 10.1007/978-3-642-02959-2_6
  • R. Bruttomesso; A. Cimatti; A. Franzen; A. Griggio; R. Sebastiani, "Delayed Theory Combination vs. Nelson-oppen for satisfiability modulo theories: A comparative analysis" in ANNALS OF MATHEMATICS AND OF ARTIFICIAL INTELLIGENCE, v. 55, n. 1-2 (2009), p. 63-99. - URL: http://www.springerlink.com/content/467531nu2526k26j/ . - DOI: 10.1007/s10472-009-9152-7
  • A. Cimatti; A. Griggio; R. Sebastiani, "Interpolant Generation for UTVPI" in Automated Deduction – CADE-22, Berlin: Springer, 2009, p. 167-182. - ISBN: 9783642029585. Proceedings of: International Conference on Automated Deduction, CADE'09., Montreal, Canada, August 2009.. - DOI: 10.1007/978-3-642-02959-2_15
  • R. Sebastiani; A. Tacchella, "SAT Techniques for Modal and Description Logics" in Handbook of Satisfiability, Amsterdam: IOS Press, 2009, p. 781-824. - ISBN: 9781586039295. - DOI: 10.3233/978-1-58603-929-5-781
  • C. Barrett; R. Sebastiani; S. Seshia; C. Tinelli, "Satisfiability Modulo Theories" in Handbook of Satisfiability, AMSTERDAM: IOS Press, 2009, p. 825-885. - ISBN: 9781586039295. - DOI: 10.3233/978-1-58603-929-5-825
  • D. Beyer; A. Cimatti; A. Griggio; E. Keremoglu; R. Sebastiani, "Software Model Checking via Large-Block Encoding." in In Proceedings of the 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009, Austin (TX), November 15-18), 2009. IEEE Computer Society Press, Los Alamitos (CA, LOS ALAMITOS, CA: IEEE Computer Society Press, 2009, p. 25-32. - ISBN: 9781424449668. Proceedings of: 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009), Austin, TX, USA, November 2009. - DOI: 10.1109/FMCAD.2009.5351147
  • A. Cimatti; A. Griggio; R. Sebastiani, "Efficient Interpolant Generation in Satisfiability Modulo Theories" in Tools and Algorithms for the Construction and Analysis of Systems, TACAS'08, Heidelberg: Springer, 2008, p. 397-412. - (LNCS). - ISBN: 9783540787990. Proceedings of: TACAS 2008, Budapest, April 2008. - DOI: 10.1007/978-3-540-78800-3_30
  • R. Bruttomesso ; A. Cimatti ; P. A. M. Franzen ; A. Griggio ; R. Sebastiani, "The MathSAT 4 SMT Solver" in Computer Aided Verification, Heidelberg: Springer, 2008, p. 299-303. - (LNCS). - ISBN: 9783540705437. Proceedings of: CAV 2008, 20th International Conference, Princeton, N.Y., July 2008
  • R. Bruttomesso ; A. Cimatti ; P. A. M. Franzen ; A. Griggio ; Z. Hanna ; A. Nadel ; A. Palti ; R. Sebastiani, "A lazy and layered SMT(BV) solver for hard industrial verification problems" in Computer Aided Verification: 19th International Conference, CAV 2007, Berlin; Heidelberg: Springer, 2007, p. 547-560. - (LNCS). - ISBN: 9783540733676. Proceedings of: CAV 2007, Berlin, 3rd-7th July 2007. - DOI: 10.1007/978-3-540-73368-3_54
  • A. Cimatti; A. Griggio; R. Sebastiani, "A Simple and Flexible Way of Computing Small Unsatifiable Cores in Satisfiability Modulo Theories" in Theory and Applications of Satisfiability Testing, Lisbon: SAT, 2007, p. 334-339. - ISBN: 9783540727873. Proceedings of: SAT 2007, Lisbon, May 2007
  • A. Cimatti ; A. Griggio ; R. Sebastiani, "A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories" in Theory and Applications of Satisfiability Testing - SAT 2007: 10th International Conference, SAT 2007, Lisbon, Portugal, May 28-31, 2007, Proceedings, Berlin: Springer, 2007, p. 334-339. - ISBN: 9783540727873. Proceedings of: SAT 2007, Lisbon, 28th-31th May 2007
  • B. Cook ; R. Sebastiani (Ed. critica a cura di), Combined Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006) and the First International Workshop on Probabilistic Automata and Logics (PaUL 2006), Amsterdam [etc.]: Elsevier, 2007, 108 p. - (ENTCS)
  • R. Sebastiani, "From KSAT to delayed theory combination: exploiting DPLL outside the SAT domain" in Proceedings of the 6th International Symposium on Frontiers of Combining Systems, Berlin; Heidelberg: Springer, 2007, p. 28-46. - (LNAI). - ISBN: 9783540746201. Proceedings of: FroCoS2007, Liverpool, Uk, SEPTEMBER
  • R. Sebastiani ; E. Siengeman ; S. Tonetta ; M. Vardi, "GSTE is partitioned Model Checking" in FORMAL METHODS IN SYSTEM DESIGN, v. 31, n. 2 (2007), p. 177-196. - DOI: 10.1007/s10703-007-0036-3
  • B. Cook; R. Sebastiani (Ed. critica a cura di), Journal on Satisfiability, Boolean Modeling and Computation -- JSAT, Special Issue on Satisfiability Modulo Theories, Amsterdam: IOS Press, 2007. - (Journal on Satisfiability, Boolean Modeling and Computation (JSAT))
  • R. Sebastiani, "Lazy Satisfiability Modulo Theories" in JOURNAL ON SATISFIABILITY, BOOLEAN MODELING AND COMPUTATION, v. 3, n. 4963 (2007), p. 141-224
  • B. Cook; R. Sebastiani (Ed. critica a cura di), Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006), Olanda: ELSEVIER, 2007. - DOI: 10.1016/j.entcs.2006.11.037
  • R. Sebastiani; S. Tonetta; M. Vardi, "Property-Driven Partitioning for Abstraction Refinement" in Thirteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'07, Berlin: Springer, 2007, p. 389-404. - (LNCS). - ISBN: 9783540712084. Proceedings of: TACAS 2007, Braga, Portugal, 24 March - 1 April
  • A. Cimatti ; R. Sebastiani, "Building Efficient Decision Procedures on top of SAT solvers" in ED. Marco Bernardo (edited by), Formal Methods for Hardware Verification: 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006, Bertinoro, Italy, May 22-27, 2006, Advances Lectures, Berlin: Springer, 2006, p. 144-175. - ISBN: 9783540343042. - DOI: 10.1007/11757283_6
  • R. Bruttomesso ; A. Cimatti ; P. A. M. Franzen ; A. Griggio ; R. Sebastiani, "Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis" in Logic for Programming, Artificial Intelligence, and Reasoning13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings, berlin: Springer, 2006, p. 527-541. - (LNCS). - ISBN: 9783540482819. Proceedings of: LPAR 2006, Phnom Penh, Cambodia, 13th-17th November 2006. - URL: http://www.springerlink.com/content/k88k71426m1t0444/fulltext.pdf . - DOI: 10.1007/11916277_36
  • M. Bozzano; R. Bruttomesso; A. Cimatti; T. Junttila; P. Van Rossum; S. Ranise; R. Sebastiani, "Efficient theory combination via Boolean search" in INFORMATION AND COMPUTATION, v. 204, n. 10 (2006), p. 1493-1525. - DOI: 10.1016/j.ic.2005.05.011
  • M. Bozzano ; R. Bruttomesso ; A. Cimatti ; P. A. M. Franzen ; Z. Hanna ; Z. Khasidashvili ; A. Palti ; R. Sebastiani, "Encoding RTL Constructs for MathSAT: a Preliminary Report" in ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, v. 144, n. 2 (2006), p. 3-14. - DOI: 10.1016/j.entcs.2005.12.001
  • R. Sebastiani ; M. Vescovi, "Encoding the satisfiability of modal and description logic into SAT: the case study of K(m)/ALC" in Theory and applications of satisfiability testing - SAT 2006: 9th international conference, Seattle, WA, USA, August 12-15, 2006, proceedings, Berlin, Heidelberg: Springer, 2006, p. 130-135. - (LNCS). - ISBN: 3540372067. Proceedings of: 9th International Conference on Theory and Applications of Satisfiability Testing (SAT'06), Seattle, 12th-15th, August 2006. - URL: http://www.springerlink.com/content/0600054485g52h76/fulltext.pdf . - DOI: 10.1007/11814948_15
  • R. Bruttomesso; A. Cimatti; P. A. M. Franzen; A. Griggio; A. Santuari; R. Sebastiani, "To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT (EUF ÈT)" in Logic for Programming, Artificial Intelligence, and Reasoning: 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings, Berlin/Heidelberg: Springer, 2006, p. 557-571. - (Lecture Notes in Computer Science). - ISBN: 9783540482819. Proceedings of: LPAR 2006, Phnom Penh (Cambodia), 13th-17th November 2006. - URL: http://www.springerlink.com/content/4t1823urk0675361/fulltext.pdf . - DOI: 10.1007/11916277_38
  • M. Bozzano; R. Bruttomesso; A. Cimatti; T. Junttila; P. Van Rossum; R. Sebastiani; S. Schulz, "An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic" in Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2005, Berlin: Springer, 2005, p. 317-333. - (LNCS). - ISBN: 3540253335. Proceedings of: Springer, Edinburgh, Scotland, 2005
  • M. Bozzano ; R. Bruttomesso ; A. Cimatti ; T. Junttila ; P. Van Rossum ; S. Ranise ; R. Sebastiani, "Efficient Satisfiability Modulo Theories via Delayed Theory Combination" in Proceedings of the 17th International Conference on Computer Aided Verification, Berlin; Heidelberg: Springer, 2005, p. 527-541. - (LNCS). - ISBN: 3540272313. Proceedings of: CAV 2005, Edinburgh, Scotland, 2005
  • M. Bozzano; R. Bruttomesso; A. Cimatti; Z. Hanna; A. Palti; Z. Kashidashvili; R. Sebastiani, "Encoding RTL Constructs for MathSAT: a Preliminary Report" in ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, v. 144, n. 2 (2005), p. 3-14
  • P. Giorgini ; J. Mylopoulos ; R. Sebastiani, "Goal-oriented Requirements Analysis and Reasoning in the Tropos Methodology" in ENGINEERING APPLICATIONS OF ARTIFICIAL INTELLIGENCE, v. 18, n. 2 (2005), p. 159-171. - DOI: 10.1016/j.engappai.2004.11.017
  • P. Barbieri; E. Rullani; M. Paiola; R. Sebastiani (edited by), "Intelligenza terziaria motore dell'economia. Alla ricerca dell'Italia che innova", by Barbieri, P., E. Rullani, M. Paiola, R. Sebastiani, Milano: Franco Angeli Editore, 2005. - (Collana T-Lab Laboratorio del Terziario che innova). - ISBN: 9788846468413
  • M. Bozzano; R. Bruttomesso; A. Cimatti; T. Junttila; P. Van Rossum; S. Schulz; R. Sebastiani, "MathSAT: Tight Integration of SAT and Mathematical Decision Procedures" in JOURNAL OF AUTOMATED REASONING, v. 35, n. 1-3 (2005), p. 265-293. - DOI: 10.1007/978-1-4020-5571-3_12
  • R. Sebastiani ; S. Tonetta ; M. Y. Vardi, "Symbolic Systems, Explicit Properties: on Hybrid Approaches for LTL Symbolic Model Checking" in Proceedings of Computer Aided Verification, Berlin Heidelberg: Springer, 2005, p. 350-363. - (LNCS). - ISBN: 3540272313. Proceedings of: CAV 2005, Edinburgh, Scotland, 2005
  • M. Bozzano ; R. Bruttomesso ; T. Junttila ; S. Schulz ; R. Sebastiani ; P. Var Rossum, "The MathSAT 3 System" in Automated Deduction: CADE-20, Berlin: Springer, 2005, p. 315-321. - (LNCS). - ISBN: 3540280057. Proceedings of: CADE 20, Tallin, July 22-27 2005
  • G. Audemard ; M. Bozzano ; A. Cimatti ; R. Sebastiani, "Verifying Industrial Hybrid Systems with MathSAT" in ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, v. 119, n. 2 (2005), p. 17-32. - DOI: 10.1016/j.entcs.2004.12.022
  • R. Sebastiani; E. Singerman; S. Tonetta; M. Y. Vardi, "GSTE is partitioned model checking" in Proceedings on Computer Aided Verification: 16th International Conference, CAV 2004, Heildelberg: Springer, 2004, p. 229-241. - (Lecture notes in computer science). - ISBN: 9783540223429. Proceedings of: 16th international conference on computer aided verification (CAV 2004), Boston, Mass., 13th-17th July 2004
  • R. Sebastiani ; P. Giorgini ; J. Mylopoulos, "Simple and Minimal-Cost Satisfiability for Goal Models" in Advanced Information Systems Engineering: 16th International Conference, CAiSE 2004, Riga, Latvia, June 7-11, 2004: Proceedings, Heidelberg: Springer, 2004, p. 20-35. - (Lecture Notes in Computer Science). - ISBN: 3540221514. Proceedings of: 16th conference on advanced information systems engineering (CAISE'04), Riga, 7th-11th June 2004
  • P. Patel-schneider ; R. Sebastiani, "A New General Method to Generate Random Modal Formulae for Testing Decision Procedures" in THE JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, v. 18, (2003), p. 351-389. - DOI: 10.1613/jair.1166
  • P. Giorgini ; E. Nicchiarelli ; R. Sebastiani ; J. Mylopoulos, "Formal Reasoning Techniques for Goal Models" in JOURNAL ON DATA SEMANTICS, v. 1(1), (2003), p. 1-20. - DOI: 10.1007/978-3-540-39733-5_1
  • R. Sebastiani ; S. Tonetta, "'More deterministic' vs. 'Smaller' Buechi Automata for Efficient LTL Model Checking" in Proc. CHARME 2003, Berlin: Springer, 2003, p. 126-140. - (LNCS). Proceedings of: CHARME, L'Aquila, 2003
  • G. Audemard ; P. Bertoli ; A. Cimatti ; A. Kornilowicz ; R. Sebastiani, "A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions" in Automated Deduction - CADE-18, Berlin: Springer Verlag, 2002, p. 195-210. - (Lecture Notes in Artificial Intelligence). - ISBN: 3540439315. Proceedings of: CADE 2002, Copenhagen, 2002
  • AUDEMARD G.; CIMATTI A.; KORNILOWICZ A; R. SEBASTIANI, "Bounded Model Checking for Timed Systems." in Formal Techniques for Networked and Distributed Systems (FORTE 2002), Berlin: Springer, 2002, p. 243-259. - (LNCS). - ISBN: 3540001417. Proceedings of: FORTE 2002, Houston, 11-14 november 2002
  • S. Linton ; R. Sebastiani, "Editorial: The Integration of Automated Reasoning and Computer Algebra Systems" in JOURNAL OF SYMBOLIC COMPUTATION, v. 34, n. 4 (2002), p. 239-239. - DOI: 10.1016/j.jsc.2004.12.001
  • A. Cimatti ; M. Pistore ; M. Roveri ; R. Sebastiani, "Improving the Encoding of LTL Model Checking into SAT" in Verification, Model Checking, and Abstract Interpretation, Third International Workshop, VMCAI 2002, Berlin: Springer Verlag, 2002, p. 196-207. - (Lecture Notes in Computer Science). - ISBN: 3540436316. Proceedings of: VMCAI 2002, Venice, January 2002
  • A. Cimatti ; E. Giunchiglia ; M. Pistore ; M. Roveri ; R. Sebastiani ; A. Tacchella, "Integrating BDD-based and SAT-based Symbolic Model Checking" in Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002, Berlin: Springer Verlag, 2002, p. 49-56. - (LNAI). - ISBN: 3540433813. Proceedings of: Frontiers of Combining Systems, FROCOS'02, Santa Margherita, January 2002
  • G. Audemard; P. Bertoli; A. Cimatti; A. Kornilowicz; R. Sebastiani, "Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms and Requirements" in Artificial Intelligence, Automated Reasoning, and Symbolic Computation, Joint International Conferences, Berlin: Springer Verlag, 2002, p. 231-245. - (Lecture notes in Artificial Intelligence). - ISBN: 3540438653. Proceedings of: Artificial Intelligence, Automated Reasoning, and Symbolic Computation, Marseille, 2002
  • S. Linton; R. Sebastiani (Ed. critica a cura di), Journal of Symbolic Computation, Special Issue on Integration of Automated Reasoning and Computer Algebra Systems, Amsterdam: Elsevier, 2002
  • S. Linton; R. Sebastiani (Ed. critica a cura di), Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems.The Integration of Automated Reasoning and Computer Algebra Systems., Amsterdam: Elsevier, 2002. - DOI: 10.1006/jsco.2002.0553
  • A. Cimatti ; E. Clarke ; E. Giunchiglia ; F. Giunchiglia ; M. Pistore ; M. Roveri ; R. Sebastiani ; A. Tacchella, "NuSMV2: an open source tool for symbolic model checking" in Computer-Aided verification (CAV'02), Berlin/Heidelberg: Springer, 2002, p. 359-364. - (Lecture Notes in Computer Science). - ISBN: 3540439978. Proceedings of: 14th international conference on computer aided verification (CAV'02), Copenhagen, 27th-31st July 2002. - [download]
  • P. Giorgini ; J. Mylopoulos ; R. Sebastiani, "Reasoning with Goal Models" in International Conference on conceptual Modeling (ER2002),, Berlin: Springer Verlag, 2002, p. 167-181. - ISBN: 3540442774. Proceedings of: International Conference on conceptual Modeling (ER2002),, Tampere, Finland, October 2002
  • P. GIORGINI; MYLOPOULOS J.; NICCHIARELLI E.; SEBASTIANI R., "Reasoning with Goal Models." in Proceedings of the 21st International Conference on Conceptual Modeling, (ER 2002), 2002
  • G. Audemard ; A. Cimatti ; A. Kornilowicz ; R. Sebastiani, "SAT-Based Bounded Model Checking for Timed Systems" in Frontiers of Combining Systems, 4th International Workshop, Berlin: Springer, 2002, p. 49-56. - (LNCS). - ISBN: 3540433813. Proceedings of: FORTE'02, Houston, Texas, November 2002
  • P. Patel-schneider ; R. Sebastiani, "A System and Methodology for Generating Random Modal Formula" in IJCAR-2001, International Joint Conference on Automated reasoning, Berlin: Springer Verlag, 2001. - (Lecture Notes in Artificial Intelligence). - ISBN: 3540422544. Proceedings of: IJCAR-2001, International Joint Conference on Automated reasoning., Siena, July 2001. - URL: http://www.science.unitn.it/~rseba/papers/ijcar2001.ps.gz
  • P. Patel-schneider ; R. Sebastiani, "Improving the generation of random modal formulae for testing decision procedures" in IJCAR2001 Workshop on Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, Berlin: Springer, 2001. Proceedings of: IJCAR2001 Workshop on Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, Siena, Italy, June 2001
  • F. GIUNCHIGLIA; SEBASTIANI R.; TRAVERSO P., "Integrating SAT Solvers with Domain-Specific Reasoners" in CALCULEMUS 2000- Symposium, Simbolic Computation and Automated Reasoning, 2001, p. 249-251
  • R. Sebastiani ; A. Tomasi ; F. Giunchiglia, "Model checking syllabi and student careers" in ETAPS 2001, Berlin: Springer, 2001, p. 128-142. - (LNCS). - ISBN: 3540418652. Proceedings of: ETAPS 2001, Genova, 2-6 April 2001. - URL: http://www.springerlink.com/app/home/contribution.asp?wasp=c96e78b4uq5wnked9j5m&referrer=parent&back
  • A. Cimatti ; E. Giunchiglia ; M. Pistore ; R. Sebastiani ; M. Roveri ; A. Tacchella, "NuSMV Version 2: BDD-based + SAT-based Symbolic ModelChecker." in Proceeding CAV 2002, Berlin: Springer, 2001, p. 241-268. - (LNCS). Proceedings of: IJCAR2001 Workshop on Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, Siena, Italy, June 2001. - DOI: 10.1007/3-540-45657-0
  • I. Horrocks ; P. Patel-schneider ; R. Sebastiani, "An Analysis of Empirical Testing for Modal Decision Procedures" in LOGIC JOURNAL OF THE IGPL, v. 8, n. 3 (2000), p. 293-323. - DOI: 10.1093/jigpal/8.3.293
  • F. Giunchiglia ; R. Sebastiani, "Building decision procedures for modal logics from propositional decision procedures: the case study of modal K(m)" in INFORMATION AND COMPUTATION, v. 162, n. 1-2 (2000), p. 158-178. - DOI: 10.1006/inco.1999.2850
  • GIUNCHIGLIA; R. SEBASTIANI; TRAVERSO P., "Integrating SAT solvers with domain-specific reasoners" in Symbolic Computation and Automated Reasoning,, MA: A K Peters Ltd, 2000. - ISBN: 9781568811451. Proceedings of: CALCULEMUS-2000 Symposium, St Andrews University, 6-9 August 2000
  • E. Giunchiglia ; F. Giunchiglia ; R. Sebastiani ; A. Tacchella, "SAT vs. translation based decision procedures for modal logics: a comparative evaluation" in JOURNAL OF APPLIED NON-CLASSICAL LOGICS, v. 10, n. 2 (2000), p. 145-172. - DOI: 10.1080/11663081.2000.10510994
  • R. Sebastiani ; E. Giunchiglia, "Applying the Davis-Putnam procedure to non-clausal formulas" in AI*IA 99:Advances in Artificial Intelligence, 6th Congress of the Italian Association for Artificial Intelligence, BERLIN: Springer Verlag, 1999, p. 84-94. - ISBN: 3540673504. Proceedings of: AI*IA'99, Bologna, Italy, April 1999
  • A. Chiappini ; A. Cimatti ; C. Porzia ; G. Rotondo ; R. Sebastiani ; P. Traverso ; A. Villafiorita, "Formal Specification and Development of a Safety-Critical Train Management System" in Formal Specification and Development of a Safety-Critical Train Management System, Berlin: Springer Verlag, 1999, p. 410-419. - (LNCS). - ISBN: 9783540664888. Proceedings of: International Conference Computer Safety, Reliablityans Security - SAFECOMP'99., Toulouse, France,, September 1999. - DOI: 10.1007/3-540-482-49_035
  • A. Cimatti ; P. Pieraccini ; R. Sebastiani ; P. Traverso ; A. Villafiorita, "Formal specification and validation of a vital protocol" in Formal Specification and Validation of a Vital Communication Protocol, Berlin: Springer Verlag, 1999, p. 1584-1604. - (LNCS). - ISBN: 3540665889. Proceedings of: FM'99 -- World Congress on Formal Methods., Toulouse, France, September 1999
  • A. Cimatti ; R. Sebastiani ; P. Traverso, "Specifica formale dei protocolli Safety Layer e Connection Manager", 1999, sponsored by: ITC-IRST e Ansaldo Segnalamento Ferroviario
  • E. Giunchiglia ; A. Massarotto ; R. Sebastiani, "Act, and the rest will follow: exploiting determinism in planning as satisfiability" in Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, Berlin: AAAI Press, 1998, p. 948-953. - ISBN: 0262510987. Proceedings of: 15th National Conference on Artificial Intelligence (AAAI98), Madison (WI), July 1998
  • A. Chiappini ; A. Cimatti ; F. Giunchiglia ; G. Rotondo ; R. Sebastiani ; P. Traverso ; A. Villafiorita, "Formal Specication of the Radio Block Centre (RBC): First Part.", 1998, sponsored by: ITC-IRST e Ansaldo Segnalamento Ferroviario
  • E. Giunchiglia ; F. Giunchiglia ; R. Sebastiani ; A. Tacchella, "More evaluation of decision procedures for modal logics" in Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning, San Francisco, Calif.: Morgan Kauffman, 1998, p. 626-635. Proceedings of: 6th international conference on principles of knowledge representation and reasoning (KR'98), Trento, 2-5 June 1998
  • A. Cimatti ; R. Sebastiani, "Protocolli Safety Layer e Connection Manager: Descrizione del Codice SDL", 1998, sponsored by: ITC-IRST e Ansaldo Segnalamento Ferroviario
  • R. Sebastiani ; A. Villafiorita, "SAT-based decision procedures for normal modal logics:a theoretical framework" in Artificial intelligence:methodology, systems and applications, 8th international conference AIMA 98, Sozopol, Bulgaria, Berlin: Springer Verlag, 1998, p. 377-388. - (LNCS. LNAI). Proceedings of: 6th International Conference onArtificial Intelligence: Methodology, Systems, Applications - AIMSA'98, Sozopol, Bulgaria, September 1998. - DOI: 10.1007/BFb0057460
  • A. Cimatti ; R. Sebastiani, "Servizi forniti dagli strati Safety Layer e Connection Manager", 1998, sponsored by: ITC-IRST e Ansaldo Segnalamento Ferroviario
  • F. Giunchiglia; M. Roveri; R. Sebastiani, "A new method for testing decision procedures in modal logics" in Automated Deduction, Berlin, Heidelberg: Springer, 1997, p. 264-267. - (LNCS. LNAI). - ISBN: 3540631046. Proceedings of: CADE-14, Townsville, 13-17 July 1997
  • F. Giunchiglia; R. Sebastiani; A. Villafiorita; T. Walsh, "A general purpose reasoner for abstraction" in Canadian Conference on Artificial Intelligence, BERLIN: Springer, 1996, p. 323-335. - (LNCS). - ISBN: 3540612912. Proceedings of: 11th biennial conference of the Canadian society for computational studies of intelligence on advances in artificial intelligence (AI'96), Toronto, 21-24 May 1996
  • F. Giunchiglia; M. Roveri; R. Sebastiani, "A new method for testing decision procedures in modal and terminological logics" in International Description Logics: Papers from the AAAI Workshop, Menlo Park, Calif.: AAAI press, 1996, p. 119-123. - (AAAI Technical Report). - ISBN: 9781577350149. Proceedings of: International Workshop on Description Logics (DL'96), Cambridge, Mass., 2-4 November 1996. - DOI: 10.1007/3-540-63104-6_26
  • F. Giunchiglia ; R. Sebastiani, "A SAT-based decision procedure for ALC" in Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR'96), San Francisco, Calif.: Morgan Kaufmann, 1996, p. 304-314. - ISBN: 1558604219. Proceedings of: 5th international conference on principles of knowledge representation and reasoning (KR'96), Cambridge, Mass., 5-8 November 1996
  • F. Giunchiglia ; R. Sebastiani, "An SAT-based decision procedure for ALC" in Proceedings of the 1996 International Workshop on Description Logics, Berlin: AAAI Press, 1996, p. 49-59. - ISBN: 1577350146. Proceedings of: International workshop on description logics (DL'96), Cambridge, Mass., 2-4 November 1996
  • F. Giunchiglia ; R. Sebastiani, "Building decision procedures for modal logics from propositional decision procedures: the case study of modal K" in 13th International Conference on Automated Deduction, Berlin: Springer, 1996, p. 583-597. - (LNCS). - ISBN: 3540615113. Proceedings of: 13th international conference on automated deduction (CADE-13), New Brunswick, N.J., 30 July - 3 August 1996
  • F. GIUNCHIGLIA; SEBASTIANI R., "Calculating criticalities" in ARTIFICIAL INTELLIGENCE, v. 88, (1996), p. 39-67
  • A. Bundy ; F. Giunchiglia ; R. Sebastiani ; T. Walsh, "Calculating criticalities" in ARTIFICIAL INTELLIGENCE, v. 88, (1996), p. 39-67. - DOI: 10.1016/S0004-3702(96)00019-7
  • A. Bundy ; F. Giunchiglia ; R. Sebastiani ; T. Walsh, "Computing abstraction hierarchies by numerical simulation" in Proceedings of the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of ArtificialIntelligence Conference, Menlo Park (CA): AAAI Press/The MIT Press, 1996, p. 523-529. - ISBN: 026251091X. Proceedings of: 13th national conference on artificial intelligence and the 8th innovative applications of artificial intelligence conference, Portland (OR), 4th-8th August 1996. - URL: http://www.aaai.org/Press/Proceedings/AAAI/1996/aaai96.html
  • R. SEBASTIANI; GIUNCHIGLIA F, "Proving Theorems by Using Abstraction Interactively" in Trends in Theoretical Informatics, 1996
  • R. Sebastiani ; A. Villafiorita ; F. Giunchiglia, "Proving theorems by using abstraction interactively" in Journal of Automated Reasoning, New York: Acm, 1995, p. 37-48. Proceedings of: 2nd international round-table on abstract intelligent agent: situation assessment (AIA'94), Roma, 23-25 February 1994
  • R. Sebastiani, "Applying GSAT To Non-Clausal Formulas" in THE JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, v. 1, (1994), p. 304-309. - DOI: 10.1613/jair.49
  • A. Villafiorita ; R. Sebastiani, "Proof Planning by Abstraction" in ECAI-94 Workshop 'From Theorem Provers to Mathematical Assistants: Issues and Possible Solutions, Berlin: Springer, 1994, p. 319-346. Proceedings of: ECAI-94 Workshop 'From Theorem Provers to Mathematical Assistants: Issues and Possible Solutions, Amsterdam, Holland, August 1994. - DOI: 10.1023/A:1005877613942
  • R. Sebastiani ; M. Di Manzo ; F. Giunchiglia, "Using abstraction interactively" in Proceedings of the Workshop on Theory Reformulation and Abstraction, Berlino: Springer, 1994, p. 39-55. Proceedings of: Workshop on theory reformulation and abstraction, Jackson Hole, Wyo., 22-24 May 1994