Q5875431
type: Item
instance of: scholarly article
author: Peter Lammich
publication date: 2023-02-03T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 7649971
zbMATH Keywords: Isabelle/HOL
zbMATH Keywords: LLVM
zbMATH Keywords: separation logic
zbMATH Keywords: verification condition generator
zbMATH Keywords: code generation
describes a project that uses: GRAT
describes a project that uses: Edmonds-Karp
describes a project that uses: Autoref
describes a project that uses: Eisbach
describes a project that uses: Vellvm
describes a project that uses: DRAT-trim
describes a project that uses: Toolchain
describes a project that uses: VST-Floyd
describes a project that uses: Archive Formal Proofs
describes a project that uses: Isabelle/HOL
describes a project that uses: libclang
describes a project that uses: GitHub
MaRDI profile type: MaRDI publication profile
cites work: Program logics for certified compilers
cites work: Extending Sledgehammer with SMT solvers
cites work: Mechanized semantics for the clight subset of the C language
cites work: Formal verification of an executable LTL model checker with partial order reduction
cites work: Imperative Functional Programming with Isabelle/HOL
cites work: VST-Floyd: a separation logic tool to verify correctness of C programs
cites work: Efficient certified RAT verification
cites work: Data refinement in Isabelle/HOL
cites work: Efficient, verified checking of propositional proofs
cites work: A verified compiler from Isabelle/HOL to CakeML
cites work: Mechanised Separation Algebra
cites work: Fast Pattern Matching in Strings
cites work: Automatic Data Refinement
cites work: Refinement to Imperative/HOL
cites work: Efficient verified (UN)SAT certificate checking
cites work: Formalizing the Edmonds-Karp algorithm
cites work: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
cites work: Applying data refinement for monadic programs to Hopcroft's algorithm
cites work: Java and the Java memory model -- a unified, machine-checked formalisation
cites work: Chain-complete posets and directed sets with applications
cites work: Eisbach: a proof method language for Isabelle
cites work: Proof-producing translation of higher-order logic into pure and stateful ML
cites work: Concrete semantics. With Isabelle/HOL
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
cites work: Verified model checking of timed automata
cites work: Formalizing the LLVM intermediate representation for verified program transformations
DOI: 10.4230/LIPICS.ITP.2019.22
description: scientific article; zbMATH DE number 7649971