### Constrained Rewriting and SMT: Emerging Trends in Rewriting

This is a joint project between Austria and Japan. It involves research teams from the following universities:

- Hokkaido University
- Japan Advanced Institute of Science and Technology
- Nagoya University
- University of Innsbruck
- University of Yamanashi
- Vienna University of Technology

The project deals with the following five tasks:

- Constrained Rewriting
- SMT (Satisfiability Modulo Theories)
- Completion
- Complexity
- Certification

The overall aim is to advance applicability of rewriting techniques in verification by focusing on constrained rewriting, a paradigm that suits program analysis better than unconstrained rewriting. Constrained rewriting is a well-studied area but different notions of constrained rewriting exist and only few attempts for automation have been undertaken. Hence a thorough comparison of these approaches is non-trivial. In this project we want to make these approaches comparable, e.g., by a suitable competition of dedicated tools. Nowadays many rewriting tools use so-called SMT solvers as external software to solve (extended) boolean constraints. The second aim of the project is to make (existing) rewriting tools more powerful by extending the underlying SMT solvers with direct support for constrained rewriting. SMT solvers are also essential for some variants and extensions of (Knuth-Bendix) completion which are studied in task 3. The aim of task 4 is to establish upper bounds on the complexity of programs automatically; also here the achievements of tasks 1 and 2 are essential for success. Finally, task 5 addresses to establish soundness of the aforementioned approaches mechanically, i.e., tool (output) is verified automatically with the help of a theorem prover.

#### Members

The project is coordinated by

- Aart Middeldorp (coordinator Austria)
- Masahiko Sakai (coordinator Japan)

The Innsbruck team consists of

- Cynthia Kop
- Aart Middeldorp
- Georg Moser
- Thomas Sternagel
- René Thiemann
- Sarah Winkler
- Harald Zankl

The Vienna team consists of

- Karl Gmeiner
- Bernhard Gramlich

#### Meetings

- kickoff meeting, July 2 – 6, 2012, Gamagori, Japan
- 39th TRS meeting, September 18 – 20, 2013, Akita, Japan
- 41st TRS meeting, September 26 – 28, 2014, Sapporo, Japan

#### FWF “International Cooperation Project” project number

I 963-N15#### Contact

aart middeldorp at uibk dot ac dot at#### Publications

Verifying Procedural Programs via Constrained Rewriting Induction

Carsten Fuhs, Cynthia Kop, Naoki Nishida

ACM Transactions on Computational Logic 18(2),
pp. 14:1 – 14:50,
2017.

Complexity of Conditional Term Rewriting

Cynthia Kop, Aart Middeldorp, Thomas Sternagel

Logical Methods in Computer Science 13(1:6),
pp. 1 – 56,
2017.

AC-KBO Revisited

Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp

Theory and Practice of Logic Programming 16(2),
pp. 163 – 188,
2016.

Constrained Term Rewriting tooL

Cynthia Kop and Naoki Nishida

Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20),
Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 9450,
pp. 549 – 557,
2015.

Formalizing Soundness and Completeness of Unravelings

Sarah Winkler and René Thiemann

Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS 2015),
Lecture Notes in Artificial Intelligence 9322,
pp. 239 – 255,
2015.

CoCo Participant: CeTA 2.21

Julian Nagele, Christian Sternagel, Thomas Sternagel, René Thiemann, Sarah Winkler, and Harald Zankl

Proceedings of the 4th International Workshop on Confluence (IWC 2015),
pp. 41,
2015.

Operational Confluence of Conditional Term Rewrite Systems

Karl Gmeiner

Proceedings of the 4th International Workshop on Confluence (IWC 2015),
pp. 18 – 22,
2015.

CoCo Participant: ConCon

Thomas Sternagel and Aart Middeldorp

Proceedings of the 4th International Workshop on Confluence (IWC 2015),
pp. 44,
2015.

Infeasible Conditional Critical Pairs

Thomas Sternagel and Aart Middeldorp

Proceedings of the 4th International Workshop on Confluence (IWC 2015),
pp. 13 – 17,
2015.

Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion

Haruhiko Sato and Sarah Winkler

Proceedings of the 25th International Conference on Automated Deduction (CADE-25),
Lecture Notes in Artificial Intelligence 9195,
pp. 152 – 162,
2015.

Conditional Complexity

Cynthia Kop, Aart Middeldorp, and Thomas Sternagel

Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015),
Leibniz International Proceedings in Informatics 36,
pp. 223 – 240,
2015.

Recording Completion for Certificates in Equational Reasoning

