A generic framework for symbolic execution: a coinductive approach.

*(English)*Zbl 1356.68044Summary: We propose a language-independent symbolic execution framework. The approach is parameterised by a language definition, which consists of a signature for the syntax and execution infrastructure of the language, a model interpreting the signature, and rewrite rules for the language’s operational semantics. Then, symbolic execution amounts to computing symbolic paths using a derivative operation. We prove that the symbolic execution thus defined has the properties naturally expected from it, meaning that the feasible symbolic executions of a program and the concrete executions of the same program mutually simulate each other. We also show how a coinduction-based extension of symbolic execution can be used for the deductive verification of programs. We show how the proposed symbolic-execution approach, and the coinductive verification technique based on it, can be seamlessly implemented in language definition frameworks based on rewriting such as the \(\mathbb{K}\) framework. A prototype implementation of our approach has been developed in \(\mathbb{K}\). We illustrate it on the symbolic analysis and deductive verification of nontrivial programs.

##### MSC:

68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |

68Q55 | Semantics in the theory of computing |

68W30 | Symbolic computation and algebraic computation |

##### Keywords:

symbolic execution; programming language; formal operational semantics; reachability logic; circular coinduction; program verification##### Software:

CIRC; Coq; CUTE; DART; KLEE; K Prover; Maude; Pex; Spec#; STP; TRACER; VeriFast; Why3; WhyML; z3
PDF
BibTeX
XML
Cite

\textit{D. Lucanu} et al., J. Symb. Comput. 80, Part 1, 125--163 (2017; Zbl 1356.68044)

Full Text:
DOI

##### References:

[1] | Ahrendt, W., The key tool, Softw. Syst. Model., 4, 32-54, (2005) |

[2] | Armando, Alessandro; Benerecetti, Massimo; Mantovani, Jacopo, Model checking linear programs with arrays, Electron. Notes Theor. Comput. Sci., 144, 3, 79-94, (2006) |

[3] | Arusoaie, Andrei; Lucanu, Dorel; Rusu, Vlad, A generic framework for symbolic execution, (6th International Conference on Software Language Engineering, Lecture Notes in Computer Science, vol. 8225, (2013), Springer Verlag), 281-301, Also available as a technical report at · Zbl 1356.68044 |

[4] | Arusoaie, Andrei; Lucanu, Dorel; Rusu, Vlad, Symbolic execution based on language transformation, Comput. Lang. Syst. Struct., 44, 48-71, (2015) · Zbl 1321.68359 |

[5] | Barnett, Mike; Rustan, K.; Leino, M.; Schulte, Wolfram, The spec# programming system: an overview, (Proc. 2004 International Conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS’04, (2005)), 49-69 |

[6] | Berdine, Josh; Calcagno, Cristiano; O’Hearn, Peter W., Symbolic execution with separation logic, (Programming Languages and Systems, Third Asian Symposium, APLAS, Lecture Notes in Computer Science, vol. 3780, (2005), Springer), 52-68 · Zbl 1159.68363 |

[7] | Cadar, Cristian; Dunbar, Daniel; Engler, Dawson, Klee: unassisted and automatic generation of high-coverage tests for complex systems programs, (Proc. 8th USENIX Conference on Operating Systems Design and Implementation, OSDI’08, (2008)), 209-224 |

[8] | Cadar, Cristian; Ganesh, Vijay; Pawlowski, Peter M.; Dill, David L.; Engler, Dawson R., EXE: automatically generating inputs of death, (ACM Conference on Computer and Communications Security, (2006)), 322-335 |

[9] | Clarke, Edmund; Kroening, Daniel, Hardware verification using ANSI-C programs as a reference, (Proceedings of the 2003 Asia and South Pacific Design Automation Conference, ASP-DAC ’03, (2003), ACM New York, NY, USA), 308-311 |

[10] | Clavel, Manuel; Durán, Francisco; Eker, Steven; Lincoln, Patrick; Oliet, Narciso M.; Meseguer, Jos’e; Talcott, Carolyn, All about maude—A high-performance logical framework: how to specify, program, and verify systems in rewriting logic, Lecture Notes in Computer Science, (2007), Springer · Zbl 1115.68046 |

[11] | Coen-Porisini, Alberto; Denaro, Giovanni; Ghezzi, Carlo; Pezzé, Mauro, Using symbolic execution for verifying safety-critical systems, Softw. Eng. Notes, 26, 5, 142-151, (2001) |

