Skip to main content
SpringerLink
Log in

Towards a Unified Theory of Operational and Axiomatic Semantics

  • Conference paper
Automata, Languages, and Programming (ICALP 2012)

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

Included in the following conference series:

Abstract

This paper presents a nine-rule language-independent proof system that takes an operational semantics as axioms and derives program reachability properties, including ones corresponding to Hoare triples. This eliminates the need for language-specific Hoare-style proof rules to verify programs, and, implicitly, the tedious step of proving such proof rules sound for each language separately. The key proof rule is Circularity, which is coinductive in nature and allows for reasoning about constructs with repetitive behaviors (e.g., loops). The generic proof system is shown sound and has been implemented in the MatchC verifier.

Full version of this paper, with proofs, available at http://hdl.handle.net/2142/30827 .

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

    Chapter  Google Scholar 

  2. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  3. Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic Execution with Separation Logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Berry, G., Boudol, G.: The chemical abstract machine. Th. Comp. Sci. 96(1), 217–248 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  5. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  6. Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533–544. ACM (2012)

    Google Scholar 

  7. Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex. MIT (2009)

    Google Scholar 

  8. Floyd, R.W.: Assigning meaning to programs. In: Symposia in Applied Mathematics, vol. 19, pp. 19–32. AMS (1967)

    Google Scholar 

  9. George, C., Haxthausen, A.E., Hughes, S., Milne, R., Prehn, S., Pedersen, J.S.: The RAISE Development Method. BCS Practitioner Series. Prentice Hall (1995)

    Google Scholar 

  10. Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. In: Handbook of Philosophical Logic, pp. 497–604 (1984)

    Google Scholar 

  11. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  12. Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice Hall (1998)

    Google Scholar 

  13. Jacobs, B.: Weakest pre-condition reasoning for java programs with JML annotations. J. Log. Algebr. Program. 58(1-2), 61–88 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  14. Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284–304 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  15. Liu, H., Moore, J.S.: Java Program Verification via a JVM Deep Embedding in ACL2. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 184–200. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  17. Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  18. 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 

  19. Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing 10, 171–186 (1998)

    Article  MATH  Google Scholar 

  20. Pasareanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M.R., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: ISSTA, pp. 15–26. ACM (2008)

    Google Scholar 

  21. 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 

  22. Roşu, G., Lucanu, D.: Circular Coinduction: A Proof Theoretical Foundation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 127–144. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  23. Rosu, G., Serbanuta, T.F.: An overview of the K semantic framework. J. Log. Algebr. Program. 79(6), 397–434 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  24. Rosu, G., Stefanescu, A.: Matching logic: A new program verification approach (NIER track). In: ICSE, pp. 868–871. ACM (2011)

    Google Scholar 

  25. Rosu, G., Stefanescu, A.: From Hoare logic to matching logic reachability. In: FM (to appear, 2012)

    Google Scholar 

  26. Rosu, G., Stefanescu, A.: Towards a unified theory of operational and axiomatic semantics. Tech. Rep., Univ. of Illinois (May 2012), http://hdl.handle.net/2142/30827

  27. Sasse, R., Meseguer, J.: Java+ITP: A verification tool based on Hoare logic and algebraic semantics. Electr. Notes Theor. Comput. Sci. 176(4), 29–46 (2007)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Illinois at Urbana-Champaign, USA

    Grigore Roşu & Andrei Ştefănescu

  2. Alexandru Ioan Cuza University, Iaşi, Romania

    Grigore Roşu

Authors
  1. Grigore Roşu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrei Ştefănescu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Centre for Discrete Mathematics and its Applications, University of Warwick, Warwick, UK

    Artur Czumaj

  2. Max-Planck-Institut für Informatik, Saarbrücken, Germany

    Kurt Mehlhorn

  3. Computer Laboratory,, University of Cambridge, UK

    Andrew Pitts

  4. ETH Zurich, Switzerland

    Roger Wattenhofer

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Roşu, G., Ştefănescu, A. (2012). Towards a Unified Theory of Operational and Axiomatic Semantics. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds) Automata, Languages, and Programming. ICALP 2012. Lecture Notes in Computer Science, vol 7392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31585-5_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31585-5_33

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31584-8

  • Online ISBN: 978-3-642-31585-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation