Certified Programs and Proofs

Modern Satisfiability Modulo Theories (SMT) solvers are fundamental to many program analysis, verification, design and testing tools. They are a good fit for the domain of software and hardware engineering because they support many domains that are commonly used by the tools. The meaning of domains are captured by theories that can be axiomatized or supported by efficient theory solvers. Nevertheless, not all domains are handled by all solvers and many domains and theories will never be native to any solver. We here explore different theories that extend Microsoft Research’s SMT solver Z3’s basic support. Some can be directly encoded or axiomatized, others make use of user theory plug-ins. Plug-ins are a powerful way for tools to supply their custom domains.

Recent developments in the theory of focused proof systems provide flexible means for structuring proofs within the sequent calculus. This structuring is organized around the construction of “macro” level inference rules based on the “micro” inference rules which introduce single logical connectives. After presenting focused proof systems for first-order classical logics (one with and one without fixed points and equality) we illustrate several examples of proof certificates formats that are derived naturally from the structure of such focused proof systems. In principle, a proof certificate contains two parts: the first part describes how macro rules are defined in terms of micro rules and the second part describes a particular proof object using the macro rules. The first part, which is based on the vocabulary of focused proof systems, describes a collection of macro rules that can be used to directly present the structure of proof evidence captured by a particular class of computational logic systems. While such proof certificates can capture a wide variety of proof structures, a proof checker can remain simple since it must only understand the micro-rules and the discipline of focusing. Since proofs and proof certificates are often likely to be large, there must be some flexibility in allowing proof certificates to elide subproofs: as a result, proof checkers will necessarily be required to perform (bounded) proof search in order to reconstruct missing subproofs. Thus, proof checkers will need to do unification and restricted backtracking search.

Lock-free algorithms are extremely hard to be built correct due to their fine-grained concurrency natures. Formal techniques for verifying them are crucial. We present a framework for verification of CAS-based lock-free algorithms, and prove a nontrivial lock-free algorithm Scalable Synchronous Queue that is practically adopted in Java 6. The strength of our approach lies on that it relieves the dependence on auxiliary variables/commands, thus is relatively easier to conduct and comprehend, comparing to existing works.

In this paper, we present a core calculus for the Fortress programming language, which provides both multiple dispatch and multiple inheritance. While previous work proposed a set of static rules to guarantee no ambiguous calls at run time, the rules were parametric to the underlying programming language. To implement such rules for a particular language, the rules should be instantiated for the language. Therefore, to concretely realize the overloading rules for Fortress, we formally define a core calculus for Fortress and mechanize the calculus and its type safety proof in Coq.

The approach is implemented on top of the generic Why platform for deductive verification, which allows us to perform experiments where proofs are discharged by combining several back-end automatic provers.