A verification environment for sequential imperative programs in Isabelle/HOL
From MaRDI portal
Recommendations
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- Program analysis and verification based on Kleene algebra in Isabelle/HOL
- Verifying asymptotic time complexity of imperative programs in Isabelle
- Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL
- Tactic program-based testing and bounded verification in Isabelle/HOL
- A verified decision procedure for orders in Isabelle/HOL
- Compositional verification of sequential programs with procedures
Cited in
(42)- On the correctness of upper layers of automotive systems
- Operating system verification---an overview
- Proving the correctness of client/server software
- Introduction to ``Milestones in interactive theorem proving
- Mechanising a type-safe model of multithreaded Java with a verified compiler
- Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS
- A verified compiler from Isabelle/HOL to CakeML
- A framework for the verification of certifying computations
- Mechanized semantics for the clight subset of the C language
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- WhyMP, a formally verified arbitrary-precision integer library
- A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
- Modeling and verifying graph transformations in proof assistants
- Verified characteristic formulae for CakeML
- Verified software toolchain (invited talk)
- Programmable verifiers in imperative programming
- Types, Maps and Separation Logic
- CSimpl: a rely-guarantee-based framework for verifying concurrent programs
- Imperative Functional Programming with Isabelle/HOL
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Pervasive Theory of Memory
- I/O automata and beyond: Temporal logic and abstraction in Isabelle
- Metatheory of verification calculi in LEGO. To what extent does syntax matter?
- Cogent: uniqueness types and certifying compilation
- Trustworthy Graph Algorithms (Invited Talk)
- A Why3 proof of GMP algorithms
- Small bisimulations for reasoning about higher-order imperative programs
- Sequential, Parallel, and Quantified Updates of First-Order Structures
- Reasoning about CBV functional programs in Isabelle/HOL
- Trace-based verification of imperative programs with I/O
- Reasoning about memory layouts
- Concurrent IMP
- Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
- Formalization of Refinement Calculus for Reactive Systems
- Algebra of Monotonic Boolean Transformers
- Concerned with the unprivileged: user programs in kernel refinement
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
- Proving fairness and implementation correctness of a microkernel scheduler
- Formal verification of C systems code. Structured types, separation logic and theorem proving
- Formal memory models for the verification of low-level operating-system code
- Balancing the load. Leveraging a semantics stack for systems verification
- A mechanical analysis of program verification strategies
This page was built for publication: A verification environment for sequential imperative programs in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5705937)