Thomas Sternagel, Sarah Winkler, and Harald Zankl

Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015),
pp. 41 – 47,
2015.

Automatic Constrained Rewriting Induction towards Verifying Procedural Programs

Cynthia Kop and Naoki Nishida

Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014),
Lecture Notes in Computer Science 8858,
pp. 334 – 353,
2014.

Certification of Nontermination Proofs using Strategies and Nonlooping Derivations

Julian Nagele, René Thiemann, and Sarah Winkler

Proceedings of the 6th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2014),
Lecture Notes in Computer Science 8471,
pp. 216 – 232,
2014.

A Satisfiability Encoding of Dependency Pair Techniques for Maximal Completion

Haruhiko Sato and Sarah Winkler

Proceedings of the 14th International Workshop on Termination (WST 2014),
pp. 80 – 84,
2014.

A New and Formalized Proof of Abstract Completion

Nao Hirokawa, Aart Middeldorp, and Christian Sternagel

Proceedings of the 5th International Conference on Interactive Theorem Proving (ITP 2014),
Lecture Notes in Computer Science 8558,
pp. 292 – 307,
2014.

Conditional Confluence (System Description)

Thomas Sternagel and Aart Middeldorp

Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014),
Lecture Notes in Computer Science 8560,
pp. 456 – 465,
2014.

Automated Complexity Analysis Based on Context-Sensitive Rewriting

Nao Hirokawa and Georg Moser

Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014),
Lecture Notes in Computer Science 8560,
pp. 257 – 271,
2014.

First-Order Formative Rules

Carsten Fuhs and Cynthia Kop

Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014),
Lecture Notes in Computer Science 8560,
pp. 240 – 256,
2014.

On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings

Naoki Nishida, Makashi Yanagisawa, and Karl Gmeiner

Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014),
OpenAccess Series in Informatics (OASIcs) 40,
pp. 39 – 50,
2014.

Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems

Karl Gmeiner and Naoki Nishida

Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014),
OpenAccess Series in Informatics (OASIcs) 40,
pp. 3 – 14,
2014.

On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation

Naoki Nishida, Makashi Yanagisawa, and Karl Gmeiner

Proceedings of the 3rd International Workshop on Confluence (IWC 2014),
pp. 24 – 28,
2014.

Normalization Equivalence of Rewrite Systems

Nao Hirokawa, Aart Middeldorp, and Christian Sternagel

Proceedings of the 3rd International Workshop on Confluence (IWC 2014),
pp. 14 – 18,
2014.

The Higher-Order Dependency Pair Framework

Cynthia Kop

Proceedings of the 7th International Workshop on Higher-Order Rewriting (HOR 2014),
2014.

AC-KBO Revisited

Akihisa Yamada, Sarah Winkler, Nao Hirokawa, and Aart Middeldorp

Proceedings of the 12th International Symposium on Functional and Logic Programming (FLOPS 2014),
Lecture Notes in Computer Science 8475,
pp. 319 – 335,
2014.

Size Complexity of BDD Construction of Pseudo-Boolean Constraints in Binary/Mixed-Radix Base Form

Naoki Nagatsuka, Masahiko Sakai, Harald Zankl, and Keiichirou Kusakari

Proceedings of the 28th Annual Conference of the Japan Society of Artificial Intelligence (JSAI 2014),
ID4-OS-11a-3,
2014.

Transformational Approaches for Conditional Term Rewrite Systems

Karl Gmeiner

PhD thesis, Vienna PhD School of Informatics, 2014.

Term Rewriting with Logical Constraints

Cynthia Kop and Naoki Nishida

Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013),
Lecture Notes in Artificial Intelligence 8152,
pp. 343 – 358,
2013.

Termination of LCTRSs

Cynthia Kop

Proceedings of the 13th International Workshop on Termination (WST 2013),
pp. 59 – 63,
2013.

Normalized Completion Revisited

Sarah Winkler and Aart Middeldorp

Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013),
Leibniz International Proceedings in Informatics 21,
pp. 319 – 334,
2013.

Proving Confluence of Conditional Term Rewriting Systems via Unravelings

Karl Gmeiner, Naoki Nishida, and Bernhard Gramlich

Proceedings of the 2nd International Workshop on Confluence (IWC 2013),
pp. 35 – 39,
2013.

KBCV 2.0 – Automatic Completion Experiments

Thomas Sternagel

Proceedings of the 2nd International Workshop on Confluence (IWC 2013),
pp. 53 – 57,
2013.

Termination Tools in Automated Reasoning

Sarah Winkler

PhD thesis, University of Innsbruck, 2013.