Certification of static analysis in many-sorted first-order logic
L'analyse statique est utilisée pour vérifier de manière formelle qu'un programme ne fait pas d'erreurs, mais un analyseur statique est lui même un programme complexe sujet aux erreurs. Une analyse statique formalisée comme un interpreteur abstrait peut être prouvée correcte, cependan...
Main Author: | Cornilleau, Pierre-Emmanuel |
---|---|
Other Authors: | Cachan, Ecole normale supérieure |
Language: | en |
Published: |
2013
|
Subjects: | |
Online Access: | http://www.theses.fr/2013DENS0012/document |
Similar Items
-
Certification of static analysis in many-sorted first-order logic
by: Cornilleau, Pierre-Emmanuel
Published: (2013) -
A Framework for Autonomous Generation of Strategies in Satisfiability Modulo Theories
by: Galvez Ramirez, Nicolas
Published: (2018) -
Finding inductive invariants using satisfiability modulo theories and convex optimization
by: Karpenkov, George Egor
Published: (2017) -
Automated deduction and proof certification for the B method
by: Halmagrand, Pierre
Published: (2016) -
First-order stable model semantics with intensional functions
by: Bartholomew, M., et al.
Published: (2019)