Title :
SMT Solvers for Testing, Program Analysis and Verification at Microsoft
Author :
Bjørner, Nikolaj
Author_Institution :
Microsoft Res., Redmond, WA, USA
Abstract :
Modern program analysis and model-based tools are increasingly complex and multi-faceted software systems. However, at their core is invariably a component using logic for describing states and transformations between system states. The system Z3, developed at Microsoft Research, is a Satisfiability Modulo Theories (SMT) solver. It provides logic inference capabilities that are critical for the functionality of these systems. The tutorial exemplifies a number of applications of Z3 at Microsoft.
Keywords :
computability; program diagnostics; program testing; program verification; theorem proving; Microsoft research; Z3 system; logic inference; model-based tools; program analysis; program verification; satisfiability modulo theories solver; Algorithm design and analysis; Application software; Computer languages; Concrete; Contracts; Logic; Scientific computing; Software algorithms; Surface-mount technology; Testing;
Conference_Titel :
Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2009 11th International Symposium on
Conference_Location :
Timisoara
Print_ISBN :
978-1-4244-5910-0
Electronic_ISBN :
978-1-4244-5911-7
DOI :
10.1109/SYNASC.2009.64
