scientific article; zbMATH DE number 7649971

DOI10.4230/LIPIcs.ITP.2019.22MaRDI QIDQ5875431

Peter Lammich

Publication date: 3 February 2023

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

code generationseparation logicIsabelle/HOLLLVMverification condition generator

Mathematics Subject Classification ID

Related Items (6)

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs ⋮ A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A formally verified, optimized monitor for metric first-order dynamic logic ⋮ Cogent: uniqueness types and certifying compilation

Uses Software

• Isabelle/HOL
• Toolchain
• Autoref
• Eisbach
• Vellvm
• DRAT-trim
• libclang
• GRAT
• GitHub
• VST-Floyd
• Edmonds-Karp
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Eisbach: a proof method language for Isabelle
• Formal verification of an executable LTL model checker with partial order reduction
• Chain-complete posets and directed sets with applications
• Isabelle/HOL. A proof assistant for higher-order logic
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Efficient, verified checking of propositional proofs
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• A verified compiler from Isabelle/HOL to CakeML
• Verified model checking of timed automata
• Extending Sledgehammer with SMT solvers
• Efficient certified RAT verification
• Mechanized semantics for the clight subset of the C language
• Formalizing the Edmonds-Karp Algorithm
• Proof-producing translation of higher-order logic into pure and stateful ML
• Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Mechanised Separation Algebra
• Concrete Semantics
• Formalizing the LLVM intermediate representation for verified program transformations
• Refinement to Imperative/HOL
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Imperative Functional Programming with Isabelle/HOL
• Fast Pattern Matching in Strings
• Automatic Data Refinement
• Data Refinement in Isabelle/HOL
• Program Logics for Certified Compilers
• Efficient verified (UN)SAT certificate checking

This page was built for publication: