Automatic Constrained Rewriting Induction towards Verifying Procedural Programs
No abstract available.
Related papers
- Automated Analysis of Logically Constrained Rewrite Systems using crest TACAS 2025
- Solving constrained Horn clauses modulo algebraic data types and recursive functions POPL 2022
- Parallelizing functional programs by generalization JFP 1999
- Synthesizing software verifiers from proof rules PLDI 2012
- A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems CPP 2021
- Higher-Order LCTRSs and Their Termination ESOP 2024
- Data-Driven Verification of Procedural Programs with Integer Arrays CAV 2025
- The Search for Constrained Random Generators PLDI 2026