2026-09-19T15:23:04Zhttps://iris.unitn.it/oai/request

oai:iris.unitn.it:11572/3687652026-04-03T00:48:40Zcom_11572_237821com_11572_101871col_11572_237822

An Effective SMT Engine for Formal Verification Griggio, Alberto Griggio, Alberto Sebastiani, Roberto Cimatti, Alessandro Settore INF/01 - Informatica Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni Settore MAT/01 - Logica Matematica 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. 2009 info:eu-repo/semantics/doctoralThesis https://hdl.handle.net/11572/368765 http://dx.doi.org/10.15168/11572_368765 10.15168/11572_368765 eng firstpage:1 lastpage:255 numberofpages:255 info:eu-repo/semantics/openAccess Università degli studi di Trento license:Tutti i diritti riservati (All rights reserved)