References

  1. Franz Baader & Tobias Nipkow (1998): Term Rewriting and All That. Cambridge University Press, doi:10.1145/505863.505888.
  2. Adel Bouhoula & Florent Jacquemard (2008): Automated Induction with Constrained Tree Automata. In: Alessandro Armando, Peter Baumgartner & Gilles Dowek: Proceedings of the 4th International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science 5195. Springer, pp. 539–554, doi:10.1007/978-3-540-71070-7_44.
  3. Aaron R. Bradley & Zohar Manna (2007): The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, doi:10.1007/978-3-540-74113-8.
  4. Stephan Falke & Deepak Kapur (2008): Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures. In: Andrei Voronkov: Proceedings of the 19th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 5117. Springer, pp. 94–109, doi:10.1007/978-3-540-70590-1_7.
  5. Stephan Falke & Deepak Kapur (2009): A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs. In: Renate A. Schmidt: Proceedings of the 22nd International Conference on Automated Deduction, Lecture Notes in Computer Science 5663. Springer, pp. 277–293, doi:10.1007/978-3-642-02959-2_22.
  6. Stephan Falke & Deepak Kapur (2012): Rewriting Induction + Linear Arithmetic = Decision Procedure. In: Bernhard Gramlich, Dale Miller & Uli Sattler: Proceedings of the 6th International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science 7364. Springer, pp. 241–255, doi:10.1007/978-3-642-31365-3_20.
  7. Carsten Fuhs, Jürgen Giesl, Martin Plücker, Peter Schneider-Kamp & Stephan Falke (2009): Proving Termination of Integer Term Rewriting. In: Ralf Treinen: Proceedings of the 20th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 5595. Springer, pp. 32–47, doi:10.1007/978-3-642-02348-4_3.
  8. Carsten Fuhs, Cynthia Kop & Naoki Nishida (2017): Verifying Procedural Programs via Constrained Rewriting Induction. ACM Transactions on Computational Logic 18(2), pp. 14:1–14:50, doi:10.1145/3060143.
  9. Yuki Furuichi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari & Toshiki Sakabe (2008): Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Systems. IPSJ Transactions on Programming 1(2), pp. 100–121. In Japanese (a translated summary is available from http://www.trs.css.i.nagoya-u.ac.jp/crisys/).
  10. Gérard Huet & Jean-Marie Hullot (1982): Proof by Induction in Equational Theories with Constructors. Journal of Computer and System Science 25(2), pp. 239–266, doi:10.1016/0022-0000(82)90006-X.
  11. Cynthia Kop & Naoki Nishida (2013): Term Rewriting with Logical Constraints. In: Pascal Fontaine, Christophe Ringeissen & Renate A. Schmidt: Proceedings of the 9th International Symposium on Frontiers of Combining Systems, Lecture Notes in Computer Science 8152. Springer, pp. 343–358, doi:10.1007/978-3-642-40885-4_24.
  12. Cynthia Kop & Naoki Nishida (2014): Automatic Constrained Rewriting Induction towards Verifying Procedural Programs. In: Jacques Garrigue: Proceedings of the 12th Asian Symposium on Programming Languages and Systems, Lecture Notes in Computer Science 8858. Springer, pp. 334–353, doi:10.1007/978-3-319-12736-1_18.
  13. Cynthia Kop & Naoki Nishida (2015): Constrained Term Rewriting tooL. In: Martin Davis, Ansgar Fehnker, Annabelle McIver & Andrei Voronkov: Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science 9450. Springer, pp. 549–557, doi:10.1007/978-3-662-48899-7_38.
  14. David R. Musser (1980): On Proving Inductive Properties of Abstract Data Types. In: Paul W. Abrahams, Richard J. Lipton & Stephen R. Bourne: Proceedings of the 7th ACM Symposium on Principles of Programming Languages, pp. 154–162, doi:10.1145/567446.567461.
  15. Naoki Nishida & Takumi Kataoka (2014): On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants. In: Carsten Fuhs: Proceedings of the 14th International Workshop on Termination, pp. 1–5.
  16. Enno Ohlebusch (2002): Advanced Topics in Term Rewriting. Springer, doi:10.1007/978-1-4757-3661-8.
  17. Uday S. Reddy (1990): Term Rewriting Induction. In: Mark E. Stickel: Proceedings of the 10th International Conference on Automated Deduction, Lecture Notes in Computer Science 449. Springer, pp. 162–177, doi:10.1007/3-540-52885-7_86.
  18. John C. Reynolds (1998): Theories of Programming Languages. Cambridge University Press, doi:10.1017/CBO9780511626364.
  19. Tsubasa Sakata, Naoki Nishida & Toshiki Sakabe (2011): On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs. In: Herbert Kuchen: Proceedings of the 20th International Workshop on Functional and (Constraint) Logic Programming, Lecture Notes in Computer Science 6816. Springer, pp. 138–155, doi:10.1007/978-3-642-22531-4_9.
  20. Tsubasa Sakata, Naoki Nishida, Toshiki Sakabe, Masahiko Sakai & Keiichirou Kusakari (2009): Rewriting Induction for Constrained Term Rewriting Systems. IPSJ Transactions on Programming 2(2), pp. 80–96. In Japanese (a translated summary is available from http://www.trs.css.i.nagoya-u.ac.jp/crisys/).
  21. Germán Vidal (2012): Closed Symbolic Execution for Verifying Program Termination. In: Proceedings of the 12th IEEE International Working Conference on Source Code Analysis and Manipulation. IEEE Computer Society, pp. 34–43, doi:10.1109/SCAM.2012.13.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org