Programmation d'un interpréteur abstrait certifié en logique constructive / Programming a certified abstract interpreter in constructive logic
In: Méthodes formelles pour l'analyse statique et la compilation, Jg. 30 (2011), Heft 4, S. 381-408
academicJournal
- print, 1 p.1/4
Zugriff:
A static analyzer aims at automatically deducing program properties by examining its source code. Proving the correctness of an analyzer is based on semantic properties, and becomes difficult to ensure when complex analysis techniques are involved. We propose to adapt the general theory of static analysis by abstract interpretation to the framework of constructive logic. Implementing this formalism into the Coq proof assistant then allows for automatic extraction of certified analyzers. We focus here on a simple imperative language and present the computation of fixpoints by widening/narrowing and syntax-directed iteration techniques.
Titel: |
Programmation d'un interpréteur abstrait certifié en logique constructive / Programming a certified abstract interpreter in constructive logic
|
---|---|
Autor/in / Beteiligte Person: | CACHERA, David ; PICHARDIE, David |
Link: | |
Zeitschrift: | Méthodes formelles pour l'analyse statique et la compilation, Jg. 30 (2011), Heft 4, S. 381-408 |
Veröffentlichung: | Paris: Lavoisier, 2011 |
Medientyp: | academicJournal |
Umfang: | print, 1 p.1/4 |
ISSN: | 0752-4072 (print) |
Schlagwort: |
|
Sonstiges: |
|