From rewriting logic, to programming language semantics, to program verification. (English) Zbl 1321.68337

Martí-Oliet, Narciso (ed.) et al., Logic, rewriting, and concurrency. Essays dedicated to José Meseguer on the occasion of his 65th birthday. Cham: Springer (ISBN 978-3-319-23164-8/pbk; 978-3-319-23165-5/ebook). Lecture Notes in Computer Science 9200, 598-616 (2015).
Summary: Rewriting logic has proven to be an excellent formalism to define executable semantics of programming languages, concurrent or not, and then to derive formal analysis tools for the defined languages with very little effort, such as model checkers. In this paper we give an overview of recent results obtained in the context of the rewriting logic semantics framework \(\mathbb {K}\), such as complete semantics of large programming languages like C, Java, JavaScript, Python, and deductive program verification techniques that allow us to verify programs in these languages using a common verification infrastructure.
For the entire collection see [Zbl 1319.68011].


68Q42 Grammars and rewriting systems
03B70 Logic in computer science
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI


[1] ISO/IEC: Programming languages–C, ISO/IEC WG14, ISO 9899:2011, December 2011. http://www.open-std.org/JTC1/SC22/WG14/www/standards
[2] Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009) · Zbl 05618496
[3] Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012) · Zbl 06123254
[4] Meseguer, J.: Conditioned rewriting logic as a united model of concurrency. Theoret. Comput. Sci. 96(1), 73–155 (1992) · Zbl 0758.68043
[5] Verdejo, A., Martí-Oliet, N.: Executable structural operational semantics in Maude. Departamento de Sistemas Informàticos y Programaciòn, Universidad Complutense de Madrid. Technical report 134-03 (2003)
[6] Verdejo, A., Martí-Oliet, N.: Executable structural operational semantics in Maude. J. Logic Algebraic Program. 67(1–2), 226–293 (2006) · Zbl 1088.68095
[7] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007) · Zbl 1115.68046
[8] Kahn, G.: Natural semantics. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol. 247, pp. 22–39. Springer, Heidelberg (1987) · Zbl 0635.68007
[9] Plotkin, G.D.: A structural approach to operational semantics. University of Aarhus, Technical report. DAIMI FN-19 (1981) republished in Journal of Logic and Algebraic Programming, 60–61 (2004)
[10] Plotkin, G.D.: A structural approach to operational semantics. J. Logic Algebraic Program. 60–61, 17–139 (2004)
[11] Şerbănuţă, T.-F., Roşu, G., Meseguer, J.: A rewriting logic approach to operational semantics. Inf. Comput. 207(2), 305–340 (2009) · Zbl 1165.68041
[12] Berry, G., Boudol, G.: The chemical abstract machine. In: POPL, pp. 81–94 (1990)
[13] Berry, G., Boudol, G.: The chemical abstract machine. Theoret. Comput. Sci. 96(1), 217–248 (1992) · Zbl 0747.68013
[14] Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theoret. Comput. Sci. 103(2), 235–271 (1992) · Zbl 0764.68094
[15] Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994) · Zbl 0938.68559
[16] Hennessy, M.: The Semantics of Programming Languages: An Elementary Introduction using Structural Operational Semantics. Wiley, New York (1990) · Zbl 0723.68067
[17] Mosses, P.D.: Foundations of modular SOS. In: Kutyłowski, M., Wierzbicki, T.M., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 70–80. Springer, Heidelberg (1999) · Zbl 0955.68075
[18] Mosses, P.D.: Pragmatics of modular SOS. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 21–40. Springer, Heidelberg (2002) · Zbl 1275.68086
[19] Mosses, P.D.: Modular structural operational semantics. J. Logic Algebraic Program. 60–61, 195–228 (2004) · Zbl 1072.68061
[20] Meseguer, J., Braga, C.O.: Modular rewriting semantics of programming languages. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 364–378. Springer, Heidelberg (2004) · Zbl 1108.68401
[21] Braga, C., Meseguer, J.: Modular rewriting semantics in practice. Electron. Notes Theor. Comput. Sci. 117, 393–416 (2005) · Zbl 1272.68168
[22] Chalub, F., Braga, C.: Maude MSOS tool. In: Denker, G., Talcott, C. (eds.) Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications (WRLA 2006). Electronic Notes in Theoretical Computer Science, vol. 176(4), pp. 133–146 (2007) · Zbl 06250532
[23] 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
[24] Ellison, C., Roşu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533–544 (2012) · Zbl 06481275
[25] Hathhorn, C., Ellison, C., Roşu, G.: Defining the undefinedness of C. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015). ACM (2015)
[26] 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 2015), pp. 445–456. ACM, January 2015 · Zbl 1346.68046
[27] Park, D., Ştefănescu, A., Roşu, G.: KJS: a complete formal semantics of JavaScript. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015). ACM (2015)
[28] Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011) · Zbl 1326.68047
[29] Ştefănescu, A., Ciobâcă, Ş., Mereuta, R., Moore, B.M., Şerbănută, T.F., Roşu, G.: All-path reachability logic. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 425–440. Springer, Heidelberg (2014) · Zbl 1416.68052
[30] Roşu, G., Ştefănescu, A., Ciobâcă, S., Moore, B.M.: One-path reachability logic. In: LICS 2013. IEEE (2013)
[31] 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 2012), pp. 555–574. ACM (2012)
[32] Roşu, G., Ştefănescu, A.: Towards a unified theory of operational and axiomatic semantics. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 351–363. Springer, Heidelberg (2012) · Zbl 1367.68075
[33] Roşu, G.: Matching logic – extended abstract. In: Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015). LNCS. Springer, Heidelberg (2015, to appear)
[34] Roşu, G., Ştefănescu, A.: From Hoare logic to matching logic reachability. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 387–402. Springer, Heidelberg (2012) · Zbl 1372.68066
[35] Roşu, G., Ştefănescu, A.: Matching logic: a new program verification approach. In: ICSE (NIER track), pp. 868–871 (2011)
[36] Roşu, G., Ellison, C., Schulte, W.: Matching logic: an alternative to Hoare/Floyd logic. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 142–162. Springer, Heidelberg (2011) · Zbl 1308.68045
[37] Roşu, G., Ştefănescu, A.: Matching logic rewriting: unifying operational and axiomatic semantics in a practical and generic framework. University of Illinois, Technical report, November 2011. http://hdl.handle.net/2142/28357
[38] de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) · Zbl 05262379
[39] Roşu, G.: CS322, Fall 2003 - Programming language design: Lecture notes. University of Illinois at Urbana-Champaign, Department of Computer Science, Technical report. UIUCDCS-R-2003-2897, December 2003, lecture notes of a course taught at UIUC
[40] Meseguer, J., Roşu, G.: Rewriting logic semantics: from language specifications to formal analysis tools. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 1–44. Springer, Heidelberg (2004) · Zbl 1126.68464
[41] Guth, D.: A formal semantics of Python 3.3. Master’s thesis, University of Illinois at Urbana-Champaign, July 2013. https://github.com/kframework/python-semantics
[42] Meredith, P., Hills, M., Roşu, G.: An executable rewriting logic semantics of K-scheme. In: Dube, D. (ed.) Proceedings of the 2007 Workshop on Scheme and Functional Programming (SCHEME 2007), Technical report DIUL-RT-0701. Laval University, pp. 91–103 (2007)
[43] Lazar, D.: K definition of Haskell’98 (2012). https://github.com/davidlazar/haskell-semantics
[44] Gligoric, M., Marinov, D., Kamin, S.: CoDeSe: fast deserialization via code generation. In: Dwyer, M.B., Tip, F. (eds.) ISSTA, pp. 298–308. ACM (2011)
[45] Asăvoae, M.: K semantics for assembly languages: a case study. In: Hills, M. (ed.) K’11. Electronic Notes in Theoretical Computer Science, vol. 304, pp. 111–125 (2014)
[46] Asăvoae, M.: A K-based methodology for modular design of embedded systems. In: WADT (preliminary proceedings). TR-08/12, Universidad Complutense de Madrid, p. 16 (2012). http://maude.sip.ucm.es/wadt2012/docs/WADT2012-preproceedings.pdf
[47] Ellison, C., Lazar, D.: K definition of the LLVM assembly language (2012). https://github.com/davidlazar/llvm-semantics
[48] Meredith, P.O., Katelman, M., Meseguer, J., Roşu, G.: A formal executable semantics of Verilog. In: Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), pp. 179–188. IEEE (2010)
[49] Hills, M., Chen, F., Roşu, G.: A rewriting logic approach to static checking of units of measurement in C. In: Kniesel, G., Pinto, J.S. (eds.) RULE 2008. Electronic Notes in Theoretical Computer Science, vol. 290, pp. 51–67. Elsevier (2012) · Zbl 06309653
[50] Rusu, V., Lucanu, D.: A \[ \mathbb{K} \] K -based formal framework for domain-specific modelling languages. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 214–231. Springer, Heidelberg (2012) · Zbl 06204968
[51] Arusoaie, A., Lucanu, D., Rusu, V.: Towards a K semantics for OCL. In: Hills, M. (ed.) K’11. Electronic Notes in Theoretical Computer Science, vol. 304, pp. 81–96 (2014)
[52] Heumann, S., Adve, V.S., Wang, S.: The tasks with effects model for safe concurrency. In: Nicolau, A., Shen, X., Amarasinghe, S.P., Vuduc, R. (eds.) PPOPP, pp. 239–250. ACM (2013)
[53] Dinges, P., Agha, G.: Scoped synchronization constraints for large scale actor systems. In: Sirjani, M. (ed.) COORDINATION 2012. LNCS, vol. 7274, pp. 89–103. Springer, Heidelberg (2012) · Zbl 06069578
[54] Şerbănuţă, T.-F., Ştefănescu, G., Roşu, G.: Defining and executing P systems with structured data in K. In: Corne, D.W., Frisco, P., Păun, G., Rozenberg, G., Salomaa, A. (eds.) WMC 2008. LNCS, vol. 5391, pp. 374–393. Springer, Heidelberg (2009) · Zbl 1196.68084
[55] Chira, C., Şerbănuţă, T.-F., Ştefănescu, G.: P systems with control nuclei: the concept. J. Logic Algebraic Program. 79(6), 326–333 (2010) · Zbl 1208.68125
[56] Şerbănuţă, T.-F.: A rewriting approach to concurrent programming language design and semantics. Ph.D. dissertation, University of Illinois at Urbana-Champaign, December 2010. https://www.ideals.illinois.edu/handle/2142/18252
[57] Ellison, C., Şerbănuţă, T.-F., Roşu, G.: A rewriting logic approach to type inference. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 135–151. Springer, Heidelberg (2009) · Zbl 1253.68211
[58] Asăvoae, I.M., Asăvoae, M.: Collecting semantics under predicate abstraction in the K framework. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 123–139. Springer, Heidelberg (2010) · Zbl 1306.68061
[59] Asăvoae, I.M.: Systematic design of abstractions in K. In: WADT (preliminary proceedings), TR-08/12, Universidad Complutense de Madrid, p. 9 (2012). http://maude.sip.ucm.es/wadt2012/docs/WADT2012-preproceedings.pdf
[60] Rot, J., Asăvoae, I.M., de Boer, F.S., Bonsangue, M.M., Lucanu, D.: Interacting via the heap in the presence of recursion. In: Carbone, M., Lanese, I., Silva, A., Sokolova, A. (eds.) ICE. Electronic Proceedings in Theoretical Computer Science, vol. 104, pp. 99–113 (2012)
[61] Asăvoae, I.M., Asăvoae, M., Lucanu, D.: Path directed symbolic execution in the K framework. In: Ida, T., Negru, V., Jebelean, T., Petcu, D., Watt, S.M., Zaharie, D. (eds.) SYNASC, pp. 133–141. IEEE Computer Society (2010)
[62] Asăvoae, I.M.: Abstract semantics for alias analysis in K. In: Hills, M. (ed.) K’11. Electronic Notes in Theoretical Computer Science, vol. 304, pp. 97–110 (2014)
[63] Arusoaie, A., Lucanu, D., Rusu, V.: A generic framework for symbolic execution. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 281–301. Springer, Heidelberg (2013) · Zbl 06360542
[64] Arusoaie, A.: A generic framework for symbolic execution: theory and applications. Ph.D. dissertation, Faculty of Computer Science, Alexandru I. Cuza, University of Iasi, September 2014. https://fmse.info.uaic.ro/publications/193/
[65] Asăvoae, M., Lucanu, D., Roşu, G.: Towards semantics-based WCET analysis. In: Healy, C. (ed.) WCET. Austian Computer Society (OCG) (2011)
[66] Asăvoae, M., Asăvoae, I.M., Lucanu, D.: On abstractions for timing analysis in the \[ \mathbb{K} \] K framework. In: Peña, R., van Eekelen, M., Shkaravska, O. (eds.) FOPARA 2011. LNCS, vol. 7177, pp. 90–107. Springer, Heidelberg (2012). http://dx.doi.org/10.1007/978-3-642-32495-6_6 · Zbl 1367.68058
[67] Asǎvoae, M., Asǎvoae, I.M.: On the modular integration of abstract semantics for WCET analysis. In: Lago, U.D., Peña, R. (eds.) FOPARA 2013. LNCS, vol. 8552, pp. 19–37. Springer, Heidelberg (2014). http://dx.doi.org/10.1007/978-3-319-12466-7_2 · Zbl 1445.68037
[68] Lucanu, D., Rusu, V.: Program equivalence by circular reasoning. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 362–377. Springer, Heidelberg (2013). https://hal.inria.fr/hal-01065830 · Zbl 06248478
[69] Ciobâcă, Ş., Lucanu, D., Rusu, V., Roşu, G.: A language-independent proof system for mutual program equivalence. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 75–90. Springer, Heidelberg (2014). https://hal.inria.fr/hal-01030754 · Zbl 06587176
[70] Ciobâcă, S., Lucanu, D., Rusu, V., Roşu, G.: A theoretical foundation for programming languages aggregation. In: 22nd International Workshop on Algebraic Development Techniques. LNCS, Sinaia, Romania. Spriger, Heidelberg, September 2014 (to appear). https://hal.inria.fr/hal-01076641 · Zbl 1472.68019
[71] Roşu, G., Schulte, W., Şerbănuţă, T.F.: Runtime verification of C memory safety. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 132–151. Springer, Heidelberg (2009) · Zbl 05615966
[72] Regehr, J., Chen, Y., Cuoq, P., Eide, E., Ellison, C., Yang, X.: Test-case reduction for C compiler bugs. In: Vitek, J., Lin, H., Tip, F. (eds.) PLDI, pp. 335–346. ACM (2012)
[73] Arusoaie, A., Lucanu, D., Rusu, V., Şerbănuţă, T.-F., Ştefănescu, A., Roşu, G.: Language definitions as rewrite theories. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 97–112. Springer, Heidelberg (2014). https://hal.inria.fr/hal-00950775 · Zbl 1356.68115
[74] Chiriţă, C.E., Şerbănuţă, T.-F.: An institutional foundation for the K semantic framework. In: 22nd International Workshop on Algebraic Development Techniques (WADT 2014). LNCS (2014, to appear)
[75] Feliú, M.A.: Logic-based techniques for program analysis and specification synthesis. Ph.D. dissertation, Universitat Politècnica de València, Departamento de Sistemas Informáticos y Computación, September 2013
[76] Alpuente, M., Feliú, M.A., Villanueva, A.: Automatic inference of specifications using matching logic. In: Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013, Rome, Italy, 21–22 January 2013, pp. 127–136. ACM (2013)
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.