ABSTRACT. DRAT proofs have become the standard for verifying unsatisfiability proofs emitted by state-of-the-art SAT solvers. However, recent work showed that the specification of the format differs from the implementation in existing tools due to optimizations that are considered necessary for efficiency. Although such differences do not compromise soundness of DRAT checkers, the sets of correct proofs according to the specification and to the implementation are incomparable.

In this paper we discuss how it is possible to check DRAT proofs faithfully according to the specification by careful modification of the standard optimization techniques. These algorithms are implemented in a tool that performs comparably to the same tool without modifications, showing that efficient verification of the DRAT specification is possible. A practical evaluation shows that the differences between specification and implementation of DRAT often arise in practice.

ABSTRACT. Cloud computing provides on-demand access to IT resources via the Internet. Permissions for these resources are defined by expressive access control policies. This industrial experience report discusses the development of a tool called Zelkova, which is used by Amazon Web Services (AWS) for analyzing access control policies. Zelkova encodes the semantics of policies into SMT, compares behaviors, and verifies properties. It provides users a sound mechanism to detect misconfigurations of their policies. Zelkova solves a PSPACE-complete problem and is invoked millions of times daily.

ABSTRACT. Being able to soundly estimate roundoff errors in finite-precision computations is important for many applications in embedded systems and scientific computing. Due to the unintuitive nature of finite-precision arithmetic, automated static analysis tools are highly valuable for this task. The results, however, are only as correct as the implementations of the static analysis tools. This paper presents a formally verified and modular tool which fully automatically checks the correctness of finite-precision roundoff error bounds encoded in a certificate. We present implementations of certificate generation and checking for both Coq and HOL4 and evaluate it on a number of examples from the literature. The experiments use both in-logic evaluation of Coq and HOL4, and execution of extracted code outside of the logics: we benchmark Coq extracted unverified OCaml code and a CakeML-generated verified binary.

ABSTRACT. In the context of formal verification, certifying proofs are proofs of the correctness of a model in a deduction system produced automatically as outcome of the verification. They are quite appealing for high-assurance systems because they can be verified independently by proof checkers, which are usually simpler to certify than the proof-generating tools.

Model checking is one of the most prominent approaches to formal verification of temporal properties and is based on an algorithmical search of the system state space. Although modern algorithms integrate deductive methods, the generation of proofs is typically restricted to invariant properties only.

In this paper, we solve this issue in the context of Linear-time Temporal Logic. By exploiting the k-liveness algorithm, we show how to extend proof generation capabilities for invariant checking to cover full LTL properties, in a simple and efficient manner, with essentially no overhead for the model checker. We implemented the technique on top of an IC3 engine, and show the feasibility of the approach on a variety of benchmarks.