FMSE
Formal
Methods in
Software Engineering
Talks for Andrei Arusoaie Talks for Dorel Lucanu Talks for Vlad Rusu Symbolic Execution in the K ... Anonymous  Login
Symbolic Execution in the K Framework: Support and Applications
Andrei Arusoaie   Dorel Lucanu   Vlad Rusu  
PAS 2013 - Second International Seminar on Program Verification, Automated Debugging and Symbolic Computation Beijing, China, October 23-25, 2013,   2013  
Abstract:

K (www.kframework.org) is an executable semantic framework for defining operational semantics of programming languages, type systems, and formal analysis tools. The K toolbox includes two main tools: the compiler and the runner. The K definition of a language, say, L, is compiled into a rewrite system. Then, the K runner executes programs in L by applying the resulting rewrite rules to configurations containing programs. Beside some simple languages used for teaching, there are a few real-word programming languages, supporting different paradigms, that have been successfully defined in K: C, Python, Java, OCaml. In [1] a symbolic execution language-independent framework is defined and a prototype of this is implemented in K. This implementation extends the K compiler with a new feature that builds a "symbolic semantics" of the language, which is able to execute programs having symbolic values as inputs. The new semantics is automatically generated from the initial K definition of the language by reusing components of the K framework: parsing, compilation steps, support for symbolic execution, and the connections to the Maude’s model-checker and the Z3 SMT solver. The result of the symbolic execution consists in a set of logical constrained configurations corresponding to different program paths. In this talk we briefly present the K framework, its symbolic execution support and how the symbolic execution is used for program analysis. In particular, we show how the existing analysis tools (e.g., the model-checker) can be used together with the symbolic semantics and how the symbolic exception mechanism can be extended to verify properties expressed as Reachability Logic formulas [2].

References

1. A. Arusoaie, D. Lucanu, and V. Rusu. A generic framework for symbolic execution. In 6th International Conference on Software Language Engineering, volume 8225 of LNCS, pages 281–301. Springer Verlag, 2013. Also available as a technical report at http://hal.inria.fr/hal-00766220/.

2. A. Arusoaie, D. Lucanu, and V. Rusu. Language-Independent Program Verification Using Symbolic Execution. Rapport de recherche RR-8369, INRIA, Sept. 2013. http://hal.inria.fr/hal-00864341/.

Project(s):    K
Grant(s):    DAK
NEWS
New publication : Model checking recursive programs interacting via ... - 01 feb 2015

Almost all modern imperative programming languages include operations for dynamically manipulating the heap, for example by allocating and deallocating objects, and by updating reference fields. In the presence of recursive ... (more)


New publication : K-Java: A Complete Semantics of Java - 10 sep 2014

This paper presents K-Java, a complete executable formal semantics of Java 1.4.
K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology.
more)


New publication : K-Java: A Complete Semantics of Java - 09 jul 2014

This paper presents K-Java, a complete executable formal semantics of Java 1.4.
K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology.
more)


New publication : Engineering Hoare Logic-based Program Verification in ... - 30 oct 2013

We propose a language-independent symbolic execution framework for languages endowed with a formal operational semantics based on term rewriting. Starting from a given definition of a language, a new language ... (more)


New talk: PAS 2013 - 20 oct 2013

Dorel lucanu will give a talk at PAS 2013.

(more)

     Archive

@FMSE 2010-2011