References

  1. M. Alpuente, S. Escobar & J. Iborra (2009): Termination of Narrowing Revisited. Theoretical Computer Science 410(46), pp. 4608–4625, doi:10.1016/j.tcs.2009.07.037.
  2. M. Alpuente, S. Escobar & J. Iborra (2011): Modular Termination of Basic Narrowing and Equational Unification. Logic Journal of the IGPL 19(6), pp. 731–762, doi:10.1007/978-3-540-70590-1_1.
  3. F. Baader & W. Snyder (2001): Unification Theory. In: J. A. Robinson & A. Voronkov: Handbook of Automated Reasoning I. Elsevier Science, pp. 447–533, doi:10.1016/B978-044450813-3/50010-2.
  4. K. Bae, S. Escobar & J. Meseguer (2013): Abstract Logical Model Checking of Infinite-State Systems Using Narrowing. In: Proc. of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), LIPIcs 21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 81–96, doi:10.4230/LIPIcs.RTA.2013.81.
  5. C. Bouchard, K. A. Gero, C. Lynch & P. Narendran (2013): On Forward Closure and the Finite Variant Property. In: Proc. of the 9th International Symposium on Frontiers of Combining Systems (FroCos 2013), Lecture Notes in Computer Science 8152. Springer, pp. 327–342, doi:10.1007/978-3-642-40885-4_23.
  6. A. Cholewa, J. Meseguer & S. Escobar (2014): Variants of Variants and the Finite Variant Property. Technical Report. University of Illinois at Urbana-Champaign. Available at http://hdl.handle.net/2142/47117.
  7. M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln, N. Martí-Oliet, J. Meseguer & C. Talcott (2016): Maude Manual (Version 2.7.1). Technical Report. SRI International Computer Science Laboratory. Available at: http://maude.cs.uiuc.edu/maude2-manual/.
  8. M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer & C. Talcott (2007): All About Maude: A High-Performance Logical Framework. Springer, doi:10.1007/978-3-540-71999-1.
  9. H. Comon-Lundh & S. Delaune (2005): The Finite Variant Property: How to Get Rid of Some Algebraic Properties. In: Proc. of the 16th International Conference on Rewriting Techniques and Applications (RTA 2005), Lecture Notes in Computer Science 3467. Springer, pp. 294–307, doi:10.1007/978-3-540-32033-3_22.
  10. J. Dreier, C. Duménil, S. Kremer & R. Sasse (2017): Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols. In: Proc. of the 6th International Symposium on Principles of Security and Trust (POST 2017), Lecture Notes in Computer Science 10204. Springer, pp. 117–140, doi:10.1007/978-3-662-54455-6_6.
  11. J. Dreier, L. Hirschi, S. Radomirovic & R. Sasse (2018): Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR. In: Proc. of the 31st International Symposium on Computer Security Foundations (CSF 2015). IEEE Computer Society Press, pp. 359–373, doi:10.1109/CSF.2018.00033.
  12. F. Durán, S. Eker, S. Escobar, N. Martí-Oliet, J. Meseguer & C. Talcott (2018): Associative Unification and Symbolic Reasoning Modulo Associativity in Maude. In: Proc. of the 12th International Workshop on Rewriting Logic and its Applications (WRLA 2018), Lecture Notes in Computer Science 11152. Springer, pp. 98–114, doi:10.1016/j.scico.2014.02.005.
  13. F. Durán, S. Lucas & J. Meseguer (2009): Termination Modulo Combinations of Equational Theories. In: Proc. of the 7th International Symposium on Frontiers of Combining Systems (FroCos 2009), Lecture Notes in Computer Science 5749. Springer, pp. 246–262, doi:10.1007/978-3-642-04222-5_15.
  14. F. Durán & J. Meseguer (2012): On the Church-Rosser and Coherence Properties of Conditional Order-sorted Rewrite Theories. The Journal of Logic and Algebraic Programming 81(7–8), pp. 816–850, doi:10.1016/j.jlap.2011.12.004.
  15. A. K. Eeralla, S. Erbatur, A. M. Marshal & C. Ringeissen (2019): Rule-based Unification in Combined Theories and the Finite Variant Property. In: Proc. of the 13th International Conference on Language and Automata Theory and Applications (LATA 2019), Lecture Notes in Computer Science 11417. Springer, pp. 356–367, doi:10.1007/978-3-030-13435-8_26.
  16. S. Erbatur, D. Kapur, A. M. Marshall, P. Narendran & C. Ringeissen (2015): Unification and Matching in Hierarchical Combinations of Syntactic Theories. In: Proc. of the 10th International Symposium on Frontiers of Combining Systems (FroCos 2015), Lecture Notes in Computer Science 9322. Springer, pp. 291–306, doi:10.1007/978-3-319-24246-0_18.
  17. S. Escobar, C. Meadows & J. Meseguer (2009): Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties. In: Foundations of Security Analysis and Design V (FOSAD 2007/2008/2009 Tutorial Lectures), Lecture Notes in Computer Science 5705. Springer, pp. 1–50, doi:10.1007/978-3-642-03829-7_1.
  18. S. Escobar & J. Meseguer (2007): Symbolic Model Checking of Infinite-State Systems Using Narrowing. In: Proc. of the 18th International Conference on Term Rewriting and Applications (RTA 2007), Lecture Notes in Computer Science 4533. Springer, pp. 153–168, doi:10.1007/978-3-540-73449-9_13.
  19. S. Escobar, R. Sasse & J. Meseguer (2012): Folding Variant Narrowing and Optimal Variant Termination. The Journal of Logic and Algebraic Programming 81(7–8), pp. 898–928, doi:10.1016/j.jlap.2012.01.002.
  20. (2019): Full Maude Website. Available at: https://github.com/maude-team/full-maude.
  21. J. M. Hullot (1980): Compilation de Formes Canoniques dans les Théories Equationnelles. Université de Paris-Sud.
  22. J. P. Jouannaud, C. Kirchner & H. Kirchner (1983): Incremental Construction of Unification Algorithms in Equational Theories. In: Proc. of the 17th International Colloquium on Automata, Languages and Programming (ICALP 1990), Lecture Notes in Computer Science 154. Springer, pp. 361–373, doi:10.1007/BFb0036921.
  23. J. P. Jouannaud & H. Kirchner (1986): Completion of a Set of Rules Modulo a Set of Equations. SIAM Journal on Computing 15(4), pp. 1155–1194, doi:10.1137/0215084.
  24. D. Kapur & P. Narendran (1987): Matching, Unification and Complexity. ACM SIGSAM Bulletin 21(4), pp. 6–9, doi:10.1145/36330.36332.
  25. S. Lucas & J. Meseguer (2016): Normal Forms and Normal Theories in Conditional Rewriting. Journal of Logical and Algebraic Methods in Programming 85, pp. 67–97, doi:10.1016/j.jlamp.2015.06.001.
  26. S. Meier, B. Schmidt, C. Cremers & D. A. Basin (2013): The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In: Proc. of the 25th International Conference on Computer Aided Verification (CAV 2013), Lecture Notes in Computer Science 8044. Springer, pp. 696–701, doi:10.1007/978-3-642-39799-8_48.
  27. J. Meseguer (1992): Conditional Rewriting Logic as a United Model of Concurrency. Theoretical Computer Science 96(1), pp. 73–155, doi:10.1016/0304-3975(92)90182-F.
  28. J. Meseguer (1997): Membership Algebra as a Logical Framework for Equational Specification. In: Proc. of the 12th International Workshop on Algebraic Development Techniques (WADT 1997), Lecture Notes in Computer Science 1376. Springer, pp. 18–61, doi:10.1007/3-540-64299-4_26.
  29. J. Meseguer (2012): Twenty Years of Rewriting Logic. The Journal of Logic and Algebraic Programming 81(7-8), pp. 721–781, doi:10.1016/j.jlap.2012.06.003.
  30. J. Meseguer (2017): Strict Coherence of Conditional Rewriting Modulo Axioms. Theoretical Computer Science 672, pp. 1–35, doi:10.1016/j.tcs.2016.12.026.
  31. J. Meseguer (2018): Symbolic Reasoning Methods in Rewriting Logic and Maude. In: Proc. of the 25th International Workshop on Logic, Language, Information, and Computation (WoLLIC 2018), Lecture Notes in Computer Science 10944. Springer, pp. 25–60, doi:10.1007/978-3-662-57669-4_2.
  32. J. Meseguer (2018): Variant-based Satisfiability in Initial Algebras. Science of Computer Programming 154, pp. 3–41, doi:10.1016/j.scico.2017.09.001.
  33. A. Riesco (2014): Using Big-Step and Small-Step Semantics in Maude to Perform Declarative Debugging. In: Proc. of the 12th International Symposium on Functional and Logic Programming (FLOPS 2014), Lecture Notes in Computer Science 8475. Springer, pp. 52–68, doi:10.1007/978-3-319-07151-0_4.
  34. V. Rusu (2010): Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications. In: Proc. of the 4th International Conference on Tests and Proofs (TAP 2010), Lecture Notes in Computer Science 6143. Springer, pp. 135–150, doi:10.1007/978-3-642-13977-2_12.
  35. TeReSe (2003): Term Rewriting Systems. Cambridge University Press, doi:10.1017/S095679680400526X.
  36. E. Tushkanova, A. Giorgetti, C. Ringeissen & O. Kouchnarenko (2015): A Rule-based System for Automatic Decidability and Combinability. Science of Computer Programming 99, pp. 3–23, doi:10.1016/j.scico.2014.02.005.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org