Cited in
(28)- Verifying array manipulating programs with full-program induction
- \textsc{Diffy}: inductive reasoning of array programs using difference invariants
- Generic abstraction of dictionaries and arrays
- Verifying Array Programs by Transforming Verification Conditions
- An extension of lazy abstraction with interpolation for programs with arrays
- Datacentric semantics for verification of privacy policy compliance by mobile applications
- Data abstraction: a general framework to handle program verification of data structures
- Apron
- JACK
- julia
- BAP
- ASTREE
- Lingva
- EUREKA
- Julia Static Analyzer
- Booster
- PRECiSA
- Daisy
- Static contract checking with abstract interpretation
- Inferring functional properties of matrix manipulating programs by abstract interpretation
- Lazy abstraction with interpolants for arrays
- Diffy
- Precondition inference from intermittent assertions and application to contracts on collections
- Inferring complete initialization of arrays
- A Galois connection calculus for abstract interpretation
- Lingva: generating and proving program properties using symbol elimination
- Booster: an acceleration-based verification framework for array programs
- An array content static analysis based on non-contiguous partitions
This page was built for software: FunArray
