scientific article; zbMATH DE number 7649971
From MaRDI portal
Publication:5875431
Cites work
- A verified compiler from Isabelle/HOL to CakeML
- Applying data refinement for monadic programs to Hopcroft's algorithm
- Automatic Data Refinement
- Chain-complete posets and directed sets with applications
- Concrete semantics. With Isabelle/HOL
- Data refinement in Isabelle/HOL
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Efficient certified RAT verification
- Efficient verified (UN)SAT certificate checking
- Efficient, verified checking of propositional proofs
- Eisbach: a proof method language for Isabelle
- Extending Sledgehammer with SMT solvers
- Fast Pattern Matching in Strings
- Formal verification of an executable LTL model checker with partial order reduction
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Formalizing the Edmonds-Karp algorithm
- Formalizing the LLVM intermediate representation for verified program transformations
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
- Imperative Functional Programming with Isabelle/HOL
- Isabelle/HOL. A proof assistant for higher-order logic
- Java and the Java memory model -- a unified, machine-checked formalisation
- Mechanised Separation Algebra
- Mechanized semantics for the clight subset of the C language
- Program logics for certified compilers
- Proof-producing translation of higher-order logic into pure and stateful ML
- Refinement to Imperative/HOL
- Verified model checking of timed automata
- VST-Floyd: a separation logic tool to verify correctness of C programs
Cited in
(16)- A formally verified, optimized monitor for metric first-order dynamic logic
- A verified compiler from Isabelle/HOL to CakeML
- Cogent: uniqueness types and certifying compilation
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
- scientific article; zbMATH DE number 7649969 (Why is no real title available?)
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
- A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL
- A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
- Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
- Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
- Verified path indexing
- Formally verified suffix array construction
- Fast and verified UNSAT certificate checking
- Efficient computation of stationary measures and the Lyapunov landscape for families of random dynamical systems with smooth additive noise
- Verifying an efficient algorithm for computing Bernoulli numbers
- van Emde Boas Trees
Describes a project that uses
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875431)
