Language-Independent Program Verification Using Symbolic Execution

Arusoaie, Andrei, Lucanu, Dorel, Rusu, Vlad. Language-Independent Program Verification Using Symbolic Execution. Rapport de recherche RR-8369, INRIA, Sep 2013.


We present an automatic, language-independent program verification approach and experimental tool based on symbolic execution. The program-specification formalism we consider is Reachability Logic, a language-independent alternative to Hoare logics. Reachability Logic has a sound and relatively complete deduction system, which offers a lot of freedom (but very few guidelines) for constructing proofs. Hence, we propose in this paper an alternative proof system, in which symbolic execution becomes a rule for proof construction. We show that under reasonable conditions on the semantics of programming languages our proof system is sound. We then present a Reachability-Logic verifier based on our proof system, which is implemented in the K framework and illustrated on programs written in languages also defined in K.

link to PDF :