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@uibk.ac.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.
Nach oben scrollen