[12] | Cormen, Thomas H.; Leiserson, Charles E.; Rivest, Ronald L.; Stein, Clifford, Introduction to algorithms, (2009), MIT Press · Zbl 1187.68679 |

[13] | Ştefănescu, Andrei; Ciobâcă, Ştefan; Mereuţă, Radu; Moore, Brandon M.; Şerbănuţă, Traian Florin; Roşu, Grigore, All-path reachability logic, (Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, RTA-TLCA’14, Lecture Notes in Computer Science, vol. 8560, (July 2014), Springer), 425-440 · Zbl 1416.68052 |

[14] | Cui, Heming; Hu, Gang; Wu, Jingyue; Yang, Junfeng, Verifying systems rules using rule-directed symbolic execution, ACM SIGPLAN Not., 48, 4, 329-342, (March 2013) |

[15] | de Halleux, Jonathan; Tillmann, Nikolai, Parameterized unit testing with pex, (Tests and Proofs, Second International Conference, Lecture Notes in Computer Science, vol. 4966, (2008), Springer), 171-181 |

[16] | de Moura, Leonardo; Bjørner, Nikolaj, Z3: an efficient SMT solver, (Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS’08, Lecture Notes in Computer Science, vol. 4963, (2008), Springer), 337-340 |

[17] | Escobar, Santiago; Meseguer, José; Sasse, Ralf, Variant narrowing and equational unification, Electron. Notes Theor. Comput. Sci., 238, 3, 103-119, (2009) · Zbl 1347.68194 |

[18] | Filliâtre, Jean Christophe, Proof of KMP string searching algorithm, (1998) |

[19] | Filliâtre, Jean-Christophe; Paskevich, Andrei, Why3—where programs meet provers, (Proceedings of the 22nd European Symposium on Programming, Lecture Notes in Computer Science, vol. 7792, (March 2013), Springer), 125-128 |

[20] | Godefroid, Patrice; Klarlund, Nils; Sen, Koushik, DART: directed automated random testing, (Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, (2005), ACM), 213-223 |

[21] | Harel, David; Kozen, Dexter; Tiuryn, Jerzy, Dynamic logic, (Handbook of Philosophical Logic, (1984), MIT Press), 497-604 · Zbl 0875.03076 |

[22] | Jacobs, Bart; Smans, Jan; Piessens, Frank, A quick tour of the verifast program verifier, (Proceedings of the 8th Asian Conference on Programming Languages and Systems, APLAS’10, (2010), Springer-Verlag Berlin/Heidelberg), 304-311 |

[23] | Jaffar, Joxan; Murali, Vijayaraghavan; Navas, Jorge A.; Santosa, Andrew E., TRACER: a symbolic execution tool for verification, (Computer Aided Verification—24th International Conference, 2012 Proceedings, CAV 2012, Berkeley, CA, USA, July 7-13, Lecture Notes in Computer Science, (2012), Springer), 758-766 |

[24] | King, James C., Symbolic execution and program testing, Commun. ACM, 19, 7, 385-394, (1976) · Zbl 0329.68018 |

[25] | Knuth, Donald E.; Morris, J. H.; Pratt, Vaughan R., Fast pattern matching in strings, SIAM J. Comput., 6, 2, 323-350, (1977) · Zbl 0372.68005 |

[26] | Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei; Nowak, David, Verifying reachability-logic properties on rewriting-logic specifications, (Logic, Rewriting, and Concurrency—Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday, Lecture Notes in Computer Science, vol. 9200, (2015), Springer), 451-474 · Zbl 1321.68359 |

[27] | Lucanu, Dorel; Şerbănuţă, Traian-Florin, Cink—an exercise on how to think in K, (December 2013), Alexandru Ioan Cuza University, Faculty of Computer Science, Technical Report TR 12-03, Version 2 |

[28] | The Coq development team. The Coq proof assistant reference manual. LogiCal Project 2004. Version 8.0. |

[29] | Meseguer, José; Thati, Prasanna, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, High.-Order Symb. Comput., 20, 1-2, 123-160, (2007) · Zbl 1115.68079 |

[30] | Moore, Brandon; Roşu, Grigore, Program verification by coinduction, (February 2015), University of Illinois, Technical report |

[31] | Moss, Lawrence S.; Danner, Norman, On the foundations of corecursion, Log. J. IGPL, 5, 2, 231-257, (1997) · Zbl 0872.03030 |

