In modern compilers, many optimizations and analyses, in particular those based on the SSA form, rely on dominance information, so computing dominators efficiently is an important problem. The classic algorithm to compute dominators in a control flow graph is the one designed by Lengauer and Tarjan in 1979. Other efficient algorithms have been proposed since. Previous works formally verified less efficient algorithms, and formally validated parts of the Lengauer-Tarjan algorithm, but there is no complete formal verification or validation of any of the fast algorithms computing dominators so far. In 2016, Georgiadis and Tarjan described a method to tackle these. They defined a certificate with which it becomes easy to validate dominators. Following their method, we successfully implemented and proved correct a validator of dominators in the Rocq Prover, inside the CompCertSSA verified compiler. This is the first complete mechanized certification of a fast algorithm computing dominators.

In this paper we describe the design and implementation of feqb, a tool that synthesizes sound equality tests for inductive data types in the dependent type theory of the Coq system. Our procedure scales to large inductive data types, as in hundreds of constructors, since the terms and proofs it synthesizes are linear in the size of the inductive type. Moreover it supports some forms of dependently typed arguments and sigma types pairing data with proofs of decidable properties. Finally feqb handles deeply nested containers without requiring any human intervention.

Abstract Program slicing can be used to reduce a given initial program to a smaller one (a slice ) that preserves the behavior of the initial program with respect to a chosen criterion. Verification and validation (V&V) of software can become easier on slices, but require particular care in the presence of errors or non-termination in order to avoid unsound results or a poor level of code reduction in slices with respect to the initial program. This article proposes a theoretical foundation for conducting V&V activities on a slice instead of the initial program. We introduce the notion of relaxed slicing that is still capable of producing small slices, even in the presence of errors or non-termination, and establish an appropriate soundness property. It allows us to give a precise interpretation of verification results (absence or presence of errors) obtained for a slice in terms of the initial program. The implementation of these results in the Coq proof assistant is presented and some of its difficult points are discussed.