Abstract | ||
---|---|---|
This paper presents a methodology for automated modular verification of C programs against specifications written in separation logic. The distinguishing features of the approach are representation of the C memory model in separation logic by means of ... |
Year | DOI | Venue |
---|---|---|
2009 | 10.1016/j.entcs.2009.09.059 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
distinguishing feature,automated modular verification,assembly code,verification,microcontroller software,c program,parallel and distributed algorithms,embedded software,separation logic,c memory model,invariant checking,distributed algorithm,temporal logic,state space,formal verification,model checking,parallel algorithm,embedded system | Abstraction model checking,Model checking,Embedded software,Parallel algorithm,Computer science,Parallel computing,Theoretical computer science,Software,Distributed algorithm,Invariant (mathematics),Formal verification | Journal |
Volume | ISSN | Citations |
254, | Electronic Notes in Theoretical Computer Science | 1 |
PageRank | References | Authors |
0.35 | 18 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Jörg Brauer | 1 | 219 | 19.33 |
Bastian Schlich | 2 | 214 | 17.98 |
Stefan Kowalewski | 3 | 602 | 65.14 |