Paper Info
Title
A precise memory model for low-level bounded model checking
Abstract
Formalizing the semantics of programming languages like C or C++ for bounded model checking can be cumbersome if complete coverage of all language features is to be achieved. On the other hand, low-level languages that occur during translation (compilation) have a much simpler semantics since they are closer to the machine level. It thus makes sense to use these low-level languages for bounded model checking. In this paper we present a highly precise memory model suitable for bounded model checking of such low-level languages. Our method also takes memory protection (malloc/free) into account.
Year
Venue
Keywords
2010
SSV
precise memory model,memory protection,simpler semantics,low-level bounded model checking,programming language,bounded model checking,language feature,low-level language,complete coverage,machine level
Field
DocType
Citations 
Memory protection,Abstraction model checking,Programming language,Model checking,C dynamic memory allocation,Computer science,Theoretical computer science,Memory model,Semantics,Bounded function
Conference
20
PageRank 
References 
Authors
1.00
16
3
Name
Order
Citations
PageRank
Carsten Sinz178746.29
Stephan Falke251127.86
Florian Merz31519.56