Symbolic execution based on language transformation.(English)Zbl 1387.68047

Summary: 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 $$\mathbb{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.

MSC:

 68N15 Theory of programming languages 68Q55 Semantics in the theory of computing

Software:

STP; K tool; KLOVERA; K Prover; K-Java; KOOL; CUTE; DART; Maude; Pex; z3
Full Text:

References:

 [1] Armando A, Benerecetti M, Mantovani J. Model checking linear programs with arrays. In: Proceedings of the workshop on software model checking, vol. 144(3), 2006. p. 79-94. [2] Arusoaie A, Lucanu D, Rusu V. A generic framework for symbolic execution. In: 6th international conference on software language engineering. Lecture notes in computer science, vol. 8225. Indianapolis, USA: Springer Verlag; 2013. p. 281-301. Also available as a technical report, http://hal.inria.fr/hal-00853588. [3] Arusoaie, A.; Lucanu, D.; Rusu, V., Towards a semantics for OCL, Electron Notes Theor Comput Sci, 304, 81-96, (2014), (Proceedings of the second international workshop on the K framework and its applications (K 2011)) [4] Arusoaie A, Lucanu D, Rusu V, Şerbănuţă TF, Ştefănescu A, Roşu G. Language definitions as rewrite theories. In: Proceedings of the 10th international workshop on rewriting logic and its applications (WRLA׳14). Lecture notes in computer science, vol. 8663. Grenoble, France: Springer; 2014. p. 97-112. [5] Baader, F.; Nipkow, T., Term rewriting and all that, (1998), Cambridge University Press New York, NY, USA [6] Berdine J, Calcagno C, O׳Hearn PW. Symbolic execution with separation logic. In: APLAS, 2005. p. 52-68. · Zbl 1159.68363 [7] Bogdănaş D, Roşu G. K-java: a complete semantics of java. In: Proceedings of the 42nd symposium on principles of programming languages (POPL׳15). Mumbay, India ACM, 2015. [8] Cadar C, Ganesh V, Pawlowski PM, Dill DL, Engler DR. EXE: automatically generating inputs of death. New York, USA, In: Juels A, Wright RN, di Vimercati SDC, editors. ACM conference on computer and communications security. ACM, 2006. p. 322-35. [9] Clavel M, Durán F, Eker S, Meseguer J, Lincoln P, Martí-Oliet N, et al. All about Maude, a high-performance logical framework. Lecture notes in computer science, vol. 4350. Springer; 2007. · Zbl 1115.68046 [10] de Halleux J, Tillmann N. Parameterized unit testing with Pex. In: TAP. Lecture notes in computer science, vol. 4966. Springer; 2008. p. 171-81. [11] de Moura, L. M.; Bjørner, N., Z3an efficient SMT solver, (Ramakrishnan, C. R.; Rehof, J., TACAS. Lecture notes in computer science, vol. 4963, (2008), Springer Berlin, Germany), 337-340 [12] Dillon L.Verifying general safety properties of Ada tasking programs. IEEE Trans. Softw. Eng. 1990;16 (January (1)):51-63. [13] Ellison C, Roşu G. An executable formal semantics of C with applications. In: ACM SIGPLAN notices, vol. 47. New York, USA: ACM; 2012. p. 533-44. [14] Escobar, S.; Meseguer, J.; Sasse, R., Variant narrowing and equational unification, Electron. Notes Theor. Comput. Sci., 238, 3, 103-119, (2009), (Proceedings of the 7th international workshop on rewriting logic and its applications (WRLA׳08)) · Zbl 1347.68194 [15] Filaretti D, Maffeis S. An executable formal semantics of PHP. In: Jones R. editor. Proceedings of European conference on object-oriented programming. Lecture notes in computer science. Berlin, Heidelberg: Springer; 2014. p. 567-92. [16] Godefroid P, Klarlund N, Sen K. DART: directed automated random testing. In: Sarkar V, Hall MW. editors. PLDI. New York, USA: ACM; 2005. p. 213-23. [17] Hills M, Roşu G. Kool: an application of rewriting logic to language prototyping and analysis. Paris, France, In: RTA, Lecture notes in computer science, vol. 4533. Paris, France: Springer; 2007. p. 246-56. [18] Khurshid, S.; Păsăreanu, C. S.; Visser, W., Generalized symbolic execution for model checking and testing, (Garavel, H.; Hatcliff, J., TACAS. Lecture notes in computer science, vol. 2619, (2003), Springer Warsaw, Poland), 553-568 · Zbl 1031.68519 [19] King, J. C., Symbolic execution and program testing, Commun ACM, 19, 7, 385-394, (1976) · Zbl 0329.68018 [20] Li, G.; Ghosh, I.; Rajan, S. P., KLOVERA symbolic execution and automatic test generation tool for C++ programs, (Gopalakrishnan, G.; Qadeer, S., CAV. Lecture notes in computer science, vol. 6806, (2011), Springer), 609-615 [21] Lucanu D, Rusu V, Arusoaie A, Nowak D. Verifying reachability-logic properties on rewriting-logic specifications. In: Logic, rewriting, and concurrency - Festschrift Symposium in Honor of José Meseguer, 2015 to appear. Also available as a technical report, http://www.infoiasi.ro/ tr/tr.pl.cgi. [22] Lucanu D, Şerbănuţă TF, Roşu G. The K Framework distilled. In: 9th international workshop on rewriting logic and its applications (WRLA׳12). Lecture notes in computer science, vol. 7571. Tallinn, Estonia, Springer; 2012. p. 31-53 (Invited talk). [23] Meseguer, J.; Thati, P., Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, Higher-Order Symb Comput, 20, 1-2, 123-160, (2007) · Zbl 1115.68079 [24] Păsăreanu, C. S.; Visser, W., Verification of Java programs using symbolic execution and invariant generation, (Graf, S.; Mounier, L., SPIN. Lecture notes in computer science, vol. 2989, (2004), Springer Barcelona, Spain), 164-181 · Zbl 1125.68367 [25] Păsăreanu, C. S.; Visser, W., A survey of new trends in symbolic execution for software testing and analysis, Softw Tools Technol Transf, 11, 4, 339-353, (2009) [26] Pecheur C, Andrews J, Nitto ED. editors. ASE 2010, 25th IEEE/ACM international conference on automated software engineering, Antwerp, Belgium, September 20-24. ACM; 2010. [27] Rocha C, Meseguer J, Muñoz CA. Rewriting modulo SMT and open system analysis. In: Proceedings of the 10th international workshop on rewriting logic and its applications (WRLA׳14). Lecture notes in computer science, vol. 8663. Grenoble, France: Springer, 2014. p. 247-62. [28] Roşu G, Ştefănescu A, Ciobâcă Ş, Moore BM. One-path reachability logic. New Orleans, LA, USA, In: Proceedings of the 28th symposium on logic in computer science (LICS׳13). IEEE; June 2013. p. 358-67. [29] Roşu, G.; Şerbănuţă, T. F., An overview of the K semantic framework, J Logic Algebraic Program, 79, 6, 397-434, (2010) · Zbl 1214.68188 [30] Roşu G, Ştefănescu A. Checking reachability using matching logic. In: Proceedings of the 27th conference on object-oriented programming, systems, languages, and applications (OOPSLA׳12). Huston, Arizona: ACM; 2012. p. 555-74. [31] Roşu G, Ştefănescu A. From Hoare logic to matching logic reachability. In: Proceedings of the 18th international symposium on formal methods (FM׳12). Lecture notes in computer science, vol. 7436. Paris, France: Springer; 2012. p. 387-402. · Zbl 1372.68066 [32] Sannella D, Tarlecki A. Foundations of algebraic specification and formal software development. Monographs in theoretical computer science. An EATCS series. Springer; 2012. · Zbl 1237.68129 [33] Schmitt PH, Weiß B. Inferring invariants by symbolic execution. In: Proceedings of 4th international verification workshop (VERIFY׳07), 2007. [34] Sen K, Marinov D, Agha G. CUTE: a concolic unit testing engine for C. In: Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on foundations of software engineering, ESEC/FSE-13. New York, NY, USA: ACM; 2005. p. 263-72. [35] Şerbănuţă TF, Arusoaie A, Lazăr D, Ellison C, Lucanu D, Roşu G. The K primer (version 3.3). In Hills M, editor. Proceedings of the second international workshop on the K framework and its applications (K׳11), vol. 304, 2014. p. 57-80. [36] Şerbănuţă, T.-F.; Roşu, G.; Meseguer, J., A rewriting logic approach to operational semantics, Inf Comput, 207, 305-340, (2009) · Zbl 1165.68041 [37] Siegel SF, Mironova A, Avrunin GS, Clarke LA. Using model checking with symbolic execution to verify parallel numerical programs. In: Pollock LL, Pezzè M. editors. ISSTA. ACM; 2006. p. 157-68. [38] Staats M, Păsăreanu CS. Parallel symbolic execution for structural test generation. In: Tonella P, Orso A, editors. ISSTA. Trento, Italy ACM; 2010. p. 183-94. [39] Yi K. editor. Programming languages and systems, third Asian symposium, APLAS 2005, Proceedings. Lecture notes in computer science, Tsukuba, Japan, November 2-5, 2005, vol. 3780. Springer; 2005.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.