Verifying Procedural Programs via Constrained Rewriting Induction
From MaRDI portal
Publication:5278212
DOI10.1145/3060143zbMath1367.68248arXiv1409.0166OpenAlexW2964206513MaRDI QIDQ5278212
Naoki Nishida, Cynthia Kop, Carsten Fuhs
Publication date: 13 July 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1409.0166
program analysisinductive theorem provinglemma generationrewriting inductionconstrained term rewriting
Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)
Related Items
ATLAS: automated amortised complexity analysis of self-adjusting data structures ⋮ Loop detection by logically constrained term rewriting ⋮ Transforming orthogonal inductive definition sets into confluent term rewrite systems ⋮ On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs ⋮ Operationally-based program equivalence proofs using LCTRSs ⋮ Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting ⋮ Unnamed Item ⋮ Type-based analysis of logarithmic amortised complexity ⋮ Runtime complexity analysis of logically constrained rewriting
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Rippling: A heuristic for guiding inductive proofs
- Cost analysis of object-oriented bytecode programs
- Proofs by induction in equational theories with constructors
- Deaccumulation techniques for improving provability
- Inference rules for proving the equivalence of recursive procedures
- Mechanizing structural induction. I: Formal system
- Automated theorem proving by test set induction
- Sound generalizations in mathematical induction
- Preface: Special issue on automatic resource bound analysis
- Automatic Constrained Rewriting Induction towards Verifying Procedural Programs
- Term Rewriting with Logical Constraints
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Secure information flow by self-composition
- Recursive functions of symbolic expressions and their computation by machine, Part I
- Removing redundant arguments automatically
- Solving SAT and SAT Modulo Theories
- Constrained Term Rewriting tooL
- Automated Induction with Constrained Tree Automata
- Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions
- Inference Rules for Proving the Equivalence of Recursive Procedures
- Proving Termination of Integer Term Rewriting
- Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
- Term Rewriting and All That
- Towards Modularly Comparing Programs Using Automated Theorem Provers
- Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures
- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
- On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs
- Termination Analysis of C Programs Using Compiler Intermediate Languages
- Automated Termination Analysis of Java Bytecode by Term Rewriting
- Predicate abstraction and refinement for verifying multi-threaded programs
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- Static Analysis
