Translating HOL-Light Proofs to Coq
Découvrez la traduction des preuves HOL-Light vers Coq, explorant les défis et solutions pour la vérification formelle entre systèmes logiques différents.
Building Measure Theory Using Hierarchy Builder
Explore the Hierarchy Builder DSL for Coq and its application in constructing measure theory and Lebesgue measure, with insights for potential adaptations to other proof assistants.
From 100 to 1000+ Theorems - Advancements in Mathematical Proof Verification
Explore the journey of formalizing mathematics, from initial proofs to extensive theorem libraries, and discover the challenges and progress in this field.
Univalent Double Categories - Formalization and Applications in Category Theory
Explore univalent double categories in category theory, their formalization in Coq, and applications in mathematics and computer science.
RustBelt: A Quick Dive Into the Abyss - Formalizing Rust's Safety Story
Explore Rust's safety mechanisms, type system, and semantic interpretations. Dive into lifetime logic, sharing predicates, and Coq implementations of Cell operations.
Melocoton - A Program Logic for Verified Interoperability Between OCaml and C
Explore Melocoton, a groundbreaking program logic for verifying interactions between OCaml and C components through OCaml's foreign function interface, featuring a formal semantics and Coq mechanization.
Formally Verifying Optimizations with Block Simulations
Explore formal verification of compiler optimizations using block simulations. Learn about enhancing CompCert with efficient, verified validators for advanced optimizations like LCM and SR.
Modular Verification of Op-Based CRDTs in Separation Logic
Explore modular verification of op-based CRDTs using separation logic. Learn about Reliable Causal Broadcast and OpLib for simplified CRDT implementation and correctness proofs.
Mechanizing Refinement Types
Explore the mechanization of refinement types, combining semantic subtyping and parametric polymorphism. Learn about λRF calculus, data propositions, and metatheory proofs in LiquidHaskell and Coq.
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Explore asynchronous probabilistic couplings in higher-order separation logic, addressing synchronization issues in relational program logics for enhanced reasoning about probabilistic programs.
Using Formal Methods to Eliminate Exploitable Bugs - YOW! 2015
Explore formal methods for creating bug-free software, including SeL4 microkernel and CompCert compiler. Learn about recent advancements and limitations in producing high-assurance software for vehicles.
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives
Explore CryptOpt, a verified compilation pipeline for cryptographic primitives that generates high-performance assembly code with formal proofs, outperforming GCC and Clang for specific applications.
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating Above FF-A
Explore VMSL, a novel separation logic for reasoning about virtual machine communication and security in hypervisor systems, with focus on Arm's FF-A hypercall ABIs.
Putting Weak Memory in Order via a Promising Intermediate Representation
Explore an in-order shared-memory concurrency model for C/C++, supporting non-atomic accesses and compiler optimizations while maintaining soundness between source and intermediate representation.
Specifying Smart Contracts with Hax and ConCert
Explore high-assurance smart contracts using Hax toolchain and ConCert for embedding, specifying security properties, and verification in Rust.
Mostly Automated Proof Repair for Verified Libraries
Explore automated proof repair for higher-order imperative functions, combining dynamic program alignment, enumerative invariant synthesis, and proof-driven testing to maintain verified software efficiently.
Fair Operational Semantics - Theory for Expressing and Reasoning About Fairness Properties
Explore Fair Operational Semantics (FOS), a novel theory for expressing and reasoning about fairness properties in program verification, with applications in concurrent systems and weak memory models.
Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning
Explore Zar: a verified compiler for discrete probabilistic programs, transforming cpGCL to executable samplers. Learn about choice-fix trees, interaction trees, and sampling equidistribution theorem.
Merging Inductive Relations for Improved Program Specification
Explore an algorithm for merging inductive relations, improving automatic generation performance and simplifying mechanized proofs in proof engineering tools like QuickChick for Coq.
CQS: A Formally-Verified Framework for Fair and Abortable Synchronization
Explore a formally-verified framework for fair and abortable synchronization, enabling efficient implementation of various primitives with modular proofs and improved performance.
LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
Explore LiDO, a consensus model enabling safety and liveness verification in Byzantine fault-tolerant protocols through refinement. Learn about mechanized proofs for Jolteon in Coq, advancing blockchain technology.