A Constructor-Based Reachability Logic for Rewrite Theories

• Autorzy: Skeirik Stephen , Stefanescu Andrei , Meseguer José

Identyfikatory

DOI

10.3233/FI-2020-1926

• Języki publikacji: EN

Abstrakty

EN

Reachability logic has been applied to K rewrite-rule-based language definitions as a language-generic logic of programs to verify a wide range of sophisticated programs in conventional languages. Here we study how reachability logic can be made not just language-generic, but also rewrite-theory-generic, so that we can verify both conventional programs based on their rewriting logic operational semantics and distributed system designs specified as rewrite theories. A theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. Particular attention is given to increasing the logic's automation by means of constructor-based semantic unification, matching, narrowing, and satisfiability procedures. The relationships to Hoare logic and LTL are discussed, new methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new methods are presented.

Słowa kluczowe

EN

deductive verification; reachability logics; rewriting logics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 173, nr 4
• Strony: 315--382
• Opis fizyczny: Bibliogr. 69 poz., tab.

Twórcy

autor

Skeirik Stephen

• Department of Computer Science, University of Illinois at Urbana-Champaign, Illinois, USA

autor

Stefanescu Andrei

• Department of Computer Science, University of Illinois at Urbana-Champaign, Illinois, USA

autor

Meseguer José

• Department of Computer Science, University of Illinois at Urbana-Champaign, Illinois, USA

Bibliografia

