[Zurück]


Beiträge in Tagungsbänden:

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", herausgegeben von: Dang Van Hung and Mizuhito Ogawa; Springer LNCS 8172, 2013.



Kurzfassung englisch:
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.

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


Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/PubDat_221284.pdf


Erstellt aus der Publikationsdatenbank der Technischen Universitšt Wien.