×

(Co)inductive proof systems for compositional proofs in reachability logic. (English) Zbl 1455.03040

Summary: Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems for this formalism, all of which are sound and complete and inherit the coinductive nature of the logic. The proof systems differ, however, in several aspects. First, they use induction and coinduction in different proportions. The second aspect regards compositionality, broadly meaning their ability to prove simpler formulas on smaller systems and to reuse those formulas as lemmas for proving more complex formulas on larger systems. The third aspect is the difficulty of their soundness proofs.
We show that the more induction a proof system uses, and the more specialised is its use of coinduction (with respect to our problem domain), the more compositional the proof system is, but the more difficult is its soundness proof.
We present formalisations of these results in the Coq proof assistant. In particular we have developed support for coinductive proofs that is comparable to that provided by Coq for inductive proofs. This may be of interest to a broader class of Coq users.

MSC:

03B70 Logic in computer science
68V20 Formalization of mathematics in connection with theorem provers
PDF BibTeX XML Cite
Full Text: DOI arXiv

References:

[1] Stefanescu, A.; Ciobâcă, Ş.; Mereuta, R.; Moore, B. M.; Serbanuta, T.; Rosu, G., All-path reachability logic, Log. Methods Comput. Sci., 15, 2 (2019) · Zbl 1421.68015
[2] Hoare, C. A.R., An axiomatic basis for computer programming, Commun. ACM, 12, 10, 576-580 (1969) · Zbl 0179.23105
[3] O’Hearn, P. W., Separation logic, Commun. ACM, 62, 2, 86-95 (2019)
[4] Rosu, G.; Stefanescu, A.; Ciobâcă, Ş.; Moore, B. M., One-path reachability logic, (28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013. 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013 (2013), IEEE Computer Society), 358-367 · Zbl 1366.68182
[5] Stefanescu, A.; Park, D.; Yuwen, S.; Li, Y.; Rosu, G., Semantics-based program verifiers for all languages, (Visser, E.; Smaragdakis, Y., Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, Part of SPLASH 2016. Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, Part of SPLASH 2016, Amsterdam, the Netherlands, October 30 - November 4, 2016 (2016), AMC), 74-91
[6] Lucanu, D.; Rusu, V.; Arusoaie, A.; Nowak, D., Verifying reachability-logic properties on rewriting-logic specifications, (Martí-Oliet, N.; Ölveczky, P. C.; Talcott, C. L., Logic, Rewriting, and Concurrency - Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday. Logic, Rewriting, and Concurrency - Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday, Lecture Notes in Computer Science, vol. 9200 (2015), Springer), 451-474 · Zbl 1321.68359
[7] Skeirik, S.; Stefanescu, A.; Meseguer, J., A constructor-based reachability logic for rewrite theories, (Fioravanti, F.; Gallagher, J. P., Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers. Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers, Namur, Belgium, October 10-12, 2017. Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers. Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers, Namur, Belgium, October 10-12, 2017, Lecture Notes in Computer Science, vol. 10855 (2017), Springer), 201-217 · Zbl 1471.68075
[8] Rusu, V.; Grimaud, G.; Hauspie, M., Proving partial-correctness and invariance properties of transition-system models, (Pang, J.; Zhang, C.; He, J.; Weng, J., 2018 International Symposium on Theoretical Aspects of Software Engineering, TASE 2018. 2018 International Symposium on Theoretical Aspects of Software Engineering, TASE 2018, Guangzhou, China, August 29-31, 2018 (2018), IEEE Computer Society), 60-67
[9] Bertot, Y.; Castéran, P., Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science. an EATCS Series (2004), Springer · Zbl 1069.68095
[10] Rusu, V.; Nowak, D., (Co)inductive proof systems for compositional proofs in reachability logic, (Marin, M.; Craciun, A., Proceedings Third Symposium on Working Formal Methods, FROM 2019. Proceedings Third Symposium on Working Formal Methods, FROM 2019, Timişoara, Romania, 3-5 September 2019. Proceedings Third Symposium on Working Formal Methods, FROM 2019. Proceedings Third Symposium on Working Formal Methods, FROM 2019, Timişoara, Romania, 3-5 September 2019, EPTCS, vol. 303 (2019)), 32-47
[11] Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL - a Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283 (2002), Springer · Zbl 0994.68131
[12] Ciobâcă, Ş.; Lucanu, D., A coinductive approach to proving reachability properties in logically constrained term rewriting systems, (Galmiche, D.; Schulz, S.; Sebastiani, R., Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings, Oxford, UK, July 14-17, 2018. Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings, Oxford, UK, July 14-17, 2018, Lecture Notes in Computer Science, vol. 10900 (2018), Springer), 295-311 · Zbl 06958106
[13] Lucanu, D.; Rusu, V.; Arusoaie, A., A generic framework for symbolic execution: a coinductive approach, J. Symb. Comput., 80, 125-163 (2017) · Zbl 1356.68044
[14] Moore, B. M.; Peña, L.; Rosu, G., Program verification by coinduction, (Ahmed, A., Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings, Thessaloniki, Greece, April 14-20, 2018. Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings, Thessaloniki, Greece, April 14-20, 2018, Lecture Notes in Computer Science, vol. 10801 (2018), Springer), 589-618 · Zbl 1418.68060
[15] Giménez, E., Codifying guarded definitions with recursive schemes, (Dybjer, P.; Nordström, B.; Smith, J. M., Types for Proofs and Programs, International Workshop TYPES’94, Selected Papers. Types for Proofs and Programs, International Workshop TYPES’94, Selected Papers, Båstad, Sweden, June 6-10, 1994. Types for Proofs and Programs, International Workshop TYPES’94, Selected Papers. Types for Proofs and Programs, International Workshop TYPES’94, Selected Papers, Båstad, Sweden, June 6-10, 1994, Lecture Notes in Computer Science, vol. 996 (1994), Springer), 39-59
[16] Rusu, V.; Grimaud, G.; Hauspie, M., Proving partial-correctness and invariance properties of transition-system models, Sci. Comput. Program., 186 (2020)
[17] Bertot, Y.; Komendantskaya, E., Inductive and coinductive components of corecursive functions in Coq, (Adámek, J.; Kupke, C., Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, CMCS 2008. Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, CMCS 2008, Budapest, Hungary, April 4-6, 2008. Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, CMCS 2008. Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, CMCS 2008, Budapest, Hungary, April 4-6, 2008, Electronic Notes in Theoretical Computer Science, vol. 203 (2008), Elsevier), 25-47 · Zbl 1279.68285
[18] Bertot, Y.; Komendantskaya, E., Using structural recursion for corecursion, (Berardi, S.; Damiani, F.; de’Liguoro, U., Types for Proofs and Programs, International Conference, TYPES 2008, Revised Selected Paper. Types for Proofs and Programs, International Conference, TYPES 2008, Revised Selected Paper, Torino, Italy, March 26-29, 2008s. Types for Proofs and Programs, International Conference, TYPES 2008, Revised Selected Paper. Types for Proofs and Programs, International Conference, TYPES 2008, Revised Selected Paper, Torino, Italy, March 26-29, 2008s, Lecture Notes in Computer Science, vol. 5497 (2008), Springer), 220-236 · Zbl 1246.68196
[19] Hur, C.; Neis, G.; Dreyer, D.; Vafeiadis, V., The power of parameterization in coinductive proof, (Giacobazzi, R.; Cousot, R., The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’13. The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’13, Rome, Italy - January 23-25, 2013 (2013), ACM), 193-206 · Zbl 1301.68220
[20] Pous, D., Coinduction all the way up, (Grohe, M.; Koskinen, E.; Shankar, N., Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’16. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’16, New York, NY, USA, July 5-8, 2016 (2016), ACM), 307-316 · Zbl 1394.68352
[21] Danielsson, N. A., Beating the productivity checker using embedded languages, (Komendantskaya, E.; Bove, A.; Niqui, M., Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010. Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010. Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010. Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010, EPiC Series, vol. 5 (2010), EasyChair), 34-54
[22] Abel, A.; Pientka, B., Well-founded recursion with copatterns and sized types, J. Funct. Program., 26, e2 (2016) · Zbl 1420.68031
[23] Lochbihler, A., Coinductive, archive of formal proofs (Feb. 2010), Formal proof development
[24] Sangiorgi, D., Introduction to Bisimulation and Coinduction (2011), Cambridge University Press: Cambridge University Press New York, NY, USA · Zbl 1252.68008
[25] de Roever, W. P.; de Boer, F. S.; Hannemann, U.; Hooman, J.; Lakhnech, Y.; Poel, M.; Zwiers, J., Concurrency Verification: Introduction to Compositional and Noncompositional Methods, Cambridge Tracts in Theoretical Computer Science, vol. 54 (2001), Cambridge University Press · Zbl 1009.68020
[26] Giacomo, G. D.; Vardi, M. Y., Linear temporal logic and linear dynamic logic on finite traces, (Rossi, F., IJCAI 2013. IJCAI 2013, Beijing, China, August 3-9, 2013. IJCAI 2013. IJCAI 2013, Beijing, China, August 3-9, 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence (2013), IJCAI/AAAI), 854-860
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.