Skip to main content
SpringerLink
Log in
SpringerLink
Log in

From Rewriting Logic, to Programming Language Semantics, to Program Verification

  • Chapter
  • First Online:
Logic, Rewriting, and Concurrency

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9200))

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The official test suite for Java implementations is the Java Compatibility Kit (JCK) from Oracle, which is not publicly available. Oracle offers free access for non-profit organizations willing to implement the whole JDK (http://openjdk.java.net/groups/conformance/JckAccess/), i.e., both the language and the class library. We applied and Oracle rejected our request, because we did not “implement” the complete Java library. Also, note that the NIST Juliet testsuite (http://samate.nist.gov/SARD/testsuite.php) is meant to asses the capability of Java static analysis tools, and not the completeness of Java implementations.

  2. 2.

    In mathematical mode, we prefer the notation \(\langle {...}\rangle _\mathsf{{k}}\) for cells instead of the XML-like notation \(\mathtt{<k>...</k> }\) preferred in ASCII.

References

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  4. Meseguer, J.: Conditioned rewriting logic as a united model of concurrency. Theoret. Comput. Sci. 96(1), 73–155 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  6. Verdejo, A., Martí-Oliet, N.: Executable structural operational semantics in Maude. J. Logic Algebraic Program. 67(1–2), 226–293 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  10. Plotkin, G.D.: A structural approach to operational semantics. J. Logic Algebraic Program. 60–61, 17–139 (2004)

    MathSciNet  MATH  Google Scholar 

  11. Şerbănuţă, T.-F., Roşu, G., Meseguer, J.: A rewriting logic approach to operational semantics. Inf. Comput. 207(2), 305–340 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  12. Berry, G., Boudol, G.: The chemical abstract machine. In: POPL, pp. 81–94 (1990)

    Google Scholar 

  13. Berry, G., Boudol, G.: The chemical abstract machine. Theoret. Comput. Sci. 96(1), 217–248 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  15. Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  16. Hennessy, M.: The Semantics of Programming Languages: An Elementary Introduction using Structural Operational Semantics. Wiley, New York (1990)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  19. Mosses, P.D.: Modular structural operational semantics. J. Logic Algebraic Program. 60–61, 195–228 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  21. Braga, C., Meseguer, J.: Modular rewriting semantics in practice. Electron. Notes Theor. Comput. Sci. 117, 393–416 (2005)

    Article  MATH  Google Scholar 

  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)

    Google Scholar 

  23. Roşu, G., Şerbănuţă, T.-F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397–434 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  24. Ellison, C., Roşu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533–544 (2012)

    Google Scholar 

  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)

    Google Scholar 

  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

    Google Scholar 

  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)

    Google Scholar 

  28. Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  30. Roşu, G., Ştefănescu, A., Ciobâcă, S., Moore, B.M.: One-path reachability logic. In: LICS 2013. IEEE (2013)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  35. Roşu, G., Ştefănescu, A.: Matching logic: a new program verification approach. In: ICSE (NIER track), pp. 868–871 (2011)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  50. Rusu, V., Lucanu, D.: A \(\mathbb{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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  66. Asăvoae, M., Asăvoae, I.M., Lucanu, D.: On abstractions for timing analysis in the \(\mathbb{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

    Chapter  Google Scholar 

  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

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Google Scholar 

  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

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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

    Google Scholar 

  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)

    Google Scholar 

  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

    Google Scholar 

  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)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Illinois at Urbana-Champaign, Champaign, USA

    Grigore Roșu

Authors
  1. Grigore Roșu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Grigore Roșu .

Editor information

Editors and Affiliations

  1. Universidad Complutense de Madrid, Madrid, Spain

    Narciso Martí-Oliet

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

  3. SRI International, Menlo Park, California, USA

    Carolyn Talcott

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Roșu, G. (2015). From Rewriting Logic, to Programming Language Semantics, to Program Verification. In: Martí-Oliet, N., Ölveczky, P., Talcott, C. (eds) Logic, Rewriting, and Concurrency. Lecture Notes in Computer Science(), vol 9200. Springer, Cham. https://doi.org/10.1007/978-3-319-23165-5_28

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23165-5_28

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23164-8

  • Online ISBN: 978-3-319-23165-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation