Department of Computer Science
University of Innsbruck
Home Research Teaching Members Events News Jobs
Research
publications projects software

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:

The project deals with the following five tasks:

  1. Constrained Rewriting
  2. SMT (Satisfiability Modulo Theories)
  3. Completion
  4. Complexity
  5. 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

The Innsbruck team consists of

The Vienna team consists of

Meetings

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.