Constrained narrowing for conditional equational theories modulo axioms

Abdulla, 2002, Regular tree model checking, vol. 2404, 555 Aguirre, 2014, Conditional narrowing modulo in rewriting logic and maude, vol. 8663, 80 Alur, 1993, Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems, vol. 739, 209 Alur, 1994, A theory of timed automata, Theor. Comput. Sci., 126, 183, 10.1016/0304-3975(94)90010-8 Alur, 2009, Adding nesting structure to words, J. ACM, 56, 10.1145/1516512.1516518 Armando, 2006, Bounded model checking of software using SMT solvers instead of SAT solvers, 146 Baader, 1998 Bachmair, 1994, Associative-commutative superposition, vol. 968, 1 Bae, 2013, Abstract logical model checking of infinite-state systems using narrowing, vol. 21, 81 Bae, 2014, Infinite-state model checking of LTLR formulas using narrowing, vol. 8663, 113 Beyene, 2014, CTL+FO verification as constraint solving, 101 Bockmayr, 1993, Conditional narrowing modulo of set of equations, Appl. Algebra Eng. Commun. Comput., 4, 147, 10.1007/BF01202035 Bouajjani, 2001, Languages, rewriting systems, and verification of infinite-state systems, 24 Bouajjani, 2006, Rewriting models of boolean programs, vol. 4098, 136 Bouajjani, 2000, Regular model checking, 403 Bruni, 2006, Semantic foundations for generalized rewrite theories, Theor. Comput. Sci., 360, 386, 10.1016/j.tcs.2006.04.012 Burel, 2010, Embedding deduction modulo into a prover, vol. 6247, 155 2001, vol. 2002 Comon-Lundth, 2005, The finite variant property: how to get rid of some algebraic properties, vol. 3467, 294 Cordeiro, 2009, SMT-based bounded model checking for embedded ANSI-C software, 137 Dershowitz, 1990, Rewrite systems, 244 Dershowitz, 2001, Rewriting, 535 Dowek, 2003, Theorem proving modulo, J. Autom. Reason., 31, 33, 10.1023/A:1027357912519 Durán, 2008, Proving operational termination of membership equational programs, High.-Order Symb. Comput., 21, 59, 10.1007/s10990-008-9028-2 Durán, 2009, Methods for proving termination of rewriting-based programming languages by transformation, Electron. Notes Theor. Comput. Sci., 248, 93, 10.1016/j.entcs.2009.07.062 Durán, 2009, Termination modulo combinations of equational theories, vol. 5749, 246 Durán, 2012, On the Church–Rosser and coherence properties of conditional order-sorted rewrite theories, J. Log. Algebr. Program., 81, 816, 10.1016/j.jlap.2011.12.004 Erbatur, 2012, Effective symbolic protocol analysis via equational irreducibility conditions, vol. 7459, 73 Erbatur, 2013, Asymmetric unification: a new unification paradigm for cryptographic protocol analysis, vol. 7898, 231 Escobar, 2009, Maude-NPA: cryptographic protocol analysis modulo equational properties, vol. 5705, 1 Escobar, 2007, Symbolic model checking of infinite-state systems using narrowing, vol. 4533, 153 Escobar, 2012, Folding variant narrowing and optimal variant termination, J. Log. Algebr. Program., 81, 898, 10.1016/j.jlap.2012.01.002 Farzan, 2015, Automated program verification, vol. 8977, 25 Gallier, 1989, Complete sets of transformations for general e-unification, Theor. Comput. Sci., 67, 203, 10.1016/0304-3975(89)90004-2 Ganai, 2006, Accelerating high-level bounded model checking, 794 Ganai, 2008, Completeness in SMT-based BMC for software programs, 831 H. Ganzinger, R. Nieuwenhuis, Constraints and theorem proving, in: Comon et al. [18], pp. 159–201. Genet, 2001, Reachability analysis of term rewriting systems with timbuk, 695 Ghilardi, 2010, MCMT: a model checker modulo theories, vol. 6173, 22 Goguen, 1992, Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci., 105, 217, 10.1016/0304-3975(92)90302-V González-Moreno, 1999, An approach to declarative programming based on a rewriting logic, J. Log. Program., 40, 47, 10.1016/S0743-1066(98)10029-8 Hendrix, 2012, Order-sorted equational unification revisited, Electron. Notes Theor. Comput. Sci., 290, 37, 10.1016/j.entcs.2012.11.010 Horbach, 2014, Locality transfer: from constrained axiomatizations to reachability predicates, vol. 8562, 192 Hullot, 1980, Canonical forms and unification, vol. 87, 318 Jouannaud, 1991, Solving equations in abstract algebras: a rule-based survey of unification, 257 Jouannaud, 1983, Incremental construction of unification algorithms in equational theories, vol. 154, 361 Jouannaud, 1986, Completion of a set of rules modulo a set of equations, SIAM J. Comput., 15, 1155, 10.1137/0215084 Kirchner, 2006 Kirchner, 1988, Operational semantics of OBJ3, vol. 317, 287 Kirchner, 1994, Constraint solving by narrowing in combined algebraic domains, 617 Kirchner, 1990, Deduction with symbolic constraints, Rev. Intell. Artif., 4, 9 Lucas, 1998, Context-sensitive computations in functional and functional logic programs, J. Funct. Logic Program., 1, 446 Lucas, 2005, Operational termination of conditional term rewriting systems, Inf. Process. Lett., 95, 446, 10.1016/j.ipl.2005.05.002 Lucas, 2014, Strong and weak operational termination of order-sorted rewrite theories, vol. 8663, 178 Martí-Oliet, 1994, General logics and logical frameworks, 355 Meseguer, 1992, Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci., 96, 73, 10.1016/0304-3975(92)90182-F Meseguer, 1998, Membership algebra as a logical framework for equational specification, vol. 1376, 18 Meseguer, 2012, Twenty years of rewriting logic, J. Log. Algebr. Program., 81, 721, 10.1016/j.jlap.2012.06.003 Meseguer, 2013, Symbolic formal methods: combining the power of rewriting, narrowing, SMT solving and model checking, vol. 8161 Meseguer Meseguer, 2014 Meseguer, 1989, Order-sorted unification, J. Symb. Comput., 8, 383, 10.1016/S0747-7171(89)80036-7 Middeldorp, 1994, Completeness results for basic narrowing, Appl. Algebra Eng. Commun. Comput., 5, 213, 10.1007/BF01190830 Milicevic, 2011, Model checking using SMT and theory of lists, 282 Ohlebusch, 2002 Ohsaki, 2003, Recognizing boolean closed a-tree languages with membership conditional rewriting mechanism, 483 Peterson, 1981, Complete sets of reductions for some equational theories, J. Assoc. Comput. Mach., 28, 233, 10.1145/322248.322251 Robinson, 1969, Paramodulation and theorem proving in first order theories with equality, vol. 4, 133 Rocha, 2008, Theorem Proving Modulo Based on Boolean Equational Procedures, vol. 4988, 337 Rocha, 2014, Rewriting modulo SMT and open system analysis, 247 TeReSe, 2003 Thati, 2007, Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols, High.-Order Symb. Comput., 20, 123 Veanes, 2008, An SMT approach to bounded reachability analysis of model programs, 53 Viry, 1998, Adventures in sequent calculus modulo equations, Electron. Notes Theor. Comput. Sci., 15, 21, 10.1016/S1571-0661(05)82550-2 Walter, 2007, Bounded model checking of analog and mixed-signal circuits using an SMT solver, 66 Walther, 1985, A mechanical solution of Schubert's steamroller by many-sorted resolution, Artif. Intell., 26, 217, 10.1016/0004-3702(85)90029-3