Name
Abstract | ||
|---|---|---|
Static analyzers based on abstract interpretation are complex pieces of software implementing delicate algorithms. Even if static analysis techniques are well understood, their implementation on real languages is still error-prone. This paper presents a formal verification using the Coq proof assistant: a formalization of a value analysis (based on abstract interpretation), and a soundness proof of the value analysis. The formalization relies on generic interfaces. The mechanized proof is facilitated by a translation validation of a Bourdoncle fixpoint iterator. The work has been integrated into the CompCert verified C-compiler. Our verified analysis directly operates over an intermediate language of the compiler having the same expressiveness as C. The automatic extraction of our value analysis into OCaml yields a program with competitive results, obtained from experiments on a number of benchmarks and comparisons with the Frama-C tool. |
Year | Venue | DocType |
|---|---|---|
2013 | Lecture Notes in Computer Science | Conference |
Volume | ISSN | Citations |
7935 | 0302-9743 | 16 |
PageRank | References | Authors |
0.73 | 24 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sandrine Blazy | 1 | 338 | 27.40 |
| Vincent Laporte | 2 | 81 | 3.61 |
| André Maroneze | 3 | 24 | 1.86 |
| david pichardie | 4 | 488 | 33.73 |