[Back]


Contributions to Proceedings:

A. Biere, J. Knoop, L. Kovacs, J. Zwirchmayr:
"SmacC: A Retargetable Symbolic Execution Engine";
in: "AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS 11th International Symposium, ATVA 2013", issued by: Dang Van Hung and Mizuhito Ogawa; Springer LNCS 8172, 2013.



English abstract:
SmacC is a symbolic execution engine for C programs. It can be used
for program verification, bounded model checking and generating SMT bench-
marks. More recently we also successfully applied SmacC for high-level timing
analysis of programs to infer exact loop bounds and safe over-approximations.
SmacC uses the logic for bit-vectors with arrays to construct a bit-precise memory-
model of a program for path-wise exploration.

Keywords:
symbolic execution, program analysis, wcet analysis, verification


Electronic version of the publication:
http://publik.tuwien.ac.at/files/PubDat_221284.pdf


Created from the Publication Database of the Vienna University of Technology.