DocumentCode
2315752
Title
SMT Solvers for Testing, Program Analysis and Verification at Microsoft
Author
Bjørner, Nikolaj
Author_Institution
Microsoft Res., Redmond, WA, USA
fYear
2009
fDate
26-29 Sept. 2009
Firstpage
15
Lastpage
15
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/SYNASC.2009.64
Filename
5460875
Link To Document