Name
Abstract | ||
|---|---|---|
A mechanism for generating verification conditions (VCs) for the iteration-free fragment of an imperative language is fundamental in any deductive program verification system. In this paper we revisit symbolic execution, weakest preconditions, and bounded model checking as VC-generation mechanisms, and propose a uniform presentation of the corresponding sets of VCs, in terms of (logical encodings of) paths in the control-flow graph of a single-assignment form of the program under analysis. This allows us to compare the mechanisms, in particular with respect to the size of the generated formulas. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1145/2245276.2231977 | SAC |
Keywords | Field | DocType |
vc-generation mechanism,iteration-free fragment,imperative language,logical encodings,corresponding set,control-flow graph,single-assignment form,bounded model checking,verification condition,single-assignment program,deductive program verification system,attribute selection,quality assurance,weakest precondition,control flow graph | Functional verification,Single assignment,Model checking,Programming language,Feature selection,Computer science,Imperative programming,Runtime verification,Theoretical computer science,Symbolic execution,Bounded function | Conference |
Citations | PageRank | References |
1 | 0.36 | 7 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daniela da Cruz | 1 | 9 | 3.19 |
| Maria João Frade | 2 | 19 | 2.89 |
| Jorge Sousa Pinto | 3 | 160 | 23.19 |