A Formal Proof of Square Root and Division Elimination in Embedded Programs
Abstract elided by the publisher.
354 papers · page 17 of 18
Proving Concurrent Noninterference
Abstract elided by the publisher.
A Formally-Verified Alias Analysis
Abstract elided by the publisher.
Producing Certified Functional Code from Inductive Specifications
Abstract elided by the publisher.
Compositional Verification of a Baby Virtual Memory Manager
Abstract elided by the publisher.
Mechanized Verification of Computing Dominators for Formalizing Compilers
Abstract elided by the publisher.
VeriSmall: Verified Smallfoot Shape Analysis
Abstract elided by the publisher.
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
Abstract elided by the publisher.
Automatically Verifying Typing Constraints for a Data Processing Language
Abstract elided by the publisher.
Modular SMT Proofs for Fast Reflexive Checking Inside Coq
Abstract elided by the publisher.
Engineering Theories with Z3
Abstract elided by the publisher.
Full Reduction at Full Throttle
Abstract elided by the publisher.
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL
Abstract elided by the publisher.
Coquet: A Coq Library for Verifying Hardware
We propose a new library to model and verify hardware circuits in the Coq proof assistant. This library allows one to easily build circuits by following the usual pen-and-paper diagrams. We define a deep-embedding: we use a (dependently typed) data-type that models the architectu…
Tactics for Reasoning Modulo AC in Coq
We present a set of tools for rewriting modulo associativity and commutativity (AC) in Coq, solving a long-standing practical problem. We use two building blocks: first, an extensible reflexive decision procedure for equality modulo AC; second, an OCaml plug-in for pattern matchi…
Mechanizing the Metatheory of mini-XQuery
Abstract elided by the publisher.
A Decision Procedure for Regular Expression Equivalence in Type Theory
Abstract elided by the publisher.
Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience
Abstract elided by the publisher.
Constructive Formalization of Hybrid Logic with Eventualities
Abstract elided by the publisher.
Formalization of Wu's Simple Method in Coq
Abstract elided by the publisher.