Skip to Main content Skip to Navigation

Language-Independent Program Verification Using Symbolic Execution

Andrei Arusoaie 1 Dorel Lucanu 2 Vlad Rusu 3 
3 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Université de Lille, Sciences et Technologies, Inria Lille - Nord Europe, CNRS - Centre National de la Recherche Scientifique
Abstract : We present an automatic, language-independent program verification approach and prototype 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 that offers a lot of freedom to the user regarding the manner and order of rule application, but it lacks a strategy for automatic proof construction. Hence, we propose a procedure for proof construction, in which symbolic execution plays a major role. We prove that, under reasonable conditions on its inputs (the operational semantics of a programming language, and a specification of a program, both given as sets of Reachability Logic formulas) our procedure is partially correct: if it terminates it correctly answers (positively or negatively) to the question of whether the given program specification holds when executing the program according to the given semantics. Termination, of course, cannot be guaranteed, since program-verification is an undecidable problem; but it does happen if the provided set of goals includes enough information in order to be circularly provable (using each other as hypotheses). We introduce a prototype program-verification tool implementing our procedure in the K language-definition framework, and illustrate it by verifying nontrivial programs written in languages defined in K
Document type :
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download
Contributor : Mister Dart Connect in order to contact the contributor
Submitted on : Friday, October 10, 2014 - 8:18:00 AM
Last modification on : Thursday, January 20, 2022 - 5:29:07 PM
Long-term archiving on: : Friday, April 14, 2017 - 1:39:53 PM


Files produced by the author(s)


  • HAL Id : hal-00864341, version 6


Andrei Arusoaie, Dorel Lucanu, Vlad Rusu. Language-Independent Program Verification Using Symbolic Execution. [Research Report] RR-8369, Inria. 2014, pp.28. ⟨hal-00864341v6⟩



Record views


Files downloads