• [1] Rosu G, Serbanuta T. An overview of the K semantic framework. J. Log. Algebr. Program., 2010. 79(6):397-434. URL https://doi.org/10.1016/j.jlap.2010.03.012.
• [2] Stefanescu A, Ştefan Ciobâcă, Mereuta R, Moore BM, Serbanuta T, Rosu G. All-Path Reachability Logic. In: Proc. RTA-TLCA 2014, volume 8560. Springer LNCS, 2014 pp. 425-440. doi:10.1007/978-3-319-08918-8_29.
• [3] Stefanescu A, Park D, Yuwen S, Li Y, Rosu G. Semantics-based program verifiers for all languages. In: Proc. OOPSLA 2016. ACM, 2016 pp. 74-91. URL https://doi.org/10.1145/2983990.2984027.
• [4] Meseguer J. Conditional Rewriting Logic as a Unified Model of Concurrency. Theoretical Computer Science, 1992. 96(1):73-155. URL https://doi.org/10.1016/0304-3975(92)90182-F.
• [5] Meseguer J. Twenty years of rewriting logic. J. Algebraic and Logic Programming, 2012. 81:721-781. URL https://doi.org/10.1016/j.jlap.2012.06.003.
• [6] Meseguer J, Rosu G. The rewriting logic semantics project: A progress report. Inf. Comput., 2013. 231:38-69. URL https://doi.org/10.1016/j.ic.2013.08.004.
• [7] Lucanu D, Rusu V, Arusoaie A, Nowak D. Verifying Reachability-Logic Properties on Rewriting-Logic Specifications. In: Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, volume 9200. Springer LNCS, 2015 pp. 451-474. doi:10.1007/978-3-319-23165-5_21.
• [8] Siekmann JH. Unification Theory. J. Symb. Comput., 1989. 7(3/4):207-274.
• [9] Jouannaud JP, Kirchner C. Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification. In: Computational Logic - Essays in Honor of Alan Robinson. MIT Press, 1991 pp. 257-321.
• [10] Baader F, Siekmann JH. Unification theory. In: Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 2, pp. 41-126. Oxford University Press, 1994.
• [11] Baader F, Snyder W. Unification Theory. In: Handbook of Automated Reasoning (in 2 volumes), pp. 445-532. Elsevier and MIT Press, 2001.
• [12] Hullot JM. Canonical Forms and Unification. In: Proc. Fifth Conference on Automated Deduction, volume 87 of LNCS, pp. 318-334. Springer, 1980. doi:10.1007/3-540-10009-1_25.
• [13] Jouannaud JP, Kirchner C, Kirchner H. Incremental construction of unification algorithms in equational theories. In: Proc. ICALP’83. Springer LNCS 154, 1983 pp. 361-373. doi:10.1007/BFb0036921.
• [14] Escobar S, Sasse R, Meseguer J. Folding variant narrowing and optimal variant termination. J. Algebraic and Logic Programming, 2012. 81:898-928. URL https://doi.org/10.1016/j.jlap.2012.01.002.
• [15] Meseguer J, Thati P. Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols. J. Higher-Order and Symbolic Computation, 2007. 20(1-2):123-160. URL https://doi.org/10.1007/s10990-007-9000-6.
• [16] Maher MJ. Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees. In: Proc. LICS ’88. IEEE Computer Society, 1988 pp. 348-357. doi:10.1109/LICS.1988.5132.
• [17] Comon H, Lescanne P. Equational Problems and Disunification. Journal of Symbolic Computation, 1989. 7:371-425. URL https://doi.org/10.1016/S0747-7171(89)80017-3.
• [18] Comon H. Complete Axiomatizations of Some Quotient Term Algebras. Theor. Comput. Sci., 1993. 118(2):167-191.
• [19] Baader F, Schulz KU. Combination Techniques and Decision Problems for Disunification. Theor. Comput. Sci., 1995. 142(2):229-255. URL https://doi.org/10.1016/0304-3975(94)00277-0.
• [20] Comon H, Delor C. Equational Formulae with Membership Constraints. Inf. Comput., 1994. 112(2):167-216. URL https://doi.org/10.1006/inco.1994.1056.
• [21] Meseguer J, Skeirik S. Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras. In: Falaschi M (ed.), Proc. LOPSTR 2015, volume 9527. Springer LNCS, 2015 pp. 36-53. doi:10.1007/978-3-319-27436-2_3.
• [22] Giesl J, Kapur D. Decidable Classes of Inductive Theorems. In: Proc. IJCAR 2001, volume 2083. Springer LNCS, 2001 pp. 469-484. doi:10.1007/3-540-45744-5_41.
• [23] Giesl J, Kapur D. Deciding Inductive Validity of Equations. In: Proc. CADE 2003, volume 2741. Springer LNCS, 2003 pp. 17-31. doi:10.1007/978-3-540-45085-6_3.
• [24] Falke S, Kapur D. Rewriting Induction + Linear Arithmetic = Decision Procedure. In: Proc. IJCAR 2012, volume 7364. Springer LNCS, 2012 pp. 241-255. doi:10.1007/978-3-642-31365-3_20.
• [25] Aoto T, Stratulat S. Decision Procedures for Proving Inductive Theorems without Induction. In: Proc. PPDP2014. ACM, 2014 pp. 237-248. doi:10.1145/2643135.2643156.
• [26] Meseguer J. Variant-Based Satisfiability in Initial Algebras. In: Artho C, Ölveczky P (eds.), Proc. FTSCS 2015. Springer CCIS 596, 2016 pp. 3-34. doi:10.1007/978-3-319-29510-7_1.
• [27] Bae K, Meseguer J. Model checking linear temporal logic of rewriting formulas under localized fairness. Sci. Comput. Program., 2015. 99:193-234. URL https://doi.org/10.1016/j.scico.2014.02.006.
• [28] Futatsugi K. Fostering Proof Scores in CafeOBJ. In: Proc. ICFEM 2010, volume 6447. Springer LNCS, 2010 pp. 1-20. doi:10.1007/978-3-642-16901-4_1.
• [29] Skeirik S, Stefanescu A, Meseguer J. A Constructor-Based Reachability Logic for Rewrite Theories. In: Proc. Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, volume 10855 of Lecture Notes in Computer Science. Springer, 2017 pp. 201-217. doi:10.1007/978-3-319-94460-9_12.
• [30] Meseguer J. Variant-based satisfiability in initial algebras. Sci. Comput. Program., 2018. 154:3-41. doi:10.1007/978-3-319-29510-7_1.
• [31] Skeirik S, Meseguer J. Metalevel algorithms for variant satisfiability. J. Log. Algebr. Meth. Program., 2018. 96:81-110. URL https://doi.org/10.1016/j.jlamp.2017.12.006.
• [32] Meseguer J. Membership algebra as a logical framework for equational specification. In: Proc.WADT’97. Springer LNCS 1376, 1998 pp. 18-61. doi:10.1007/3-540-64299-4_26.
• [33] Goguen J, Meseguer J. Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. Theoretical Computer Science, 1992. 105:217-273. URL https://doi.org/10.1016/0304-3975(92)90302-V.
• [34] Clavel M, Durán F, Eker S, Meseguer J, Lincoln P, Martí-Oliet N, Talcott C. All About Maude - A High-Performance Logical Framework. Springer LNCS Vol. 4350, 2007. doi:10.1007/978-3-540-71999-1.
• [35] Dershowitz N, Jouannaud JP. Rewrite Systems. In: van Leeuwen J (ed.), Handbook of Theoretical Computer Science, Vol. B, pp. 243-320. North-Holland, 1990. URL https://doi.org/10.1016/B978-0-444-88074-1.50011-1.
• [36] Gutiérrez R, Meseguer J, Rocha C. Order-sorted equality enrichments modulo axioms. Sci. Comput. Program., 2015. 99:235-261. URL https://doi.org/10.1016/j.scico.2014.07.003.
• [37] Meseguer J. Generalized Rewrite Theories and Coherence Completion. In: Rusu V (ed.), Proc. Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, volume 11152 of Lecture Notes in Computer Science. Springer, 2018 pp. 164-183. URL http://hdl.handle.net/2142/102183.
• [38] Lucas S, Meseguer J. Normal forms and normal theories in conditional rewriting. J. Log. Algebr. Meth. Program., 2016. 85(1):67-97. URL https://doi.org/10.1016/j.jlamp.2015.06.001.
• [39] Durán F, Meseguer J. On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Log. Algebr. Program., 2012. 81(7-8):816-850. URL https://doi.org/10.1016/j.jlap.2011.12.004.
• [40] Meseguer J. Symbolic Reasoning Methods in Rewriting Logic and Maude. In: Moss LS, de Queiroz RJGB, Martínez M (eds.), Logic, Language, Information, and Computation - 25th International Workshop, WoLLIC 2018, Bogotá, Colombia, July 24-27, 2018, Proceedings, volume 10944 of Lecture Notes in Computer Science. Springer, 2018 pp. 25-60. doi:10.1007/978-3-662-57669-4_2.
• [41] Rocha C, Meseguer J, Muñoz CA. Rewriting Modulo SMT and Open System Analysis. Journal of Logic and Algebraic Methods in Programming, 2017. 86(1):269-297. URL https://doi.org/10.1016/j.jlamp.2016.10.001.
• [42] Bruni R, Meseguer J. Semantic foundations for generalized rewrite theories. Theor. Comput. Sci., 2006. 360(1-3):386-414. doi:10.1016/j.tcs.2006.04.012.
• [43] Comon-Lundth H, Delaune S. The finite variant property: how to get rid of some algebraic properties. In Proc RTA’05, Springer LNCS 3467, 294-307, 2005. doi:10.1007/978-3-540-32033-3_22.
• [44] Cholewa A, Meseguer J, Escobar S. Variants of Variants and the Finite Variant Property. Technical report, CS Dept. University of Illinois at Urbana-Champaign, 2014. URL http://hdl.handle.net/2142/47117.
• [45] Meseguer J. Generalized Rewrite Theories, Coherence Completion, and Symbolic Methods, 2019. To appear in Journal of Logical and Algebraic Methods in Programming.
• [46] Rocha C, Meseguer J. Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories. In: Proc. LPAR 2010, volume 6397 of Lecture Notes in Computer Science. Springer, 2010 pp. 594-609. doi:10.1007/978-3-642-16242-8_42.
• [47] Hoare CAR. An Axiomatic Basis for Computer Programming. Commun. ACM, 1969. 12(10):576-580.
• [48] Rosu G, Stefanescu A. From Hoare Logic to Matching Logic Reachability. In: Giannakopoulou D, Méry D (eds.), FM, volume 7436 of Lecture Notes in Computer Science. Springer. 2012 pp. 387-402. ISBN:978-3-642-32758-2.
• [49] Reynolds JC. Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS 2002. IEEE, 2002 pp. 55-74. doi:10.1109/LICS.2002.1029817.
• [50] Meseguer J, Roşu G. The Rewriting Logic Semantics Project. Theoretical Computer Science, 2007. 373(3):213-237. URL https://doi.org/10.1016/j.tcs.2006.12.018.
• [51] Ellison C, Rosu G. An executable formal semantics of C with applications. In: Field J, Hicks M (eds.), POPL. ACM. 2012 pp. 533-544. ISBN: 978-1-4503-1083-3.
• [52] Dowek G, Hardin T, Kirchner C. Theorem Proving Modulo. J. Autom. Reasoning, 2003. 31(1):33-72. doi:10.1023/A:1027357912519.
• [53] Viry P. Adventures in sequent calculus modulo equations. Electr. Notes Theor. Comput. Sci., 1998. 15:21-32. doi:10.1016/S1571-0661(05)82550-2.
• [54] Rocha C, Meseguer J. Theorem Proving Modulo Based on Boolean Equational Procedures. In: Proc. RelMiCS 2008, volume 4988. Springer LNCS, 2008 pp. 337-351. doi:10.1007/978-3-540-78913-0_25.
• [55] Durán F, Ölveczky PC. A Guide to Extending Full Maude Illustrated with the Implementation of Real-Time Maude. Electronic Notes in Theoretical Computer Science, 2009. 238(3):83-102. URL https://doi.org/10.1016/j.entcs.2009.05.014.
• [56] Skeirik S, Meseguer J. Metalevel Algorithms for Variant-Based Satisfiability. In: Lucanu D (ed.), Proc. WRLA 2016, volume 9942. Springer LNCS, 2016 pp. 167-184. doi:10.1007/978-3-319-44802-2_10.
• [57] Durán F, Eker S, Escobar S, Martí-Oliet N, Meseguer J, Talcott CL. Associative Unification and Symbolic Reasoning Modulo Associativity in Maude. In: Rusu V (ed.), Proc. Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, volume 11152 of Lecture Notes in Computer Science. Springer, 2018 pp. 98-114. doi:10.1007/978-3-319-99840-4_6.
• [58] Rosu G, Stefanescu A. Checking reachability using matching logic. In: Proc. OOPSLA 2012. ACM, 2012 pp. 555-574. doi:10.1145/2398857.2384656.
• [59] Moore B. Coinductive Program Verification. Ph.D. thesis, University of Illinois at Urbana-Champaign, 2016. URL http://hdl.handle.net/2142/95372.
• [60] Lucanu D, Rusu V, Arusoaie A. A generic framework for symbolic execution: A coinductive approach. J. Symb. Comput., 2017. 80(1):125-163. URL https://doi.org/10.1016/j.jsc.2016.07.012.
• [61] Ştefan Ciobâcă, Lucanu D. A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. In: Proc. IJCAR 2018, volume 10900 of Lecture Notes in Computer Science. Springer, 2018 pp. 295-311. doi:10.1007/978-3-319-94205-6_20.
• [62] Futatsugi K, Diaconescu R. CafeOBJ Report. World Scientific, 1998.
• [63] Goguen J. OBJ as a Theorem Prover with Application to Hardware Verification. In: Subramanyam P, Birtwistle G (eds.), Current Trends in Hardware Verification and Automated Theorem Proving, pp. 219-267. Springer-Verlag, 1989. doi:10.1007/978-1-4612-3658-0_5.
• [64] Futatsugi K. Generate & Check Method for Verifying Transition Systems in CafeOBJ. In: De Nicola R, Hennicker R (eds.), Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, volume 8950 of Lecture Notes in Computer Science. Springer, 2015 pp. 171-192. doi:10.1007/978-3-319-15545-6_13.
• [65] Gâinâ D, Lucanu D, Ogata K, Futatsugi K. On Automation of OTS/CafeOBJ Method. In: Iida S, Meseguer J, Ogata K (eds.), Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi, volume 8373 of Lecture Notes in Computer Science. Springer, 2014 pp. 578-602. doi:10.1007/978-3-642-54624-2_29.
• [66] Riesco A, Ogata K. Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores. ACM Trans. Softw. Eng. Methodol., 2018. 27(2):6:1-6:32. URL https://doi.org/10.1145/3208951.
• [67] Rocha C, Meseguer J. Proving Safety Properties of Rewrite Theories, 2011. In Proc. CALCO 2011, Springer LNCS 6859, pp. 314-328. doi:10.1007/978-3-642-22944-2_22.
• [68] Rocha C. Symbolic Reachability Analysis for Rewrite Theories. Ph.D. thesis, University of Illinois at Urbana-Champaign, 2012.
• [69] Rocha C, Meseguer J. Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool. In: Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi, volume 8373 of Lecture Notes in Computer Science. Springer, 2014 pp. 603-629. doi:10.1007/978-3-642-54624-2_30.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).