On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction
Abstract elided by the publisher.
Related papers
- Abstract Interpretation-Based Static Analysis of Mobile Ambients SAS 2001
- Verifying Global Two-Safety Properties in Neural Networks with Confidence CAV 2024
- Formally proving a compiler transformation safe Haskell 2015
- On polymorphic gradual typing ICFP 2017
- A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code OOPSLA 2024
- Verified heap theorem prover by paramodulation ICFP 2012
- Proving that programs eventually do something good POPL 2007
- Theorems for free for free: parametricity, with and without types ICFP 2017