Abstract
dc:descriptionFormal 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.
Degree
thesis:*- Grantor dc:publisher
- Università degli studi di Trento
- Year dc:date
- 2009
Author and committee
dc:creator, dc:contributor.*- Author dc:creator
-
- Griggio, Alberto
- Contributors dc:contributor
-
- Sebastiani, Roberto
- Cimatti, Alessandro
Subjects
dc:subject × 3Rights
dc:rights- Statement dc:rights
-
- info:eu-repo/semantics/openAccess
- license:Tutti i diritti riservati (All rights reserved)
- Language dc:language
- eng
Identifiers
dc:identifier.*- OAI identifier oai:identifier
- oai:iris.unitn.it:11572/368765