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,
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.
symbolic execution, program analysis, wcet analysis, verification
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.