Griggio, Alberto (2009) An Effective SMT Engine for Formal Verification. PhD thesis, University of Trento.
This is the latest version of this item.
|PDF - Doctoral Thesis|
Formal methods are becoming increasingly important for debugging and verifying hardware and software systems, whose current complexity makes the traditional approaches based on testing increasingly-less adequate. One of the most promising research directions in formal verification is based on the exploitation of Satisfiability Modulo Theories (SMT) solvers. In this thesis, we present MathSAT, a modern, efficient SMT solver that provides several important functionalities, and can be used as a workhorse engine in formal verification. We develop novel algorithms for two functionalities which are very important in verification -- the extraction of unsatisfiable cores and the generation of Craig interpolants in SMT -- that significantly advance the state of the art, taking full advantage of modern SMT techniques. Moreover, in order to demonstrate the usefulness and potential of SMT in verification, we develop a novel technique for software model checking, that fully exploits the power and functionalities of the SMT engine, showing that this leads to significant improvements in performance.
|Item Type:||Doctoral Thesis (PhD)|
|Doctoral School:||Information and Communication Technology|
|Subjects:||Area 01 - Scienze matematiche e informatiche > INF/01 INFORMATICA|
Area 09 - Ingegneria industriale e dell'informazione > ING-INF/05 SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
Area 01 - Scienze matematiche e informatiche > MAT/01 LOGICA MATEMATICA
|Repository Staff approval on:||25 Jan 2010 14:20|
Available Versions of this Item
- An Effective SMT Engine for Formal Verification. (deposited 11 Jan 2010 13:24)
- An Effective SMT Engine for Formal Verification. (deposited 25 Jan 2010 14:20) [Currently Displayed]
Repository Staff Only: item control page