These written and oral presentations, and all the material contained within, are protected by copyright law.
Élagage d'invariants de programmes - Pruning program invariants
2008 December, 15
166 pages
Language: French, English
Team(s): LANDE
Summary:
This thesis addresses the generation of certificates for Proof-Carrying Code that are both small and easy to check. We propose methods for obtaining small witnesses of a safety property in the context of Abstraction-Carrying Code. In the distributive case, the weakest witness (i.e., the smallest) may be computed. For the general case, we propose a pruning technique for weakening a given witness. This technique is applied to the abstract domain of convex polyhedra, in the intraprocedural and then interprocedural case. Another application is presented, which allows the lightweight bytecode verification to be enriched by including interface method calls, without making the checker more complex. We present various reconstruction algorithms which generalise existing checking algorithms. Finally, to facilitate the use of Binary Decision Diagrams in static analysis (and thus for Abstraction-Carrying Code), we prove the soundness of a relational formulation of the least fixpoint semantics of definite range-restricted logic programs.