Formal Verification¶

Papers on formal verification from POPL, PLDI, OOPSLA, ECOOP, and ICFP.

2026¶

Formal Verification for JavaScript Regular Expressions — POPL 2026 🏆 Distinguished Paper
Fully mechanized (Coq) semantics for all ECMAScript regex features.
Miri: Practical Undefined Behavior Detection for Rust — POPL 2026
Interpreter-based runtime UB detection with a formalized memory model for Rust.

Correctness Meets Performance: From Agda to Futhark — ICFP 2025
Bridge from Agda proofs to high-performance GPU code via formal correspondence.
Formal Semantics and Program Logics for a Fragment of OCaml — ICFP 2025
Mechanized separation logic for realistic OCaml fragment with higher-order functions.
McTT: A Verified Kernel for a Proof Assistant — ICFP 2025
Verified kernel for a Martin-Löf type theory proof assistant, mechanized in Coq.
SecRef*: Securely Sharing Mutable References — ICFP 2025
F proof rules for secure sharing at verified/unverified code boundaries.*
Verified Compilation of a Dependently Typed Language — PLDI 2025
Mechanized compiler correctness proof for a dependent type theory.
Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language — ICFP 2025
Iris/Coq-verified interpreter for Nix with lazy evaluation and dynamic typing.
Verifying Graph Algorithms in Separation Logic — ICFP 2025
Algebraic approach to verifying graph algorithms in separation logic.