SMT-Based Array Invariant Generation
No abstract available.
Related papers
- Quantified Invariants via Syntax-Guided Synthesis CAV 2019
- Generalized Arrays for Stainless Frames VMCAI 2022
- Bridging Arrays and ADTs in Recursive Proofs TACAS 2021
- Spatial Interpolants ESOP 2015
- Type-based data structure verification PLDI 2009
- Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays TACAS 2009
- SAFARI: SMT-Based Abstraction for Arrays with Interpolants CAV 2012
- Statically Inferring Complex Heap, Array, and Numeric Invariants SAS 2010