[32] | Păsăreanu, Corina S.; Rungta, Neha, Symbolic pathfinder: symbolic execution of Java bytecode, (International Conference on Automated Software Engineering, ASE’10, (2010), ACM), 179-180 |

[33] | Păsăreanu, Corina S.; Visser, Willem, Verification of Java programs using symbolic execution and invariant generation, (SPIN, Lecture Notes in Computer Science, vol. 2989, (2004), Springer), 164-181 · Zbl 1125.68367 |

[34] | Păsăreanu, Corina S.; Visser, Willem, A survey of new trends in symbolic execution for software testing and analysis, Int. J. Softw. Tools Technol. Transf., 11, 4, 339-353, (2009) |

[35] | Ramos, David A.; Engler, Dawson R., Practical, low-effort equivalence verification of real code, (Proceedings of the 23rd International Conference on Computer Aided Verification, CAV’11, (2011), Springer-Verlag Berlin/Heidelberg), 669-685 |

[36] | Reynolds, John C., Separation logic: a logic for shared mutable data structures, (Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS ’02, (2002), IEEE Computer Society Washington, DC, USA), 55-74 |

[37] | Rocha, Camilo; Meseguer, José; Muñoz, César A., Rewriting modulo SMT and open system analysis, (Rewriting Logic and Its Applications—10th International Workshop, WRLA 2014, Revised Selected Papers, Lecture Notes in Computer Science, vol. 8663, (2014), Springer), 247-262 · Zbl 1367.68151 |

[38] | Roşu, Grigore, Matching logic—extended abstract, (Proceedings of the 26th International Conference on Rewriting Techniques and Applications, RTA’15, Leibniz International Proceedings in Informatics (LIPIcs), vol. 36, (July 2015), Dagstuhl Germany), 5-21, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik · Zbl 1366.68027 |

[39] | Roşu, Grigore; Ştefănescu, Andrei, From Hoare logic to matching logic reachability, (Proceedings of the 18th International Symposium on Formal Methods, FM’12, Lecture Notes in Computer Science, vol. 7436, (2012), Springer), 387-402 · Zbl 1372.68066 |

[40] | Roşu, Grigore; Ştefănescu, Andrei; Ciobâcă, Ştefan; Moore, Brandon M., One-path reachability logic, (Proceedings of the 28th Symposium on Logic in Computer Science, LICS’13, (June 2013), IEEE), 358-367 · Zbl 1366.68182 |

[41] | Roşu, Grigore; Lucanu, Dorel, Circular coinduction—a proof theoretical foundation, (CALCO 2009, Lecture Notes in Computer Science, vol. 5728, (2009), Springer), 127-144 · Zbl 1239.68067 |

[42] | Roşu, Grigore; Şerbănuţă, Traian Florin, An overview of the K semantic framework, J. Log. Algebraic Program., 79, 6, 397-434, (2010) · Zbl 1214.68188 |

[43] | Roşu, Grigore; Ştefănescu, Andrei, Checking reachability using matching logic, (OOPSLA, (2012), ACM), 555-574, Also available as technical report · Zbl 1372.68066 |

[44] | Rusu, Vlad; Lucanu, Dorel; Serbanuta, Traian Florin; Arusoaie, Andrei; Ştefănescu, Andrei; Roşu, Grigore, Language definitions as rewrite theories, J. Log. Algebraic Methods Program., 85, 1, Part 1, 1:98-120, (2016) · Zbl 1356.68125 |

[45] | Sangiorgi, Davide, An introduction to bisimulation and coinduction, (2012), Cambridge University Press, A preliminary version of Chapter 2 from which we adapt paterial can be found at · Zbl 1252.68008 |

[46] | Schmitt, Peter H.; Weiß, Benjamin, Inferring invariants by symbolic execution, (VERIFY, CEUR Workshop Proceedings, vol. 259, (2007), CEUR-WS.org) |

[47] | Sen, Koushik; Marinov, Darko; Agha, Gul, CUTE: a concolic unit testing engine for C, (Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC/FSE-13, (2005), ACM New York, NY, USA), 263-272 |

[48] | Şerbănuţă, Traian-Florin; Roşu, Grigore; Meseguer, José, A rewriting logic approach to operational semantics, Inf. Comput., 207, 2, 305-340, (2009) · Zbl 1165.68041 |

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.