Name
Abstract | ||
|---|---|---|
This paper reports on the design and soundness proof, using the Coq proof assistant, of Verasco, a static analyzer based on abstract interpretation for most of the ISO C 1999 language (excluding recursion and dynamic allocation). Verasco establishes the absence of run-time errors in the analyzed programs. It enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and non-relational. Verasco integrates with the CompCert formally-verified C compiler so that not only the soundness of the analysis results is guaranteed with mathematical certitude, but also the fact that these guarantees carry over to the compiled code. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1145/2676726.2676966 | POPL |
Keywords | Field | DocType |
assertion checkers,abstract interpretation,correctness proofs,mechanical verification,soundness proofs,static analysis,proof assistants | Programming language,Computer science,Abstract interpretation,Static analysis,Compiler,Theoretical computer science,Compiled language,Soundness,Spectrum analyzer,Recursion,Proof assistant | Conference |
Volume | Issue | ISSN |
50 | 1 | 0362-1340 |
Citations | PageRank | References |
33 | 0.93 | 31 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jacques-Henri Jourdan | 1 | 109 | 7.21 |
| Vincent Laporte | 2 | 81 | 3.61 |
| Sandrine Blazy | 3 | 338 | 27.40 |
| Xavier Leroy | 4 | 2125 | 138.02 |
| david pichardie | 5 | 488 | 33.73 |