Verifying Array Programs by Transforming Verification Conditions
Abstract elided by the publisher.
Related papers
- Data-Driven Verification of Procedural Programs with Integer Arrays CAV 2025
- Primitive Recursive Program Transformations POPL 1976
- Formally Validating a Practical Verification Condition Generator CAV 2021
- Automatic Verification of Integer Array Programs CAV 2009
- Verified VCG and Verified Compiler for Dafny CPP 2026
- Symbolic conditioning of arrays in probabilistic programs ICFP 2017
- Implementation of an Array Bound Checker POPL 1977
- Property Checking Array Programs Using Loop Shrinking TACAS 2018