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 :
Reports
Complete list of metadatas

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-00864341
Contributor : Mister Dart <>
Submitted on : Friday, October 10, 2014 - 8:18:00 AM
Last modification on : Thursday, February 21, 2019 - 10:34:09 AM
Long-term archiving on: Friday, April 14, 2017 - 1:39:53 PM

File

jfla2015-techreport.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00864341, version 6

Citation

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

Share

Metrics

Record views

317

Files downloads

174