Advertisement

Unification in Matching Logic

  • Andrei ArusoaieEmail author
  • Dorel Lucanu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)

Abstract

Matching Logic is a framework for specifying programming language semantics and reasoning about programs. Its formulas are called patterns and are built with variables, symbols, connectives and quantifiers. A pattern is a combination of structural components (term patterns), which must be matched, and constraints (predicate patterns), which must be satisfied. Dealing with more than one structural component in a pattern could be cumbersome because it involves multiple matching operations. A source for getting patterns with many structural components is the conjunction of patterns. Here, we propose a method that uses a syntactic unification algorithm to transform conjunctions of structural patterns into equivalent patterns having only one structural component and some additional constraints. We prove the soundness and the completeness of our approach, and we provide sound strategies to generate certificates for the equivalences.

Keywords

Matching Logic Syntactic term unification Semantic unification Certification 

Notes

Acknowledgements

We thank the anonymous reviewers for their insightful comments. We would like to especially thank the Kore developers and researchers: Phillip Harris, Traian Şerbănuţă and Virgil Şerbănuţă for their valuable assistance and feedback. They helped us with our proof generation strategy and they suggested improvements for our current work. We also want to specially thank Grigore Roşu for the fruitful discussions that we had about this topic at FROM 2018. This work was supported by a grant of the “Alexandru Ioan Cuza” University of Iaşi, within the Research Grants program, Grant UAIC, ctr. no. 6/01-01-2017.

References

  1. 1.
    The Kore language (GitHub repository). https://github.com/kframework/kore. Accessed 07 Nov 2018
  2. 2.
    The semantics of K (online document). https://github.com/kframework/kore/blob/master/docs/semantics-of-k.pdf. Accessed 07 Nov 2018
  3. 3.
    Chapter 23 axiomatizable classes of locally free algebras of various types. In: Mal’cev, A.I. (ed.) The Metamathematics Algebraic Systems, Studies in Logic and the Foundations of Mathematics, vol. 66, pp. 262–281. Elsevier (1971).  https://doi.org/10.1016/S0049-237X(08)70560-3
  4. 4.
    Arusoaie, A., Lucanu, D., Rusu, V.: Symbolic execution based on language transformation. Comput. Lang. Syst. Struct. 44, 48–71 (2015)zbMATHGoogle Scholar
  5. 5.
    Arusoaie, A., Nowak, D., Rusu, V., Lucanu, D.: A certified procedure for RL verification. In: SYNASC 2017, pp. 129–136. IEEE CPS, Timişoara, Romania, September 2017. https://hal.inria.fr/hal-01627517
  6. 6.
    Baader, F.: Unification theory. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol. 572, pp. 151–170. Springer, Heidelberg (1992).  https://doi.org/10.1007/3-540-55124-7_5CrossRefGoogle Scholar
  7. 7.
    Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_14CrossRefGoogle Scholar
  8. 8.
    Bogdanas, D., Roşu, G.: K-Java: a complete semantics of Java. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, pp. 445–456. ACM, New York (2015).  https://doi.org/10.1145/2676726.2676982
  9. 9.
    Chen, X., Roşu, G.: Matching mu-logic. In: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019) (2019, to appear)Google Scholar
  10. 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_29CrossRefGoogle Scholar
  11. 11.
    Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pp. 533–544. ACM, New York (2012).  https://doi.org/10.1145/2103656.2103719
  12. 12.
    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, pp. 336–345. ACM, New York (2015).  https://doi.org/10.1145/2737924.2737979
  13. 13.
    Kovács, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 260–270. ACM, New York (2017).  https://doi.org/10.1145/3009837.3009887
  14. 14.
    Lucanu, D., Rusu, V., Arusoaie, A., Nowak, D.: Verifying reachability-logic properties on rewriting-logic specifications. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 451–474. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-23165-5_21CrossRefzbMATHGoogle Scholar
  15. 15.
    Łukasiewicz, J.: The shortest axiom of the implicational calculus of propositions. Proc. R. Irish Acad. Sect. Math. Phys. Sci. 52, 25–33 (1948). http://www.jstor.org/stable/20488489MathSciNetGoogle Scholar
  16. 16.
    Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. Program. Lang. Syst. 4(2), 258–282 (1982).  https://doi.org/10.1145/357162.357169CrossRefzbMATHGoogle Scholar
  17. 17.
    Moore, B., Peña, L., Rosu, G.: Program verification by coinduction. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 589–618. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89884-1_21CrossRefGoogle Scholar
  18. 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).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  19. 19.
    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, pp. 346–356. ACM, New York (2015).  https://doi.org/10.1145/2737924.2737991
  20. 20.
    Park, D., Zhang, Y., Saxena, M., Daian, P., Roşu, G.: A formal verification tool for ethereum VM bytecode. In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018, pp. 912–915. ACM, New York (2018).  https://doi.org/10.1145/3236024.3264591
  21. 21.
    Roşu, G.: Matching logic. Log. Methods Comput. Sci. 13(4), 1–61 (2017). http://arxiv.org/abs/1705.06312MathSciNetzbMATHGoogle Scholar
  22. 22.
    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).  https://doi.org/10.1007/978-3-642-32759-9_32CrossRefGoogle Scholar
  23. 23.
    Roşu, G., Ştefănescu, A.: Matching logic: a new program verification approach. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu, HI, USA, 21–28 May 2011, pp. 868–871 (2011).  https://doi.org/10.1145/1985793.1985928
  24. 24.
    Roşu, G., Ştefănescu, A., Ştefan Ciobâcă, Moore, B.M.: One-path reachability logic. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, 25–28 June 2013, pp. 358–367 (2013).  https://doi.org/10.1109/LICS.2013.42
  25. 25.
    Rusu, V., Arusoaie, A.: Proving reachability-logic formulas incrementally. In: Lucanu, D. (ed.) WRLA 2016. LNCS, vol. 9942, pp. 134–151. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-44802-2_8CrossRefzbMATHGoogle Scholar
  26. 26.
    Ştefănescu, A., Park, D., Yuwen, S., Li, Y., Roşu, G.: Semantics-based program verifiers for all languages. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, pp. 74–91. ACM, New York (2016).  https://doi.org/10.1145/2983990.2984027

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Alexandru Ioan Cuza UniversityIaşiRomania

Personalised recommendations