×

Generalized rewrite theories, coherence completion, and symbolic methods. (English) Zbl 1496.68166

Summary: A new notion of generalized rewrite theory suitable for symbolic reasoning and generalizing the standard notion in [R. Bruni and the author, Theor. Comput. Sci. 360, No. 1–3, 386–414 (2006; Zbl 1097.68051)] is motivated and defined. Also, new requirements for symbolic executability of generalized rewrite theories that extend those in [F. Durán and the author, J. Log. Algebr. Program. 81, No. 7–8, 816–850 (2012; Zbl 1272.03139)] for standard rewrite theories, including a generalized notion of coherence, are given. Symbolic executability, including coherence, is both ensured and made available for a wide class of such theories by automatable theory transformations. Using these foundations, several symbolic reasoning methods using generalized rewrite theories are studied, including: (i) symbolic description of sets of terms by pattern predicates; (ii) reasoning about universal reachability properties by generalized rewriting; (iii) reasoning about existential reachability properties by constrained narrowing; and (iv) symbolic verification of safety properties such as invariants and stability properties.

MSC:

68Q42 Grammars and rewriting systems
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Abdulla, P.; Jonsson, B.; Mahata, P.; d’Orso, J., Regular tree model checking, (Computer Aided Verification (2002), Springer), 452-466
[2] Althaus, E.; Kruglov, E.; Weidenbach, C., Superposition modulo linear arithmetic SUP(LA), (Ghilardi, S.; Sebastiani, R., FroCos. FroCos, Lecture Notes in Computer Science, vol. 5749 (2009), Springer), 84-99 · Zbl 1193.03024
[3] Alur, R.; Courcoubetis, C.; Henzinger, T. A.; Ho, P. H., Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems, (Grossman, R.; Nerode, A.; Ravn, A.; Rischel, H., Workshop on Theory of Hybrid Systems. Workshop on Theory of Hybrid Systems, LNCS, vol. 739 (1993), Springer), 209-229
[4] Alur, R.; Dill, D. L., A theory of timed automata, Theor. Comput. Sci., 126, 2, 183-235 (1994) · Zbl 0803.68071
[5] Alur, R.; Madhusudan, P., Adding nesting structure to words, J. ACM, 56, 3 (2009) · Zbl 1325.68138
[6] Armando, A.; Mantovani, J.; Platania, L., Bounded model checking of software using SMT solvers instead of SAT solvers, (Valmari, A., Model Checking Software, Proceedings of the 13th International SPIN Workshop. Model Checking Software, Proceedings of the 13th International SPIN Workshop, Vienna, Austria, March 30 - April 1, 2006. Model Checking Software, Proceedings of the 13th International SPIN Workshop. Model Checking Software, Proceedings of the 13th International SPIN Workshop, Vienna, Austria, March 30 - April 1, 2006, Lecture Notes in Computer Science, vol. 3925 (2006), Springer), 146-162 · Zbl 1178.68148
[7] Arusoaie, A.; Lucanu, D.; Rusu, V., Symbolic execution based on language transformation, Comput. Lang. Syst. Struct., 44, 48-71 (2015) · Zbl 1387.68047
[8] Ayala-Rincón, M., Expressiveness of Conditional Equational Systems with Built-in Predicates (1993), Universität Kaiserslauten, Ph.D. thesis
[9] Bae, K.; Escobar, S.; Meseguer, J., Abstract logical model checking of infinite-state systems using narrowing, (Rewriting Techniques and Applications. Rewriting Techniques and Applications, RTA’13. Rewriting Techniques and Applications. Rewriting Techniques and Applications, RTA’13, LIPIcs, vol. 21 (2013), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 81-96 · Zbl 1356.68140
[10] Bae, K.; Meseguer, J., Infinite-state model checking of LTLR formulas using narrowing, (Proc. WRLA 2014. Proc. WRLA 2014, LNCS, vol. 8663 (2014), Springer), 113-129 · Zbl 1366.68162
[11] Bae, K.; Rocha, C., Guarded terms for rewriting modulo SMT, (Formal Aspects of Component Software - Proceedings of the 14th International Conference. Formal Aspects of Component Software - Proceedings of the 14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017 (2017)), 78-97
[12] Bergstra, J.; Tucker, J., Characterization of computable data types by means of a finite equational specification method, (de Bakker, J. W.; van Leeuwen, J., Automata, Languages and Programming, Seventh Colloquium. Automata, Languages and Programming, Seventh Colloquium, LNCS, vol. 81 (1980), Springer-Verlag), 76-90 · Zbl 0449.68003
[13] Beyer, D.; Keremoglu, M. E., Cpachecker: a tool for configurable software verification, (Proc CAV 2011. Proc CAV 2011, LNCS, vol. 6806 (2011), Springer), 184-190
[14] Bouajjani, A., Languages, rewriting systems, and verification of infinite-state systems, Autom. Lang. Program., 24-39 (2001) · Zbl 0986.68517
[15] Bouajjani, A.; Esparza, J., Rewriting models of boolean programs, (Term Rewriting and Applications (2006)), 136-150 · Zbl 1151.68440
[16] Bouajjani, A.; Jonsson, B.; Nilsson, M.; Touili, T., Regular model checking, (Computer Aided Verification (2000), Springer), 403-418 · Zbl 0974.68118
[17] Bouhoula, A.; Rusinowitch, M., Implicit induction in conditional theories, J. Autom. Reason., 14, 189-235 (1995) · Zbl 0819.68114
[18] Bozzano, M.; Cavada, R.; Cimatti, A.; Dorigatti, M.; Griggio, A.; Mariotti, A.; Micheli, A.; Mover, S.; Roveri, M.; Tonetta, S., nuXmv 1.0 User Manual (2014), Tech. Rep., FBK
[19] Bruni, R.; Meseguer, J., Semantic foundations for generalized rewrite theories, Theor. Comput. Sci., 360, 1-3, 386-414 (2006) · Zbl 1097.68051
[20] Cholewa, A.; Escobar, S.; Meseguer, J., Constrained narrowing for conditional equational theories modulo axioms, Sci. Comput. Program., 112, 24-57 (2015)
[21] Cimatti, A.; Griggio, A.; Mover, S.; Tonetta, S., HyComp: an SMT-based model checker for hybrid systems, (Proc. TACAS 2015. Proc. TACAS 2015, LNCS, vol. 9035 (2015), Springer), 52-67
[22] Ciobâcă, Ştefan; Arusoaie, A.; Lucanu, D., Unification modulo builtins, (Logic, Language, Information, and Computation - Proceedings of the 25th International Workshop. Logic, Language, Information, and Computation - Proceedings of the 25th International Workshop, WoLLIC 2018, Bogota, Colombia, July 24-27, 2018. Logic, Language, Information, and Computation - Proceedings of the 25th International Workshop. Logic, Language, Information, and Computation - Proceedings of the 25th International Workshop, WoLLIC 2018, Bogota, Colombia, July 24-27, 2018, LNCS, vol. 10944 (2018), Springer), 179-195 · Zbl 1509.68116
[23] Ciobâcă, Ştefan; Lucanu, D., A coinductive approach to proving reachability properties in logically constrained term rewriting systems, (Proc. IJCAR 2018. Proc. IJCAR 2018, Lecture Notes in Computer Science, vol. 10900 (2018), Springer), 295-311 · Zbl 1511.68132
[24] Clavel, M.; Durán, F.; Eker, S.; Meseguer, J.; Lincoln, P.; Martí-Oliet, N.; Talcott, C., All About Maude - A High-Performance Logical Framework, LNCS, vol. 4350 (2007), Springer · Zbl 1115.68046
[25] Comon, H., Equational formulas in order-sorted algebras, (Proc. ICALP’90. Proc. ICALP’90, LNCS, vol. 443 (1990), Springer), 674-688 · Zbl 0774.68071
[26] Comon, H.; Delor, C., Equational formulae with membership constraints, Inf. Comput., 112, 2, 167-216 (1994) · Zbl 0827.03020
[27] Comon, H.; Nieuwenhuis, R., Induction=i-axiomatization+first-order consistency, Inf. Comput., 159, 1-2, 151-186 (2000) · Zbl 1046.68640
[28] Comon-Lundth, H.; Delaune, S., The finite variant property: how to get rid of some algebraic properties, (Proc RTA’05. Proc RTA’05, LNCS, vol. 3467 (2005), Springer), 294-307 · Zbl 1078.68059
[29] Cordeiro, L.; Fischer, B.; Marques-Silva, J., SMT-based bounded model checking for embedded ANSI-c software, (ASE (2009), IEEE), 137-148
[30] Delzanno, G.; Podelski, A., Constraint-based deductive model checking, Int. J. Softw. Tools Technol. Transf., 3, 3, 250-270 (2001) · Zbl 0991.68013
[31] Dershowitz, N.; Jouannaud, J. P., Rewrite systems, (van Leeuwen, J., Handbook of Theoretical Computer Science, Vol. B (1990), North-Holland), 243-320 · Zbl 0900.68283
[32] Dijkstra, E.; Scholten, C., Petri Nets (1990), Springer-Verlag
[33] Durán, F.; Meseguer, J., On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, J. Log. Algebraic Program., 81, 816-850 (2012) · Zbl 1272.03139
[34] Ehrig, H.; Mahr, B., Fundamentals of Algebraic Specification 1 (1985), Springer · Zbl 0557.68013
[35] Escobar, S.; Meadows, C.; Meseguer, J., Maude-NPA: cryptographic protocol analysis modulo equational properties, (Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures. Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, LNCS, vol. 5705 (2009), Springer), 1-50 · Zbl 1252.94061
[36] Escobar, S.; Meadows, C.; Meseguer, J.; Santiago, S., State space reduction in the Maude-NRL protocol analyzer, Inf. Comput., 238, 157-186 (2014) · Zbl 1360.94307
[37] Escobar, S.; Meadows, C.; Meseguer, J.; Santiago, S., Symbolic protocol analysis with disequality constraints modulo equational theories, (Programming Languages with Applications to Biology and Security - Essays in Honour of Pierpaolo Degano on the Occasion of His 65th Birthday. Programming Languages with Applications to Biology and Security - Essays in Honour of Pierpaolo Degano on the Occasion of His 65th Birthday, LNCS, vol. 9465 (2015), Springer), 238-261 · Zbl 1437.94060
[38] Escobar, S.; Meseguer, J., Symbolic model checking of infinite-state systems using narrowing, (Proc. RTA. Proc. RTA, Lecture Notes in Computer Science, vol. 4533 (2007)), 153-168 · Zbl 1203.68097
[39] Escobar, S.; Sasse, R.; Meseguer, J., Folding variant narrowing and optimal variant termination, J. Log. Algebraic Program., 81, 898-928 (2012) · Zbl 1291.68217
[40] Falke, S., Term Rewriting with Built-In Numbers and Collection Data Structures (2009), University of New: University of New Mexico, Ph.D. thesis
[41] Falke, S.; Kapur, D., Dependency pairs for rewriting with built-in numbers and semantic data structures, (19th International Conference on Rewriting Techniques and Applications. 19th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 5117 (2008), Springer: Springer Berlin, Heidelberg), 94-109 · Zbl 1145.68445
[42] Falke, S.; Kapur, D., Operational termination of conditional rewriting with built-in numbers and semantic data structures, Electron. Notes Theor. Comput. Sci., 237, 75-90 (2009) · Zbl 1294.68096
[43] Falke, S.; Kapur, D., Rewriting induction + linear arithmetic = decision procedure, (Proc. IJCAR 2012. Proc. IJCAR 2012, LNCS, vol. 7364 (2012), Springer), 241-255 · Zbl 1358.68252
[44] Futatsugi, K., Fostering proof scores in CafeOBJ, (Proc. ICFEM 2010. Proc. ICFEM 2010, LNCS, vol. 6447 (2010), Springer), 1-20
[45] Ganai, M.; Gupta, A., Accelerating high-level bounded model checking, (2006 IEEE/ACM International Conference on Computer Aided Design (Nov 2006)), 794-801
[46] Ganai, M.; Gupta, A., Completeness in SMT-based BMC for software programs, (DATE (2008), IEEE), 831-836
[47] Ganzinger, H.; Nieuwenhuis, R., Constraints and theorem proving, (Constraints in Computational Logics: Theory and Applications, International Summer School, CCL’99, Gif-sur-Yvette, France, September 5-8, 1999, Revised Lectures. Constraints in Computational Logics: Theory and Applications, International Summer School, CCL’99, Gif-sur-Yvette, France, September 5-8, 1999, Revised Lectures, Lecture Notes in Computer Science, vol. 2002 (1999), Springer), 159-201 · Zbl 0976.03518
[48] Genet, T.; Tong, V., Reachability analysis of term rewriting systems with Timbuk, (Logic for Programming, Artificial Intelligence, and Reasoning (2001), Springer), 695-706 · Zbl 1275.68083
[49] Ghilardi, S.; Nicolini, E.; Ranise, S.; Zucchelli, D., Towards SMT model checking of array-based systems, (Automated Reasoning, Proceedings of the 4th International Joint Conference. Automated Reasoning, Proceedings of the 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008. Automated Reasoning, Proceedings of the 4th International Joint Conference. Automated Reasoning, Proceedings of the 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Lecture Notes in Computer Science, vol. 5195 (2008), Springer), 67-82 · Zbl 1165.68406
[50] Ghilardi, S.; Ranise, S., MCMT: a model checker modulo theories, (Proc. Automated Reasoning, 5th International Joint Conference. Proc. Automated Reasoning, 5th International Joint Conference, IJCAR 2010. Proc. Automated Reasoning, 5th International Joint Conference. Proc. Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Lecture Notes in Computer Science, vol. 6173 (2010), Springer), 22-29 · Zbl 1291.68257
[51] Goguen, J.; Meseguer, J., Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci., 105, 217-273 (1992) · Zbl 0778.68056
[52] Gurfinkel, A.; Kahsai, T.; Komuravelli, A.; Navas, J. A., The seahorn verification framework, (Proc. CAV 2015, Part I. Proc. CAV 2015, Part I, LNCS, vol. 9206 (2015), Springer), 343-361
[53] Gutiérrez, R.; Meseguer, J.; Rocha, C., Order-sorted equality enrichments modulo axioms, Sci. Comput. Program., 99, 235-261 (2015)
[54] Jaffar, J.; Maher, M. J., Constraint logic programming: a survey, J. Log. Program., 19/20, 503-581 (1994)
[55] Jouannaud, J. P.; Kirchner, H., Completion of a set of rules modulo a set of equations, SIAM J. Comput., 15, 1155-1194 (November 1986) · Zbl 0665.03005
[56] Kahsai, T.; Tinelli, C., PKind: a parallel k-induction based model checker, (Proc. PDMC 2011. Proc. PDMC 2011, EPTCS, vol. 72 (2011)), 55-62
[57] Kirchner, H.; Ringeissen, C., Combining symbolic constraint solvers on algebraic domains, J. Symb. Comput., 18, 2, 113-155 (1994) · Zbl 0819.68111
[58] Kirchner, H.; Ringeissen, C., Constraint solving by narrowing in combined algebraic domains, (Logic Programming, Proceedings of the Eleventh International Conference on Logic Programming (1994), MIT Press), 617-631
[59] Kirchner, K.; Kirchner, H.; Rusinowitch, M., Deduction with symbolic constraints, Rev. Intell. Artif., 4, 3, 9-52 (1990)
[60] Kop, C.; Nishida, N., Term rewriting with logical constraints, (9th International Symposium on Frontiers of Combining Systems. 9th International Symposium on Frontiers of Combining Systems, Lecture Notes in Computer Science, vol. 8152 (2013), Springer), 343-358 · Zbl 1398.68276
[61] Kop, C.; Nishida, N., Automatic constrained rewriting induction towards verifying procedural programs, (Garrigue, J., Programming Languages and Systems - Proceedings of the 12th Asian Symposium. Programming Languages and Systems - Proceedings of the 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014. Programming Languages and Systems - Proceedings of the 12th Asian Symposium. Programming Languages and Systems - Proceedings of the 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Lecture Notes in Computer Science, vol. 8858 (2014), Springer), 334-353 · Zbl 1453.68050
[62] Kreisel, G.; Krivine, J., Mathematical Logic (1967), North-Holland · Zbl 0155.33801
[63] 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
[64] Lucanu, D.; Rusu, V.; Arusoaie, A.; Nowak, D., Verifying reachability-logic properties on rewriting-logic specifications, (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, LNCS, vol. 9200 (2015), Springer), 451-474 · Zbl 1321.68359
[65] Lucas, S.; Meseguer, J., Normal forms and normal theories in conditional rewriting, J. Log. Algebraic Methods Program., 85, 1, 67-97 (2016) · Zbl 1356.68124
[66] MacLane, S., Categories for the Working Mathematician (1971), Springer-Verlag · Zbl 0232.18001
[67] Manes, E., Algebraic Theories, Graduate Texts in Mathematics, vol. 26 (1976), Springer · Zbl 0353.18007
[68] Meseguer, J.; Thati, P., Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols, High.-Order Symb. Comput., 20, 1-2, 123-160 (2007) · Zbl 1115.68079
[69] Meseguer, J., General logics, (H. D.E.; etal., Logic Colloquium ’87 (1989), North-Holland), 275-329 · Zbl 0691.03001
[70] Meseguer, J., Membership algebra as a logical framework for equational specification, (Proc. WADT’97. Proc. WADT’97, LNCS, vol. 1376 (1998), Springer), 18-61 · Zbl 0903.08009
[71] Meseguer, J., Strict coherence of conditional rewriting modulo axioms, Theor. Comput. Sci., 672, 1-35 (2017) · Zbl 1386.68080
[72] Meseguer, J., Generalized rewrite theories and coherence completion, (Rusu, V., Proc. Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018. Proc. Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Lecture Notes in Computer Science, vol. 11152 (2018), Springer), 164-183 · Zbl 1517.68166
[73] Meseguer, J., Variant-based satisfiability in initial algebras, Sci. Comput. Program., 154, 3-41 (2018) · Zbl 1396.68074
[74] Meseguer, J.; Goguen, J., Initiality, induction and computability, (Nivat, M.; Reynolds, J., Algebraic Methods in Semantics (1985), Cambridge University Press), 459-541 · Zbl 0571.68004
[75] Meseguer, J.; Palomino, M.; Martí-Oliet, N., Equational abstractions, Theor. Comput. Sci., 403, 2-3, 239-264 (2008) · Zbl 1155.68050
[76] Meseguer, J.; Skeirik, S., Equational formulas and pattern operations in initial order-sorted algebras, Form. Asp. Comput., 29, 3, 423-452 (2017) · Zbl 1362.68054
[77] Milicevic, A.; Kugler, H., Model checking using SMT and theory of lists, (NASA 3rd International Symposium on Formal Methods. NASA 3rd International Symposium on Formal Methods, Lecture Notes in Computer Science, vol. 6617 (2011), Springer), 282-297
[78] Moore, B., Coinductive Program Verification (2016), University of Illinois at Urbana-Champaign, Ph.D. thesis
[79] de Moura, L. M.; Owre, S.; Rueß, H.; Rushby, J. M.; Shankar, N.; Sorea, M.; Tiwari, A., SAL 2, (Proc. CAV 2004. Proc. CAV 2004, LNCS, vol. 3114 (2004), Springer), 496-500 · Zbl 1103.68644
[80] Ohsaki, H.; Seki, H.; Takai, T., Recognizing boolean closed a-tree languages with membership conditional rewriting mechanism, (Rewriting Techniques and Applications (2003), Springer), 483-498 · Zbl 1038.68070
[81] Peterson, G. E.; Stickel, M. E., Complete sets of reductions for some equational theories, J. Assoc. Comput. Mach., 28, 2, 233-264 (1981) · Zbl 0479.68092
[82] Podelski, A., Model checking as constraint solving, (Static Analysis, Proceedings of the 7th International Symposium. Static Analysis, Proceedings of the 7th International Symposium, SAS 2000, Santa Barbara, CA, USA, June 29 - July 1, 2000. Static Analysis, Proceedings of the 7th International Symposium. Static Analysis, Proceedings of the 7th International Symposium, SAS 2000, Santa Barbara, CA, USA, June 29 - July 1, 2000, Lecture Notes in Computer Science, vol. 1824 (2000), Springer), 22-37 · Zbl 0966.68121
[83] Rocha, C.; Meseguer, J., Proving safety properties of rewrite theories, (Proc. CALCO 2011. Proc. CALCO 2011, LNCS, vol. 6859 (2011), Springer), 314-328 · Zbl 1344.68142
[84] Rocha, C., Symbolic Reachability Analysis for Rewrite Theories (2012), University of Illinois at Urbana-Champaign, Ph.D. thesis
[85] Rocha, C.; Meseguer, J., Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool, (Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi. Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi, Lecture Notes in Computer Science, vol. 8373 (2014), Springer), 603-629 · Zbl 1407.68302
[86] Rocha, C.; Meseguer, J.; Muñoz, C. A., Rewriting modulo SMT and open system analysis, (Proc. Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014. Proc. Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Lecture Notes in Computer Science, vol. 8663 (2014), Springer), 247-262 · Zbl 1367.68151
[87] Rocha, C.; Meseguer, J.; Muñoz, C. A., Rewriting modulo SMT and open system analysis, J. Log. Algebraic Methods Program., 86, 269-297 (2017) · Zbl 1353.68156
[88] Rybina, T.; Voronkov, A., A logical reconstruction of reachability, (Perspectives of Systems Informatics, 5th International Andrei Ershov Memorial Conference, Revised Papers. Perspectives of Systems Informatics, 5th International Andrei Ershov Memorial Conference, Revised Papers, PSI 2003, Akademgorodok, Novosibirsk, Russia, July 9-12, 2003. Perspectives of Systems Informatics, 5th International Andrei Ershov Memorial Conference, Revised Papers. Perspectives of Systems Informatics, 5th International Andrei Ershov Memorial Conference, Revised Papers, PSI 2003, Akademgorodok, Novosibirsk, Russia, July 9-12, 2003, Lecture Notes in Computer Science, vol. 2890 (2003), Springer), 222-237 · Zbl 1254.68153
[89] Shoenfield, J. R., Degrees of Unsolvability (1971), North-Holland · Zbl 0245.02037
[90] Skeirik, S.; Meseguer, J., Metalevel algorithms for variant satisfiability, J. Log. Algebraic Methods Program., 96, 81-110 (2018) · Zbl 1430.68423
[91] Skeirik, S.; Stefanescu, A.; Meseguer, J., A constructor-based reachability logic for rewrite theories, (Proc. Logic-Based Program Synthesis and Transformation - 27th International Symposium. Proc. Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017. Proc. Logic-Based Program Synthesis and Transformation - 27th International Symposium. Proc. Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Lecture Notes in Computer Science, vol. 10855 (2017), Springer), 201-217 · Zbl 1471.68075
[92] Stefanescu, A.; Ciobâcă, Ştefan; Mereuta, R.; Moore, B. M.; Serbanuta, T.; Rosu, G., All-path reachability logic, (Proc. RTA-TLCA 2014. Proc. RTA-TLCA 2014, LNCS, vol. 8560 (2014), Springer), 425-440 · Zbl 1416.68052
[93] Stefanescu, A.; Park, D.; Yuwen, S.; Li, Y.; Rosu, G., Semantics-based program verifiers for all languages, (Proc. OOPSLA 2016 (2016), ACM), 74-91
[94] Tiwari, A., Hybrids al relational abstracter, (Proc. CAV 2012. Proc. CAV 2012, LNCS, vol. 7358 (2012), Springer), 725-731
[95] Veanes, M.; Bjørner, N.; Raschke, A., An SMT approach to bounded reachability analysis of model programs, (28th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (2008), Springer), 53-68
[96] Vidal, G., Closed symbolic execution for verifying program termination, (IEEE 12th International Working Conference on Source Code Analysis and Manipulation (Sept 2012)), 34-43
[97] Vidal, G., Symbolic execution as a basis for termination analysis, Sci. Comput. Program., 102, 142-157 (2015)
[98] Viry, P., Equational rules for rewriting logic, Theor. Comput. Sci., 285, 487-517 (2002) · Zbl 1001.68058
[99] Walter, D.; Little, S.; Myers, C., Bounded model checking of analog and mixed-signal circuits using an SMT solver, (5th International Symposium on Automated Technology for Verification and Analysis (2007), Springer: Springer Berlin, Heidelberg), 66-81 · Zbl 1141.68494
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.