A central objective of the verifying compiler grand challenge is to develop a push-button
verifier that generates proofs of correctness in a syntax-driven fashion similar to the way an …

The interfaces between layers of a system are susceptible to bugs if developers of adjacent
layers proceed under subtly different assumptions. Formal verification of two layers against …

We present verification of a bare-metal server built using diverse implementation techniques
and languages against a whole-system input-output specification in terms of machine code …

We present a networked key-value server, implemented in C and formally verified in Coq.
The server interacts with clients using a subset of the HTTP/1.1 protocol and is specified and …

We present an approach for automatically generating provably correct abstractions from C
source code that are useful for practical implementation verification. The abstractions are …

Instruction sets, from families like x86 and ARM, are at the center of many ambitious formal-
methods projects. Many verification, synthesis, programming, and debugging tools rely on …

Developing technology for building verified stacks, ie, computer systems with
comprehensive proofs of correctness, is one way the science of programming languages …

The growing complexity and diversity of models used for engineering dependable systems
implies that a variety of formal methods, across differing abstractions, paradigms, and …

Most verification approaches embed a model of program state into their semantic treatment.
Though a variety of heterogeneous state-space models exists, they all possess common …

We present an automatic proof-producing translator targeting the hardware description
language Verilog. The tool takes a circuit represented as a HOL function as input, translates …