[Back]

J. Zwirchmayr:
"A Satisfiability Modulo Theories Memory-Model and Assertion Checker for C";
Talk: 27. Workshop der GI-Fachgruppe "Programmiersprachen und Rechenkonzepte", Bad Honnef; 2010-05-03 - 2010-05-05; in: "27. Workshop der GI-Fachgruppe Programmiersprachen & Rechenkonzepte", M. Hanus, F. Reck (ed.); Technischer Bericht des Instituts für Informatik der Christian-Albrechts Universität zu Kiel, 0811 / Kiel (2010), Paper ID 18, 10 pages.

This paper presents SmacC, a tool for software verification
and SMT benchmark generation. It builds upon a state-of-the-art SMT
solver, Boolector, developed at FMV institute at JKU, Linz. SmacC gets
as input a program that lies in the supported subset of C and transforms
it to SMT formulas. The SMT representation allows verification of properties
that are required to hold on the program. SmacC symbolically executes
the programs source code, establishing an SMT (memory-) model
for the program. Some statements and expressions require the construction
of SMT formulas specifying properties about them, the SMT solver
decides their satisfiability. If properties checked do not hold on the SMT
representation, they do not hold on the real program. SmacC can generate
SMT benchmarks by dumping the SMT instances for those checks.

smacc, sw verification, SMT, SAT, symbolic execution, symbolic simulation