Research Outputs Roberto Sebastiani


  • A. Griggio, H.T. T. 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:3)2012 - see details
  • 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 - see details
  • A. Cimatti, R. Sebastiani (edited by), "Theory and Applications of Satisfiability Testing - SAT 2012- 15th International Conference.", Berlin: Springer, 2012, 364 p. - (LNCS; 5749). - ISBN: 9783642316111. - DOI: 10.1007/978-3-642-31612-8 - see details
  • 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; 6803). Proceedings of: CADE 2011, WROCLAW, 31 JULY - 5 AUGUST. - URL: http://www.springerlink.com/content/k706v118223u6785/ . - DOI: 10.1007/978-3-642-22438-6_22 - see details
  • 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 - see details
  • 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; 6605). - ISBN: 9783642198342. Proceedings of: TACAS 2010, Saarbrücken, 26th March-3rd April 2011. - DOI: 10.1007/978-3-642-19835-9 - see details
  • A. Griggio, Q.S. Phan, S. Tomasi, R. Sebastiani, "Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT " in In proc. FroCoS 2011 - 8th International Symposium on Frontiers of Combining Systems, BERLIN: SPRINGER, 2011, p. 163-178 -(LNCS; 6989). - ISBN: 9783642243639. Proceedings of: FROCOS , Saarbrücken, 5-7 OCTOBER 2011. - URL: http://www.springer.de/comp/lncs/index.html - see details
  • 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. - URL: http://www.springerlink.com/content/np21828444m584v5/fulltext.pdf . - DOI: 10.1007/s10009-010-0168-4 - see details
  • 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/ - see details
  • 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 - see details
  • P. Giorgini, J. Mylopoulos, R. Sebastiani, "Goal Modelling and Reasoning in Tropos" in E. Yu, P. Giorgini, N. Maiden, J. Mylopoulos (edited by), Social Modeling for Requirements Engineering, Cambridge, MA ; London: MIT press, 2010, p. 645-668. - ISBN: 9780262240550 - see details
  • 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; 6015). - ISBN: 9783642120015. Proceedings of: 16th International Conference TACAS 2010, Paphos, Cyprus, 20th-28th March 2010. - DOI: 10.1007/978-3-642-12002-2_8 - see details
  • 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 - see details
  • 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; Vol. 5663). - ISBN: 9783642029585. Proceedings of: International Conference on Automated Deduction, CADE-22., Montreal, Canada, August 2009. - DOI: 10.1007/978-3-642-02959-2_6 - see details
  • 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 - see details
  • S. Ghilardi, R. Sebastiani (edited by), "Frontiers of Combining Systems", BERLIN: Springer, 2009. - ISBN: 9783642042218 - see details
  • 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 - see details
  • 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 - see details
  • 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 - see details
  • 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 - see details
  • 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; 4963). - ISBN: 9783540787990. Proceedings of: TACAS 2008, Budapest, April 2008. - DOI: 10.1007/978-3-540-78800-3_30 - see details
  • R. Bruttomesso, A. Cimatti, M.P. A. Franzen, A. Griggio, R. Sebastiani, "The MathSAT 4 SMT Solver" in Computer Aided Verification, Heidelberg: Springer, 2008, p. 299-303 -(LNCS; 5123). - ISBN: 9783540705437. Proceedings of: CAV 2008, 20th International Conference, Princeton, N.Y., July 2008 - see details
  • R. Bruttomesso, A. Cimatti, M.P. A. 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, Germany, July 3-7, 2007, Proceedings, Berlin; Heidelberg: Springer, 2007, p. 547-560 -(LNCS; 4590). - ISBN: 9783540733676. Proceedings of: CAV 2007, Berlin, 3rd-7th July 2007. - DOI: 10.1007/978-3-540-73368-3_54 - see details
  • 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 - see details
  • 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 - see details
  • B. Cook, R. Sebastiani (edited by), "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; 06/01/1900 6.08.00) - see details
  • 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; 4720). - ISBN: 9783540746201. Proceedings of: FroCoS2007, Liverpool, Uk, SEPTEMBER - see details
  • 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 - see details
  • B. Cook, R. Sebastiani (edited by), "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); 3) - see details
  • R. Sebastiani, "Lazy Satisfiability Modulo Theories" in JOURNAL ON SATISFIABILITY, BOOLEAN MODELING AND COMPUTATION, v. 3, n. 4963 (2007), p. 141-224 - see details
  • B. Cook, R. Sebastiani (edited by), "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 - see details
  • 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 - see details
  • 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: 978-3-540-34304-2. - DOI: 10.1007/11757283_6 - see details
  • R. Bruttomesso, A. Cimatti, M.P. A. 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; 4246). - 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 - see details
  • 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 - see details
  • M. Bozzano, R. Bruttomesso, A. Cimatti, M.P. A. 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 - see details
  • 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; 4121). - 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 - see details
  • R. Bruttomesso, A. Cimatti, M.P. A. 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; 4246). - 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 - see details
  • 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; 3440). - ISBN: 3540253335. Proceedings of: Springer, Edinburgh, Scotland, 2005 - see details
  • 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; 3576). - ISBN: 3540272313. Proceedings of: CAV 2005, Edinburgh, Scotland, 2005 - see details
  • 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 - see details
  • 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 - see details
  • 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 - see details
  • 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 - see details
  • 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; 3576). - ISBN: 3540272313. Proceedings of: CAV 2005, Edinburgh, Scotland, 2005 - see details
  • 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; 3632). - ISBN: 3540280057. Proceedings of: CADE 20, Tallin, July 22-27 2005 - see details
  • 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 - see details
  • 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; 3114). - ISBN: 3540223428. Proceedings of: 16th international conference on computer aided verification (CAV 2004), Boston, Mass., 13th-17th July 2004 - see details
  • 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; 3084). - ISBN: 3540221514. Proceedings of: 16th conference on advanced information systems engineering (CAISE'04), Riga, 7th-11th June 2004 - see details
  • 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 - see details
  • 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 - see details
  • 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; 2860). Proceedings of: CHARME, L'Aquila, 2003 - see details
  • 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; 2392). - ISBN: 3540439315. Proceedings of: CADE 2002, Copenhagen, 2002 - see details
  • G. Audemard, A. Cimatti, A. Kornilowicz, 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; 2529). - ISBN: 3540001417. Proceedings of: FORTE 2002, Houston, 11-14 november 2002 - see details
  • 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 - see details
  • 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; 2294). - ISBN: 3540436316. Proceedings of: VMCAI 2002, Venice, January 2002 - see details
  • 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; 2309). - ISBN: 3540433813. Proceedings of: Frontiers of Combining Systems, FROCOS'02, Santa Margherita, January 2002 - see details
  • 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; 2385). - ISBN: 3540438653. Proceedings of: Artificial Intelligence, Automated Reasoning, and Symbolic Computation, Marseille, 2002 - see details
  • S. Linton, R. Sebastiani (edited by), "Journal of Symbolic Computation, Special Issue on Integration of Automated Reasoning and Computer Algebra Systems", Amsterdam: Elsevier, 2002 - see details
  • S. Linton, R. Sebastiani (edited by), "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 - see details
  • 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; 2404). - ISBN: 3540439978. Proceedings of: 14th international conference on computer aided verification (CAV'02), Copenhagen, 27th-31st July 2002. - URL: http://eprints.biblio.unitn.it/archive/00000085/ - see details
  • 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 - see details
  • 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 - see details
  • 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; 2083). - 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 - see details
  • 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 - see details
  • F. Giunchiglia, R. Sebastiani, P. Traverso, "Integrating SAT solvers with domain-specific reasoners" in Symbolic Computation and Automated Reasoning, Wellesley, Mass.: A K Peters, 2001, p. 249-251 - see details
  • R. Sebastiani, A. Tomasi, F. Giunchiglia, "Model checking syllabi and student careers" in ETAPS 2001, Berlin: Springer, 2001, p. 128-142 -(LNCS; 2031). - 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 - see details
  • 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; 2404). 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 - see details
  • 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 - see details
  • 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 - see details
  • Giunchiglia, R. Sebastiani, P. Traverso, "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 - see details
  • 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 - see details
  • 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 - see details
  • 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; 1698). - ISBN: 9783540664888. Proceedings of: International Conference Computer Safety, Reliablityans Security - SAFECOMP'99., Toulouse, France,, September 1999. - DOI: 10.1007/3-540-482-49_035 - see details
  • 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; 1709). - ISBN: 3540665889. Proceedings of: FM'99 -- World Congress on Formal Methods., Toulouse, France, September 1999 - see details
  • A. Cimatti, R. Sebastiani, P. Traverso, "Specifica formale dei protocolli Safety Layer e Connection Manager", 1999, sponsored by: ITC-IRST e Ansaldo Segnalamento Ferroviario - see details
  • 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 - see details
  • 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 - see details
  • 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 - see details
  • A. Cimatti, R. Sebastiani, "Protocolli Safety Layer e Connection Manager: Descrizione del Codice SDL", 1998, sponsored by: ITC-IRST e Ansaldo Segnalamento Ferroviario - see details
  • 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; 1480). Proceedings of: 6th International Conference onArtificial Intelligence: Methodology, Systems, Applications - AIMSA'98, Sozopol, Bulgaria, September 1998. - DOI: 10.1007/BFb0057460 - see details
  • A. Cimatti, R. Sebastiani, "Servizi forniti dagli strati Safety Layer e Connection Manager", 1998, sponsored by: ITC-IRST e Ansaldo Segnalamento Ferroviario - see details
  • 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; 1249). - ISBN: 3540631046. Proceedings of: CADE-14, Townsville, 13-17 July 1997 - see details
  • 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; 1081). - 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 - see details
  • 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 - see details
  • 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 - see details
  • 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 - see details
  • 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 - see details
  • 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 - see details
  • 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 - see details
  • R. Sebastiani, F. Giunchiglia, "Proving Theorems by Using Abstraction Interactively" in Trends in Theoretical Informatics, 1996 - see details
  • F. Giunchiglia, R. Sebastiani, A. Villafiorita, "Proving theorems by using abstraction interactively" in R. Albrecht, H. Herre (edited by), Trends in theoretical informatics, München ; Wien: Oldenbourg, 1996, p. 83-94. - (Schriftenreihe der Österreichischen Computer Gesellschaft; 89) - see details
  • 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 - see details
  • 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 - see details
  • 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 - see details
  • 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 - see details