CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

SmacC: A Retargetable Symbolic Execution Engine

Armin Biere ; Jens Knoop ; Laura Kovacs (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Jakob Zwirchmayr
Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA 2013), October 15-18, 2013, Hanoi, Vietnam, Dang Van Hung and Mizuhito Ogawa (editors), Springer Lecture Notes in Computer Science Vol. LNCS 8172 (2013), p. 482-486.
[Konferensbidrag, refereegranskat]

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.

Nyckelord: formal methods, program analysis, program verification, timing analysis, symbolic execution, decision procedures, automated reasoning



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2014-01-07. Senast ändrad 2016-08-22.
CPL Pubid: 191561

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)