| 1 |
A Generic Framework for Symbolic Execution: a Coinductive Approach
|
|
|
|
In: ISSN: 0747-7171 ; EISSN: 1095-855X ; Journal of Symbolic Computation ; https://hal.inria.fr/hal-01238696 ; Journal of Symbolic Computation, Elsevier, 2017, 80, pp.125-163. ⟨10.1016/j.jsc.2016.07.012⟩ (2017)
|
|
BASE
|
|
Show details
|
|
|
| 2 |
A Generic Framework for Symbolic Execution: Theory and Applications ; Un cadre générique pour l'exécution symbolique : théorie et applications
|
|
|
|
In: https://hal.inria.fr/hal-00766220 ; [Research Report] RR-8189, Inria. 2015, pp.41 (2015)
|
|
BASE
|
|
Show details
|
|
|
| 3 |
Symbolic execution based on language transformation
|
|
|
|
In: ISSN: 1477-8424 ; Computer Languages, Systems and Structures ; https://hal.inria.fr/hal-01186008 ; Computer Languages, Systems and Structures, Elsevier, 2015, pp.42. ⟨10.1016/j.cl.2015.08.004⟩ (2015)
|
|
Abstract:
International audience ; 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 definition is generated, with the same syntax as the original one, but whose semantical rules are transformed in order to rewrite over logical formulas denoting possibly infinite sets of program states. Then, the symbolic execution of concrete programs is, by definition , the execution of the same programs with the symbolic semantics. We prove that the symbolic execution thus defined has the properties naturally expected from it (with respect to concrete program execution). A prototype implementation of our approach was developed in the K Framework. We demonstrate the tool's genericity by instantiating it on several languages, and illustrate it on the reachability analysis and model checking of several programs.
|
|
Keyword:
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]; [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]; formal semantics; program analysis; programming languages; symbolic execution
|
|
URL: https://doi.org/10.1016/j.cl.2015.08.004
https://hal.inria.fr/hal-01186008/file/clss2015.pdf
https://hal.inria.fr/hal-01186008/document
https://hal.inria.fr/hal-01186008
|
|
BASE
|
|
Hide details
|
|
|
| 4 |
A Generic Framework for Symbolic Execution
|
|
|
|
In: 6th International Conference on Software Language Engineering ; https://hal.inria.fr/hal-00853588 ; 6th International Conference on Software Language Engineering, Oct 2013, Indianapolis, United States. pp.281-301 (2013)
|
|
BASE
|
|
Show details
|
|
|
| 5 |
Formally Tracing Executions From an Analysis Tool Back to a Domain Specific Modeling Language's Operational Semantics
|
|
|
|
In: https://hal.inria.fr/inria-00526561 ; [Research Report] RR-7423, INRIA. 2010 (2010)
|
|
BASE
|
|
Show details
|
|
|
|
|
