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.
| Identifer | oai:union.ndltd.org:unitn.it/oai:iris.unitn.it:11572/368265 |
| Date | January 2009 |
| Creators | Griggio, Alberto |
| Contributors | Griggio, Alberto, Cimatti, Alessandro, Sebastiani, Roberto |
| Publisher | Università degli studi di Trento |
| Source Sets | Università di Trento |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/doctoralThesis |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | firstpage:1, lastpage:253, numberofpages:253 |
Page generated in 0.0023 seconds