Roberto Sebastiani - publication list

See also my personal page at Google Scholar Citations, where my papers are listed in order of citations.

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.

Edited Journal Special Issues:

• Byron Cook, Roberto Sebastiani, Editors
  "Special Issue on Satisfiability Modulo Theories".
  Journal on Satisfiability, Boolean Modeling and Computation, JSAT. Vol. 3, 2007. © IOS Press.
  
• Steve Linton, Roberto Sebastiani, Editors
  "Special Issue on Integration of Automated Reasoning and Computer Algebra Systems".
  Journal of Symbolic Computation, Vol 34 (4) October 2002, © Elsevier.
  

Papers in Journals:

• 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".
  (Extended version of CAV'05 paper.)
  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".
  (Extended version of TACAS'07 paper.)
  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.".
  Extended version. 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, 2007. Pag 141--224, © IOS Press.
  
• Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Vardi
  "GSTE is partitioned Model Checking".(Extended version).
  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.
• Steve Linton, Roberto Sebastiani
  "Editorial: The Integration of Automated Reasoning and Computer Algebra Systems ".
  Journal of Symbolic Computation, Vol 34 (4) October 2002, © Elsevier.
  
• 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".
  October 1999. "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 25, The Handbook of Satisfiability. 2009. IOS press.
• Clark Barrett, Roberto Sebastiani, Sanjit Seshia, Cesare Tinelli
  "Satisfiability Modulo Theories".
  Part II, Chapter 26, The Handbook of Satisfiability. 2009. 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:

• 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:

• 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. Available at Springerlink
• 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:

• Steve Linton, Roberto Sebastiani, Editors
  "Proceedings Calculemus 2001, 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning".
  Siena, Italy, July 2001.
  

Theses:

• Roberto Sebastiani
  "Una nuova classe di procedure di decisione per logiche modali e terminologiche: teoria, implementazione e testing".
  (A new class of decision procedures for modal and terminological logics: theory, implementation and testing.)
  Phd Thesis. DIST, University of Genua, February 1997. In italian.
• Roberto Sebastiani
  "L'astrazione in un dimostratore automatico interattivo: definizione e realizzazione".
  (Abstraction in an interactive Theorem Prover: definition and mechanization.)
  Master Thesis. University of Padua, December 1991. In italian.