×

Rewriting modulo SMT and open system analysis. (English) Zbl 1353.68156

Summary: This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze reachability properties of infinite-state open systems, i.e., systems that interact with a nondeterministic environment. Such systems exhibit both internal nondeterminism, which is proper to the system, and external nondeterminism, which is due to the environment. In a reflective formalism, such as rewriting logic, rewriting modulo SMT can be reduced to standard rewriting. Hence, rewriting modulo SMT naturally extends rewriting-based reachability analysis techniques, which are available for closed systems, to open systems. Furthermore, a single state expression with symbolic constraints can now denote an infinite set of concrete states. The proposed technique is illustrated with the formal analysis of: (i) a real-time system that is beyond the scope of timed-automata methods and (ii) automatic detection of reachability violations in a synchronous language developed to support autonomous spacecraft operations.

MSC:

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

References:

[1] Althaus, E.; Kruglov, E.; Weidenbach, C., Superposition modulo linear arithmetic SUP(LA), (7th International Symposium on Frontiers of Combining Systems. 7th International Symposium on Frontiers of Combining Systems, Lect. Notes Comput. Sci., vol. 5749 (2009), Springer), 84-99 · Zbl 1193.03024
[2] Alur, R.; Dill, D. L., A theory of timed automata, Theor. Comput. Sci., 126, 2, 183-235 (1994) · Zbl 0803.68071
[3] Armando, A.; Mantovani, J.; Platania, L., Bounded model checking of software using SMT solvers instead of SAT solvers, Int. J. Softw. Tools Technol. Transf., 11, 1, 69-83 (2009)
[4] Arusoaie, A.; Lucanu, D.; Rusu, V., A generic framework for symbolic execution, (6th International Conference on Software Language Engineering. 6th International Conference on Software Language Engineering, Lect. Notes Comput. Sci., vol. 8225 (2013), Springer), 281-301
[5] Ayala-Rincón, M., Expressiveness of Conditional Equational Systems with Built-in Predicates (1993), Universität Kaiserslauten, PhD thesis
[6] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press
[7] Baader, F.; Schulz, K., Unification in the union of disjoint equational theories: combining decision procedures, J. Symb. Comput., 21, 211-243 (1996) · Zbl 0851.68055
[8] Bae, K.; Escobar, S.; Meseguer, J., Abstract logical model checking of infinite-state systems using narrowing, (24th International Conference on Rewriting Techniques and Applications. 24th International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics, vol. 21 (2013), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik), 81-96 · Zbl 1356.68140
[9] Bae, K.; Rocha, C., A note on symbolic reachability analysis modulo integer constraints for the CASH algorithm (2012), available at
[10] Bonacina, M. P.; Lynch, C.; de Moura, L. M., On deciding satisfiability by theorem proving with speculative inferences, J. Autom. Reason., 47, 2, 161-189 (2011) · Zbl 1243.68265
[11] Boudet, A., Combining unification algorithms, J. Symb. Comput., 16, 6, 597-626 (1993) · Zbl 0822.68054
[12] Bouhoula, A.; Jacquemard, F., Automated induction with constrained tree automata, (4th International Joint Conference on Automated Reasoning. 4th International Joint Conference on Automated Reasoning, Lect. Notes Comput. Sci., vol. 5195 (2008), Springer), 539-554 · Zbl 1165.68452
[13] Bouhoula, A.; Jacquemard, F., Sufficient completeness verification for conditional and constrained TRS, J. Appl. Log., 10, 1, 127-143 (2012), Special issue on Automated Specification and Verification of Web Systems · Zbl 1279.68228
[14] Bruni, R.; Meseguer, J., Semantic foundations for generalized rewrite theories, Theor. Comput. Sci., 360, 1-3, 386-414 (2006) · Zbl 1097.68051
[15] Caccamo, M.; Buttazzo, G. C.; Sha, L., Capacity sharing for overrun control, (IEEE 34th Real-Time Systems Symposium (2000), IEEE Computer Society), 295-304
[16] Cadar, C.; Dunbar, D.; Engler, D. R., KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs, (8th USENIX Symposium on Operating Systems Design and Implementation (2008), USENIX Association), 209-224
[17] Cadar, C.; Sen, K., Symbolic execution for software testing: three decades later, Commun. ACM, 56, 2, 82-90 (Feb. 2013)
[18] Cimatti, A.; Griggio, A., Software model checking via IC3, (24th International Conference on Computer Aided Verification. 24th International Conference on Computer Aided Verification, Lect. Notes Comput. Sci., vol. 7358 (2012), Springer), 277-293
[19] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C. L., All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lect. Notes Comput. Sci., vol. 4350 (2007), Springer · Zbl 1115.68046
[20] Clavel, M.; Meseguer, J.; Palomino, M., Reflection in membership equational logic, many-sorted equational logic, horn logic with equality, and rewriting logic, Theor. Comput. Sci., 373, 1-2, 70-91 (2007) · Zbl 1111.03034
[21] Delzanno, G.; Podelski, A., Constraint-based deductive model checking, Int. J. Softw. Tools Technol. Transf., 3, 3, 250-270 (2001) · Zbl 0991.68013
[22] Dowek, G.; Muñoz, C.; Păsăreanu, C., A formal analysis framework for PLEXIL, (3rd Workshop on Planning and Plan Execution for Real-World Systems (September 2007)), 45-51
[23] Dowek, G.; Muñoz, C.; Păsăreanu, C., A Small-Step Semantics of PLEXIL (2008), National Institute of Aerospace: National Institute of Aerospace Hampton, VA, Technical Report 2008-11
[24] Dowek, G.; Muñoz, C. A.; Rocha, C., Rewriting logic semantics of a plan execution language, (6th Workshop on Structural Operational Semantics. 6th Workshop on Structural Operational Semantics, Electron. Proc. Theor. Comput. Sci., vol. 18 (2009)), 77-91 · Zbl 1454.68064
[25] Durán, F.; Lucas, S.; Marché, C.; Meseguer, J.; Urbain, X., Proving operational termination of membership equational programs, High.-Order Symb. Comput., 21, 1-2, 59-88 (2008) · Zbl 1192.68154
[26] Estlin, T.; Jónsson, A.; Păsăreanu, C.; Simmons, R.; Tso, K.; Verma, V., Plan Execution Interchange Language (PLEXIL) (2006), NASA, Technical Memorandum TM-2006-213483
[27] 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, Lect. Notes Comput. Sci., vol. 5117 (2008), Springer: Springer Berlin, Heidelberg), 94-109 · Zbl 1145.68445
[28] 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
[29] Falke, S.; Kapur, D., Rewriting induction + linear arithmetic = decision procedure, (6th International Joint Conference on Automated Reasoning. 6th International Joint Conference on Automated Reasoning, Lect. Notes Comput. Sci., vol. 7364 (2012), Springer), 241-255 · Zbl 1358.68252
[30] Ganai, M.; Gupta, A., Accelerating high-level bounded model checking, (2006 IEEE/ACM International Conference on Computer Aided Design (Nov. 2006)), 794-801
[31] Ganzinger, H.; Nieuwenhuis, R., Constraints and theorem proving, (Constraints in Computational Logics: Theory and Applications, International Summer School. Constraints in Computational Logics: Theory and Applications, International Summer School, Lect. Notes Comput. Sci., vol. 2002 (1999), Springer), 159-201 · Zbl 0976.03518
[32] Genet, T.; Le Gall, T.; Legay, A.; Murat, V., A completion algorithm for lattice tree automata, (18th International Conference on Implementation and Application of Automata. 18th International Conference on Implementation and Application of Automata, Lect. Notes Comput. Sci., vol. 7982 (2013), Springer), 134-145 · Zbl 1298.68135
[33] Ghilardi, S.; Nicolini, E.; Ranise, S.; Zucchelli, D., Combination methods for satisfiability and model-checking of infinite-state systems, (21st International Conference on Automated Deduction. 21st International Conference on Automated Deduction, Lect. Notes Comput. Sci., vol. 4603 (2007), Springer), 362-378 · Zbl 1213.68378
[34] Ghilardi, S.; Nicolini, E.; Ranise, S.; Zucchelli, D., Towards SMT model checking of array-based systems, (4th International Joint Conference on Automated Reasoning. 4th International Joint Conference on Automated Reasoning, Lect. Notes Comput. Sci., vol. 5195 (2008), Springer), 67-82 · Zbl 1165.68406
[35] Ghilardi, S.; Ranise, S., MCMT: a model checker modulo theories, (5th International Joint Conference on Automated Reasoning. 5th International Joint Conference on Automated Reasoning, Lect. Notes Comput. Sci., vol. 6173 (2010), Springer), 22-29 · Zbl 1291.68257
[36] Goguen, J. A.; Meseguer, J., Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci., 105, 2, 217-273 (1992) · Zbl 0778.68056
[37] Hojjat, H.; Rümmer, P.; Subotic, P.; Yi, W., Horn clauses for communicating timed systems, (Bjørner, N.; Fioravanti, F.; Rybalchenko, A.; Senni, V., 1st Workshop on Horn Clauses for Verification and Synthesis. 1st Workshop on Horn Clauses for Verification and Synthesis, Electron. Proc. Theor. Comput. Sci., vol. 169 (2014)), 39-52 · Zbl 1464.68207
[38] Kirchner, H.; Ringeissen, C., Combining symbolic constraint solvers on algebraic domains, J. Symb. Comput., 18, 2, 113-155 (1994) · Zbl 0819.68111
[39] Kirchner, K.; Kirchner, H.; Rusinowitch, M., Deduction with symbolic constraints, Rev. Intell. Artif., 4, 3, 9-52 (1990)
[40] 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, Lect. Notes Comput. Sci., vol. 8152 (2013), Springer), 343-358 · Zbl 1398.68276
[41] Kop, C.; Nishida, N., Automatic constrained rewriting induction towards verifying procedural programs, (12th Asian Symposium on Programming Languages and Systems. 12th Asian Symposium on Programming Languages and Systems, Lect. Notes Comput. Sci., vol. 8858 (2014), Springer), 334-353 · Zbl 1453.68050
[42] Lal, A.; Qadeer, S.; Lahiri, S., Corral: A Solver for Reachability Modulo Theories (January 2012), Microsoft Research, Technical Report MSR-TR-2012-9
[43] Larsen, K. G.; Pettersson, P.; Yi, W., UPPAAL in a nutshell, Int. J. Softw. Tools Technol. Transf., 1, 1-2, 134-152 (1997) · Zbl 1060.68577
[44] Lucanu, D.; Serbanuta, T.-F.; Rosu, G., K framework distilled, (9th International Workshop on Rewriting Logic and Its Applications. 9th International Workshop on Rewriting Logic and Its Applications, Lect. Notes Comput. Sci., vol. 7571 (2012), Springer), 31-53
[45] Lucas, S.; Meseguer, J., Operational termination of membership equational programs: the order-sorted way, Electron. Notes Theor. Comput. Sci., 238, 3, 207-225 (2009) · Zbl 1347.68198
[46] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci., 96, 1, 73-155 (1992) · Zbl 0758.68043
[47] Meseguer, J., Membership algebra as a logical framework for equational specification, (12th International Workshop on Recent Trends in Algebraic Development Techniques. 12th International Workshop on Recent Trends in Algebraic Development Techniques, Lect. Notes Comput. Sci., vol. 1376 (1997), Springer), 18-61 · Zbl 0903.08009
[48] 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) · Zbl 1115.68079
[49] 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, Lect. Notes Comput. Sci., vol. 6617 (2011), Springer), 282-297
[50] Nelson, G.; Oppen, D. C., Simplification by cooperating decision procedures, ACM Trans. Program. Lang. Syst., 1, 2, 245-257 (1979) · Zbl 0452.68013
[51] Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL \((T)\), J. ACM, 53, 6, 937-977 (2006) · Zbl 1326.68164
[52] Ölveczky, P. C.; Caccamo, M., Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude, (Baresi, L.; Heckel, R., 9th International Conference on Fundamental Approaches to Software Engineering. 9th International Conference on Fundamental Approaches to Software Engineering, Lect. Notes Comput. Sci., vol. 3922 (2006), Springer), 357-372
[53] Owre, S.; Rushby, J.; Shankar, N., PVS: a prototype verification system, (11th International Conference on Automated Deduction. 11th International Conference on Automated Deduction, Lect. Notes Artif. Intell., vol. 607 (June 1992), Springer-Verlag: Springer-Verlag Saratoga, NY), 748-752
[54] Podelski, A., Model checking as constraint solving, (7th International Symposium on Static Analysis. 7th International Symposium on Static Analysis, Lect. Notes Comput. Sci., vol. 1824 (2000), Springer), 22-37 · Zbl 0966.68121
[55] Rocha, C., Symbolic Reachability Analysis for Rewrite Theories (2012), University of Illinois at Urbana-Champaign, PhD thesis
[56] Rocha, C.; Cadavid, H.; Muñoz, C. A.; Siminiceanu, R., A formal interactive verification environment for the Plan Execution Interchange Language, (9th International Conference on Integrated Formal Methods. 9th International Conference on Integrated Formal Methods, Lect. Notes Comput. Sci., vol. 7321 (2012), Springer), 343-357
[57] Rocha, C.; Meseguer, J.; Muñoz, C., Rewriting Modulo SMT (August 2013), NASA Langley Research Center: NASA Langley Research Center Hampton, VA, Technical Memorandum NASA/TM-2013-218033
[58] Rocha, C.; Meseguer, J.; Muñoz, C., Rewriting modulo SMT and open system analysis, (10th International Workshop on Rewriting Logic and Its Applications. 10th International Workshop on Rewriting Logic and Its Applications, Lect. Notes Comput. Sci., vol. 8663 (2014), Springer International Publishing), 247-262 · Zbl 1367.68151
[59] Roşu, G.; Ştefănescu, A., Matching logic: a new program verification approach, (33rd International Conference on Software Engineering (2011), ACM: ACM New York, NY, USA), 868-871
[60] Rybina, T.; Voronkov, A., A logical reconstruction of reachability, (5th International Andrei Ershov Memorial Conference on Perspectives of Systems Informatics. 5th International Andrei Ershov Memorial Conference on Perspectives of Systems Informatics, Lect. Notes Comput. Sci., vol. 2890 (2003), Springer), 222-237 · Zbl 1254.68153
[61] Sakata, T.; Nishida, N.; Sakabe, T., On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs, (20th International Workshop on Functional and Constraint Logic Programming. 20th International Workshop on Functional and Constraint Logic Programming, Lect. Notes Comput. Sci., vol. 6816 (2011), Springer), 138-155 · Zbl 1339.68141
[62] Thati, P.; Meseguer, J., Complete symbolic reachability analysis using back-and-forth narrowing, Theor. Comput. Sci., 366, 1-2, 163-179 (2006) · Zbl 1110.68058
[63] 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
[64] Vidal, G., Closed symbolic execution for verifying program termination, (IEEE 12th International Working Conference on Source Code Analysis and Manipulation (Sept 2012)), 34-43
[65] Vidal, G., Symbolic execution as a basis for termination analysis, Sci. Comput. Program., 102, 142-157 (2015)
[66] Viry, P., Equational rules for rewriting logic, Theor. Comput. Sci., 285, 487-517 (2002) · Zbl 1001.68058
[67] 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
[68] Yovine, S., KRONOS: a verification tool for real-time systems, Int. J. Softw. Tools Technol. Transf., 1, 1, 123-133 (1997) · Zbl 1060.68606
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.