Abstract Development of formal proofs of correctness of programs can increase actual and
perceived reliability and facilitate better understanding of program specifications and their …

Formally verified correctness is one of the most desirable properties of software systems. But
despite great progress made via interactive theorem provers, such as Coq, writing proof …

Formally verifying software correctness is a highly manual process. However, because
verification proof scripts often share structure, it is possible to learn from existing proof scripts …

We implement an automated tactical prover TacticToe on top of the HOL4 interactive
theorem prover. TacticToe learns from human proofs which mathematical technique is …

The days of verifying only toy programs are long gone. The last two decades have marked a
new era of verification at scale, bringing strong guarantees to large and critical systems—an …

We report on our efforts building a new, large proof-repair dataset and benchmark suite for
the Coq proof assistant. The dataset is made up of Git commits from open-source projects …

We describe a new approach to automatically repairing broken proofs in the Coq proof
assistant in response to changes in types. Our approach combines a configurable proof term …

The cost of maintaining formally specified and verified software is widely considered
prohibitively high due to the need to constantly keep code and the proofs of its correctness in …

Proof engineering tools make it easier to develop and maintain large systems verified using
interactive theorem provers. Developing useful proof engineering tools hinges on …

It is critical that our hardware behaves as we expect it to. Hardware verification and testing is
extensive and involves a variety of techniques, including functional tests, quality control …