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.

symbolic execution, program analysis, wcet analysis, verification

Electronic version of the publication:

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