Logical and Mathematical Reasoning about Imperative Programs
Abstract
Logical and mathemlicnl reasoning ahout impcrdtive programs.'
Related papers
- Functional formal methods ICFP 2002
- Velvet: A Foundational Multi-modal Verifier for Imperative Programs in Lean CAV 2026
- Weighted programming: a programming paradigm for specifying mathematical models OOPSLA 2022
- A logical analysis of aliasing in imperative higher-order functions JFP 2007
- A logical analysis of aliasing in imperative higher-order functions ICFP 2005
- Software is discrete mathematics ICFP 2003
- High-level separation logic for low-level code POPL 2013
- Modular reasoning about concurrent higher-order imperative programs POPL 2014