×

zbMATH — the first resource for mathematics

Executing and verifying higher-order functional-imperative programs in Maude. (English) Zbl 1372.68056
Summary: We incorporate higher-order functions and state monads in Maude, thereby embedding a higher-order functional language with imperative features in the Maude framework. We illustrate, via simple programs in the resulting language: the concrete and symbolic execution of programs; their verification with respect to properties expressed in Reachability Logic, a language-parametric generalisation of Hoare Logic; and the verification of program-equivalence properties. Our approach is proved sound and is implemented in Full Maude by taking advantage of its reflective features and module system.
MSC:
68N18 Functional programming and lambda calculus
03B70 Logic in computer science
Software:
Coq; CUTE; DART; KLEE; Maude; Pex; STP; TRACER
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C., All about maude—A high-performance logical framework: how to specify, program and verify systems in rewriting logic, (2007), Springer-Verlag · Zbl 1115.68046
[2] The Haskell language · Zbl 1289.68010
[3] Roşu, G.; Ştefănescu, A., Towards a unified theory of operational and axiomatic semantics, (Proceedings of the 39th International Colloquium on Automata, Languages and Programming, ICALP’12, Lecture Notes in Computer Science, vol. 7392, (2012), Springer), 351-363 · Zbl 1367.68075
[4] Roşu, G.; Ştefănescu, A., Checking reachability using matching logic, (Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA’12, (2012), ACM), 555-574
[5] Roşu, G.; Ştefănescu, A.; Ciobâcă, Ş.; Moore, B. M., One-path reachability logic, (Proceedings of the 28th Symposium on Logic in Computer Science, LICS’13, (2013), IEEE), 358-367 · Zbl 1366.68182
[6] Ştefănescu, A.; Ciobâcă, Ş.; Mereuţă, R.; Moore, B. M.; Şerbănuţă, T. F.; Roşu, G., 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, LNCS, vol. 8560, (2014), Springer), 425-440 · Zbl 1416.68052
[7] The coq proof assistant · Zbl 1342.68280
[8] Swierstra, W., A Hoare logic for the state monad, (Berghofer, S.; Nipkow, T.; Urban, C.; Wenzel, M., Theorem Proving in Higher Order Logics, Proceedings of the 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009, Lecture Notes in Computer Science, vol. 5674, (2009), Springer), 440-451 · Zbl 1252.68067
[9] Ştefănescu, A.; Park, D.; Yuwen, S.; Li, Y.; Roşu, G., Semantics-based program verifiers for all languages, (Proceedings of the 31th Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA’16, (2016), ACM)
[10] The \(\mathbb{K}\) semantic framework
[11] Lucanu, D.; Rusu, V.; Arusoaie, A., A generic framework for symbolic execution: a coinductive approach, J. Symb. Comput. · Zbl 1356.68044
[12] Rusu, V.; Lucanu, D.; Serbanuta, T.; Arusoaie, A.; Stefanescu, A.; Rosu, G., Language definitions as rewrite theories, J. Log. Algebraic Methods Program., 85, 1, 98-120, (2016) · Zbl 1356.68125
[13] Ciobâcă, Ştefan; Lucanu, D.; Rusu, V.; Rosu, G., A language-independent proof system for full program equivalence, Form. Asp. Comput., 28, 3, 469-497, (2016) · Zbl 1355.68051
[14] Arusoaie, A.; Lucanu, D.; Rusu, V., Symbolic execution based on language transformation, Comput. Lang. Syst. Struct., 44, 48-71, (2015) · Zbl 1387.68047
[15] Lucanu, D.; Rusu, V., Program equivalence by circular reasoning, Form. Asp. Comput., 27, 4, 701-726, (2015) · Zbl 1319.68060
[16] King, J. C., Symbolic execution and program testing, Commun. ACM, 19, 7, 385-394, (1976) · Zbl 0329.68018
[17] Păsăreanu, C. S.; Rungta, N., Symbolic pathfinder: symbolic execution of Java bytecode, (International Conference on Automated Software Engineering, ASE’10, (2010), ACM), 179-180
[18] Godefroid, P.; Klarlund, N.; Sen, K., DART: directed automated random testing, (Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, (2005), ACM), 213-223
[19] Sen, K.; Marinov, D.; Agha, G., 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
[20] Cadar, C.; Ganesh, V.; Pawlowski, P. M.; Dill, D. L.; Engler, D. R., EXE: automatically generating inputs of death, (ACM Conference on Computer and Communications Security, (2006)), 322-335
[21] de Halleux, J.; Tillmann, N., Parameterized unit testing with pex, (Tests and Proofs, Second International Conference, Lecture Notes in Computer Science, vol. 4966, (2008), Springer), 171-181
[22] Cadar, C.; Dunbar, D.; Engler, D., 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
[23] Coen-Porisini, A.; Denaro, G.; Ghezzi, C.; Pezzé, M., Using symbolic execution for verifying safety-critical systems, Softw. Eng. Notes, 26, 5, 142-151, (2001)
[24] Jaffar, J.; Murali, V.; Navas, J. A.; Santosa, A. E., TRACER: a symbolic execution tool for verification, (Computer Aided Verification—Proceedings of the 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012, Lecture Notes in Computer Science, vol. 7358, (2012), Springer), 758-766
[25] Ramos, D. A.; Engler, D. 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
[26] Leroy, X., Formal verification of a realistic compiler, Commun. ACM, 52, 7, 107-115, (2009)
[27] Necula, G. C., Translation validation for an optimizing compiler, (Lam, M. S., PLDI, (2000), ACM), 83-94
[28] Pitts, A. M., Operational semantics and program equivalence, (Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, (2002), Springer-Verlag London, UK, UK), 378-412 · Zbl 1065.68067
[29] Arons, T.; Elster, E.; Fix, L.; Mador-Haim, S.; Mishaeli, M.; Shalev, J.; Singerman, E.; Tiemeyer, A.; Vardi, M. Y.; Zuck, L. D., Formal verification of backward compatibility of microcode, (Etessami, K.; Rajamani, S. K., CAV, Lecture Notes in Computer Science, vol. 3576, (2005), Springer), 185-198 · Zbl 1081.68602
[30] Craciunescu, S., Proving the equivalence of CLP programs, (Stuckey, P. J., ICLP, Lecture Notes in Computer Science, vol. 2401, (2002), Springer), 287-301 · Zbl 1045.68035
[31] Strichman, O., Regression verification: proving the equivalence of similar programs, (Bouajjani, A.; Maler, O., CAV, Lecture Notes in Computer Science, vol. 5643, (2009), Springer), 63
[32] Godlin, B.; Strichman, O., Inference rules for proving the equivalence of recursive procedures, (Manna, Z.; Peled, D., Essays in Memory of Amir Pnueli, Lecture Notes in Computer Science, vol. 6200, (2010), Springer), 167-184 · Zbl 1288.68042
[33] Bae, K.; Escobar, S.; Meseguer, J., Abstract logical model checking of infinite-state systems using narrowing, (van Raamsdonk, F., 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, The Netherlands, LIPIcs, vol. 21, (2013), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 81-96 · Zbl 1356.68140
[34] Rocha, C.; Meseguer, J.; Muñoz, C. A., Rewriting modulo SMT and open system analysis, (Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014, (2014)), Revised Selected Papers, 2014, pp. 247-262 · Zbl 1367.68151
[35] Rocha, C.; Meseguer, J.; Muñoz, C., Rewriting modulo SMT and open system analysis, J. Log. Algebraic Methods Program., 86, 269-297, (2017) · Zbl 1353.68156
[36] Arusoaie, A.; Lucanu, D.; Rusu, V., A generic framework for symbolic execution, (6th International Conference on Software Language Engineering, LNCS, vol. 8225, (2013), Springer Verlag), 281-301, also available as a technical report
[37] Rusu, V.; Arusoaie, A., Proving reachability-logic formulas incrementally, (Lucanu, D., Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016, Held as a Satellite Event of ETAPS, Eindhoven, The Netherlands, April 2-3, 2016, Revised Selected Papers, Lecture Notes in Computer Science, vol. 9942, (2016), Springer), 134-151 · Zbl 1367.68076
[38] Roşu, G.; Ellison, C.; Schulte, W., Matching logic: an alternative to Hoare/floyd logic, (Johnson, M.; Pavlovic, D., Proceedings of the 13th International Conference on Algebraic Methodology and Software Technology, AMAST ’10, Lecture Notes in Computer Science, vol. 6486, (2010)), 142-162 · Zbl 1308.68045
[39] Roşu, G.; Ştefănescu, A., Matching logic: a new program verification approach (NIER track), (ICSE’11: Proceedings of the 30th International Conference on Software Engineering, (2011), ACM), 868-871
[40] Roşu, G., Matching logic — extended abstract, (Proceedings of the 26th International Conference on Rewriting Techniques and Applications, RTA’15, LIPIcs. Leibniz Int. Proc. Inform., vol. 36, (2015), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik Dagstuhl, Germany), 5-21 · Zbl 1366.68027
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.