Sciweavers

TGC
2010
Springer

Certified Result Checking for Polyhedral Analysis of Bytecode Programs

13 years 8 months ago
Certified Result Checking for Polyhedral Analysis of Bytecode Programs
Static analysers are becoming so complex that it is crucial to ascertain the soundness of their results in a provable way. In this paper we develop a certified checker in Coq that is able to certify the results of a polyhedral array-bound analysis for an imperative, stack-oriented bytecode language with procedures, arrays and global variables. The checker uses, in addition to the analysis result, certificates which at the same time improve efficiency and make correctness proofs much easier. In particular, our result certifier avoids complex polyhedral computations such as convex hulls and is using easily checkable inclusion certificates based on Farkas lemma. Benchmarks demonstrate that our approach is effective and produces certificates that can be efficiently checked not only by an extracted Caml checker but also directly in Coq.
Frédéric Besson, Thomas P. Jensen, D
Added 15 Feb 2011
Updated 15 Feb 2011
Type Journal
Year 2010
Where TGC
Authors Frédéric Besson, Thomas P. Jensen, David Pichardie, Tiphaine Turpin
Comments (0)