Verifying procedural programs via constrained rewriting induction
From MaRDI portal
Abstract: This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend transformation methods based on integer TRSs to handle arbitrary data types, global variables, function calls and arrays, as well as encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can automatically verify memory safety and prove correctness of realistic functions. Our approach proves equivalence between two implementations, so in contrast to other works, we do not require an explicit specification in a separate specification language.
Recommendations
- Automatic constrained rewriting induction towards verifying procedural programs
- Verification of imperative programs by constraint logic program transformation
- Program verification using constraint handling rules and array constraint generalizations
- Verification of procedural programs
- Logic programs as specifications in the inductive verification of logic programs
Cites work
- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
- Automated Induction with Constrained Tree Automata
- Automated termination analysis of Java bytecode by term rewriting
- Automated theorem proving by test set induction
- Automatic constrained rewriting induction towards verifying procedural programs
- Automatic generation of generalization lemmas for proving properties of tail-recursive definitions
- Constrained term rewriting tooL
- Cost analysis of object-oriented bytecode programs
- Deaccumulation techniques for improving provability
- Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
- scientific article; zbMATH DE number 1348478 (Why is no real title available?)
- scientific article; zbMATH DE number 1149426 (Why is no real title available?)
- scientific article; zbMATH DE number 1446599 (Why is no real title available?)
- Inference rules for proving the equivalence of recursive procedures
- Inference rules for proving the equivalence of recursive procedures
- Mechanizing structural induction. I: Formal system
- On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs
- Operational termination of conditional rewriting with built-in numbers and semantic data structures
- Predicate abstraction and refinement for verifying multi-threaded programs
- Preface: Special issue on automatic resource bound analysis
- Proofs by induction in equational theories with constructors
- Proving Termination of Integer Term Rewriting
- Recursive functions of symbolic expressions and their computation by machine, Part I
- Removing redundant arguments automatically
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Rippling: A heuristic for guiding inductive proofs
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- Secure information flow by self-composition
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Sound generalizations in mathematical induction
- Static Analysis
- Term Rewriting and All That
- Term Rewriting with Logical Constraints
- Termination Analysis of C Programs Using Compiler Intermediate Languages
- The automation of proof by mathematical induction
- Towards modularly comparing programs using automated theorem provers
Cited in
(27)- Verifying programs in the calculus of inductive constructions
- Loop detection by logically constrained term rewriting
- Runtime complexity analysis of logically constrained rewriting
- Transforming orthogonal inductive definition sets into confluent term rewrite systems
- On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs
- Automatic constrained rewriting induction towards verifying procedural programs
- Modular verification of procedure equivalence in the presence of memory allocation
- scientific article; zbMATH DE number 3952736 (Why is no real title available?)
- scientific article; zbMATH DE number 4024753 (Why is no real title available?)
- Program verification using constraint handling rules and array constraint generalizations
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- Towards modularly comparing programs using automated theorem provers
- Completion for logically constrained rewriting
- Proceedings of the 9th international workshop on verification and program transformation, VPT, Luxembourg, Luxembourg, March 27--28, 2021
- Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics
- Type-based analysis of logarithmic amortised complexity
- Operationally-based program equivalence proofs using LCTRSs
- Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting
- Confluence Criteria for Logically Constrained Rewrite Systems
- On complexity bounds and confluence of parallel term rewriting
- Transforming concurrent programs with semaphores into logically constrained term rewrite systems
- Difference of constrained patterns in logically constrained term rewrite systems
- Equational theories and validity for logically constrained term rewriting
- Transforming imperative programs into bisimilar logically constrained term rewrite systems via injective functions from configurations to terms
- A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems
- Confluence of logically constrained rewrite systems revisited
- ATLAS: automated amortised complexity analysis of self-adjusting data structures
This page was built for publication: Verifying procedural programs via constrained rewriting induction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5278212)
