Armin Biere, Jens Knoop, Laura Kovács, Jakob Zwirchmayr,
"SmacC: A Retargetable Symbolic Execution Engine"
: Proc. 11th Intl. Symp. on Automated Technology for Verification and Analysis, Serie Lecture Notes in Computer Science, Vol. 8172, Springer, Seite(n) 485-486, 2013
SmacC: A Retargetable Symbolic Execution Engine
Sprache des Titels:
Proc. 11th Intl. Symp. on Automated Technology for Verification and Analysis
SmacC is a symbolic execution engine for C programs. It can be used for program verification, bounded model checking and generating SMT benchmarks. 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.