A Generic Framework for Symbolic Execution:Theory and Applications: Theory and Applications

Andrei Arusoaie 1, 2
1 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 : Symbolic execution is one of the most popular techniques used for analyzing programs. It has been used especially for test case generation, but there exist several other applications (e.g. program verification, program debugging, etc.).The doctoral thesis titled A language-independent approach for symbolic execution: theory and applications presents a generic framework for symbolic execution, where the genericity is given by the fact that this framework is based on formal definitions of programming languages. This is an advantage because symbolic execution is implemented at the level of the language definition and is not based on the syntax or on the compiler of a particular language. In this thesis, the symbolic execution framework is formally presented, using algebraic specifications. This allows proving some important properties of symbolic execution:Coverage: for each concrete execution there exists a corresponding symbolic execution on the same program (execution) path. Precision: for each symbolic execution there exists a concrete execution on the same program (execution) path.These two properties are important because, in the case in which, after analyzing a program, certain results are obtained about symbolic executions, they ensure that the results can be correctly transferred to the concrete executions. Moreover, because of these properties, the symbolic execution framework that we propose can be used for program verification.ContributionsThe major contributions of this doctoral thesis are:A formal framework for symbolic execution and an implementation thereof, based on the operational semantics of programming languages:on the theoretical side, we formally define programming languages and symbolic execution and then we prove formally the properties of Coverage and Precision;on the practical side, we present a prototype of this symbolic framework that is implemented on top of the K framework for language definitions and which is based on language transformations;Applications of symbolic execution in program verification:program verification based on Hoare logic, where we show how symbolic execution can be used to verify Hoare triples for a given programming language;program verification based on Reachability Logic, where we present an alternative proof system for Reachability Logic and an inference rule application strategy that allows to automate the checking of Reachability Logic formulae; for this proof system and for the proposed strategy, we have implemented a prototype and we have shown soundness (based on the soundness of the Reachability Logic proof system) and a form of weak completeness (for proving formulae to be false).
Liste complète des métadonnées

Cited literature [109 references]  Display  Hide  Download

https://hal.inria.fr/tel-01094765
Contributor : Pal Dream <>
Submitted on : Tuesday, January 13, 2015 - 11:22:40 AM
Last modification on : Thursday, February 21, 2019 - 10:34:09 AM
Document(s) archivé(s) le : Thursday, September 10, 2015 - 11:35:27 PM

Identifiers

  • HAL Id : tel-01094765, version 1

Collections

Citation

Andrei Arusoaie. A Generic Framework for Symbolic Execution:Theory and Applications: Theory and Applications. Computer Science [cs]. Alexandru Ioan Cuza, University of Iasi, 2014. English. ⟨tel-01094765⟩

Share

Metrics

Record views

375

Files downloads

638