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.
Psym: Efficient Symbolic Exploration of Distributed Systems
Explore efficient symbolic methods for verifying distributed systems using Psym, a tool that avoids redundant states, interleavings, and computations during exploration.
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.
An Algebraic Language for Specifying Quantum Networks
Explore BellKAT, a novel specification language for quantum networks based on Kleene algebra, designed to address resource competition and enable formal reasoning about quantum network protocols.
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.
A Verified Compiler for a Functional Tensor Language - PLDI 2024
Explore a verified compiler for functional tensor language, focusing on efficient array code production and formal correctness proof for high-performance domains like image processing and machine learning.
Qubit Recycling Revisited - Optimizing Quantum Circuit Width
Explore qubit recycling optimization for quantum circuits, focusing on complexity, algorithms, and verification using qubit dependency graphs and matrix triangularization techniques.
Hyper Hoare Logic: Proving and Disproving Program Hyperproperties
Explore Hyper Hoare Logic, a generalized proof system for program hyperproperties. Learn to reason about sets of states, proving and disproving properties beyond traditional Hoare logics.
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
Explore a novel proof recipe for linearizability in relaxed memory, using object modification order to simplify event reordering and enable proof reuse in concurrent libraries.
Falcon: A Scalable Analytical Cache Model
Explore a scalable analytical cache model for affine programs, improving performance prediction efficiency and enabling faster optimization decisions in large-scale software development.
Testing Specifications in Dafny - Dafny'24
Explore techniques for testing specifications in Dafny, including automatic mutation testing and Spec-Testing Proofs, to enhance trust in formal verification processes.
Caesar: A Verifier for Probabilistic Programs - Dafny'24
Explore Caesar, a verifier for probabilistic programs, featuring an intermediate verification language and real-valued logic for quantitative property verification in programming.
Generation of Verified Assembly Code Using Dafny and Reinforcement Learning
Explore verified assembly code generation using Dafny and reinforcement learning, combining efficiency with automatic correctness verification for complex programming tasks.
Morello Cerise - Proving Secure Encapsulation - Work in Progress
Explore Morello Cerise's approach to proving secure encapsulation in this work-in-progress presentation on cutting-edge computer security research.
Towards a Language-parametric DSL for Refactoring - Short Paper
Explore a language-parametric DSL approach for refactoring, examining its potential to streamline code improvement across multiple programming languages.
DisLog: A Separation Logic for Disentanglement
Explore DisLog, a novel separation logic for verifying disentanglement in parallel programs. Learn about its applications, benefits, and case studies in concurrent programming.
VST-A: A Foundationally Sound Annotation Verifier for Imperative Programs
Explore VST-A, a foundationally sound annotation verifier combining automation with rich assertion language and formal soundness proofs for imperative program verification.
Logical Foundations - Session Preview
Explore logical foundations in programming languages with Emanuele D'Osualdo's preview of the POPL'24 session, offering insights into cutting-edge research and developments.