Automatisation de la Certification Formelle de Systèmes Critiques par Instrumentation d'Interpréteurs Abstraits. (Automatic and formal certification of critical systems by instrumentation of abstract interpreters)

Manuel Garnacho · HAL (Le Centre pour la Communication Scientifique Directe) · 2010

Summary

Cette approche permet de certifier avec un tres haut-niveau de confiance les resultats d'outils existants, meme a l'etat de prototypes.

Type: dissertation
Published: 2010-01-01
Cited by: 1
References: 105
Access: Open access
OpenAlex: https://openalex.org/W92861834
Semantic Scholar: https://api.semanticscholar.org/CorpusID:45753741

Keywords

Humanities, Philosophy, Political science

References

Resources, Concurrency and Local ReasoningPeter W. O’Hearn — 2004
Automatic Generation of Invariants and AssertionsNikolaj Bjørner, Anca Browne, Zohar Manna — 1995
Static determination of dynamic properties of programsPatrick Cousot, Radhia Cousot — 1976
Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiésDavid Pichardie — 2005
Weakly Relational Numerical Abstract DomainsAntoine Miné, COUSOT, Patrick — 2004
Two Easy Theories Whose Combination is HardVaughan Pratt — 2002
Hilbert's Program: An Essay on Mathematical Instrumentalism.Mark Steiner, Michael Detlefsen — 1991
The collected papers of Gerhard GentzenG. Gentzen, M. E. Szabo — 1969
Natural Deduction: A Proof-Theoretical StudyDag Prawitz — 1965
Mathematical developments arising from Hilbert problemsFelix E. Browder, Symposium in Pure Mathematics 1974 De Kalb, Ill. — 1976
Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive ConstructionsPierre Castéran, Yves Bertot — 2010
A TUTORIAL OF LUSTRENicolas Halbwachs, Pascal RAYMOND — 2007
The software model checker BlastDirk Beyer, Thomas A. Henzinger, Ranjit Jhala — 2007
Brouwer's Cambridge Lectures on IntuitionismL. E. J. Brouwer, D. van Dalen — 1981
La représentation SSA : sémantique, analyses et implémentation dans GCCSebastian Pop — 2006
Integrating model-based design and preemptive scheduling in mixed time- and event-triggered systemsNorman Scaife, P. Caspi — 2004
The octahedron abstract domainRobert Clarisó, Jordi Cortadella — 2004
Property-directed incremental invariant generationAaron R. Bradley, Zohar Manna — 2008
The Calculus of ConstructionsThierry Coquand, Gérard Huet — 1988
Hoare type theory, polymorphism and separationAleksandar Nanevski, Greg Morrisett, Lars Birkedal — 2008

Cited by

Automatic Coq Proofs Generation from Static Analyzers by Lightweight InstrumentationM. Garnacho, Michaël Périn — 2014

Related papers

No related papers recorded.