Skip to main content
SpringerLink
Log in

A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2018)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10900))

Included in the following conference series:

Abstract

We introduce a sound and complete coinductive proof system for reachability properties in transition systems generated by logically constrained term rewriting rules over an order-sorted signature modulo builtins. A key feature of the calculus is a circularity proof rule, which allows to obtain finite representations of the infinite coinductive proofs.

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

References

  1. Aguirre, L., Martí-Oliet, N., Palomino, M., Pita, I.: Conditional narrowing modulo SMT and Axioms. In: PPDP 2017, pp. 17–28 (2017)

    Google Scholar 

  2. Bae, K., Rocha, C.: Guarded terms for rewriting modulo SMT. In: Proença, J., Lumpe, M. (eds.) FACS 2017. LNCS, vol. 10487, pp. 78–97. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68034-7_5

    Chapter  Google Scholar 

  3. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV 2011, pp. 171–177 (2011)

    Chapter  Google Scholar 

  4. Bogdănaş, D., Roşu, G.: K-Java: a complete semantics of Java. In: POPL 2015, pp. 445–456 (2015)

    Article  Google Scholar 

  5. Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 350–367. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35182-2_25

    Chapter  Google Scholar 

  6. Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Log. Comput. 21(6), 1177–1216 (2011)

    Article  MathSciNet  Google Scholar 

  7. Ciobâcă, Ş., Arusoaie, A., Lucanu, D.: Unification modulo builtins. In: WoLLIC 2018 (2018, to appear)

    Google Scholar 

  8. Ciobâcă, Ş., Lucanu, D.: A coinductive approach to proving reachability properties in logically constrained term rewriting systems (2018). arXiv:1804.08308

  9. Ciobâcă, Ş., Lucanu, D., Rusu, V., Roşu, G.: A language-independent proof system for full program equivalence. Formal Asp. Comput. 28(3), 469–497 (2016)

    Article  MathSciNet  Google Scholar 

  10. Ş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 2014. LNCS, vol. 8560, pp. 425–440. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08918-8_29

    Chapter  Google Scholar 

  11. Ştefănescu, A., Park, D., Yuwen, S., Li, Y., Roşu, G.: Semantics-based program verifiers for all languages. In: OOPSLA 2016, pp. 74–91 (2016)

    Google Scholar 

  12. Durán, F., Eker, S., Escobar, S., Martí-Oliet, N., Meseguer, J., Talcott, C.: Built-in variant generation and unification, and their applications in Maude 2.7. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 183–192. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_13

    Chapter  Google Scholar 

  13. Escobar, S., Meseguer, J., Thati, P.: Narrowing and rewriting logic: from foundations to applications. ENTCS 177, 5–33 (2007)

    MATH  Google Scholar 

  14. Fuhs, C., Kop, C., Nishida, N.: Verifying procedural programs via constrained rewriting induction. ACM TOCL 18(2), 14:1–14:50 (2017)

    Article  MathSciNet  Google Scholar 

  15. Hathhorn, C., Ellison, C., Roşu, G.: Defining the undefinedness of C. In: PLDI 2015, pp. 336–345 (2015)

    Article  Google Scholar 

  16. Hur, C.-K., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: POPL 2013, pp. 193–206 (2013)

    Article  Google Scholar 

  17. Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Technical report RR-1358, INRIA (1990)

    Google Scholar 

  18. Kop, C.: Termination of LCTRSs. CoRR abs/1601.03206 (2016)

    Google Scholar 

  19. Kop, C., Nishida, N.: Constrained term rewriting tool. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 549–557. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48899-7_38

    Chapter  Google Scholar 

  20. Kop, C., Nishida, N.: Term rewriting with logical constraints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 343–358. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40885-4_24

    Chapter  Google Scholar 

  21. Lucanu, D., Rusu, V., Arusoaie, A.: A generic framework for symbolic execution: a coinductive approach. J. Symb. Comput. 80, 125–163 (2017)

    Article  MathSciNet  Google Scholar 

  22. Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. High.-Order Symb. Comput. 20(1–2), 123–160 (2007)

    Article  Google Scholar 

  23. Park, D., Ştefănescu, A., Roşu, G.: KJS: a complete formal semantics of JavaScript. PLDI 2015, 346–356 (2015)

    Google Scholar 

  24. Popescu, A., Gunter, E.L.: Incremental pattern-based coinduction for process algebra and its isabelle formalization. In: Ong, L. (ed.) FoSSaCS 2010. LNCS, vol. 6014, pp. 109–127. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12032-9_9

    Chapter  Google Scholar 

  25. Rocha, C., Meseguer, J., Muñoz, C.A.: Rewriting modulo SMT and open system analysis. J. Log. Algebr. Meth. Program. 86(1), 269–297 (2017)

    Article  MathSciNet  Google Scholar 

  26. Roşu, G.: Matching logic. Log. Methods Comp. Sci. 13(4), 1–61 (2017)

    MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  29. Skeirik, S., Ştefănescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. TR. http://hdl.handle.net/2142/95770

Download references

Acknowledgements

We thank the anonymous reviewers for their valuable suggestions. This work was supported by a grant of the Romanian National Authority for Scientific Research and Innovation, CNCS/CCCDI - UEFISICDI, project number PN-III-P2-2.1-BG-2016-0394, within PNCDI III.

Author information

Authors and Affiliations

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

    Ştefan Ciobâcă & Dorel Lucanu

Authors
  1. Ştefan Ciobâcă
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dorel Lucanu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ştefan Ciobâcă .

Editor information

Editors and Affiliations

  1. Université de Lorraine, Vandoeuvre-lès-Nancy, France

    Didier Galmiche

  2. Baden-Wuerttemberg Cooperative State University, Stuttgart, Germany

    Stephan Schulz

  3. University of Trento, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ciobâcă, Ş., Lucanu, D. (2018). A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94205-6_20

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94204-9

  • Online ISBN: 978-3-319-94205-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation