Asphalion is an extension of Velisarios, also implemented in Coq, that supports the verification of hybrid fault-tolerant systems, i.e., systems that combine components that can fail arbitrarily and components that can only crash on failure. To reason about such systems, Asphalion provides a sound knowledge sequent calculus that features both non-trusted and trusted knowledge operators. Using Asphalion we have verified one of the main safety property of the MinBFT landmark protocol. This is joint work with Ivana Vukotic and Paulo Verissimo
Velisarios is an extension of EventML, implemented in Coq, that supports the verification of Byzantine fault-tolerant systems, and reasoning about distributed epistemic knowledge. Using Velisarios we have verified the standard agreement safety property of the PBFT landmark protocol. Check out our implementation for details. In the future, we want to support proving properties such as liveness and timeliness, and we want to connect Velisarios with the Verified Software Toolchain (VST) in order to verify the correctness of programs written in C. This is joint work with Ivana Vukotic, Marcus Volp, and Paulo Verissimo
Allen's Partial Equivalence Relation (PER) semantics provides a semantics for Nuprl's type theory that allows one to prove that Nuprl's inference rules are valid, and therefore that Nuprl is consistent. Until our ITP 2014 paper, these proofs were done by hand. In order to formally prove that these rules are correct (and therefore that Nuprl is consistent), we have implemented this PER semantics using the Coq proof assistant. This implementation (1) provides a bridge between Nuprl and Coq, and (2) is the basis for developing certified versions of Nuprl. This is joint work with Abhishek Anand and Mark Bickford.
KeYmaera X is a theorem prover for cyber-physical systems (modeled as hybrid systems) that implements a logic called Differential Dynamic Logic (dL for short). KeYmaera X has a small core thanks a uniform substitution based proof calculus. We have implemented and verified this core in Coq. Check out our implementation for details. This was joint work with Brandon Bohrer and Andre Platzer from CMU, who have implemented and verified KeYmaera's core in Isabelle.
Using our formalization of Nuprl in Coq, we are turning Nuprl into an intuitionistic type theory, i.e., we have proved that some versions of Brouwer's continuity and bar induction principles are valid w.r.t. Nuprl's PER semantics. In order to prove the validity of such continuity principles we have turned Nuprl into a nominal type theory. It remains open whether stronger continuity and bar induction rules are also valid. Moreover, we have also implemented a version of Brouwer's concept of choice sequences on top of Nuprl's underlying digital library of facts and definitions. In addition, the library can now also contain sequences of choices that can be filled over time. We validated standard axioms about choice sequences by turning Nuprl's semantics into a Beth model. This is joint work with Liron Cohen, Mark Bickford, and Robert L. Constable.
EventML is a ML-like constructive specification language that implements a paradigm for verified programming. It gives precedence to the programming task, and also allows programmers to cooperate with a proof assistant in order to structure arguments of correctness. It is designed specifically to cooperate with the Nuprl proof assistant in order to develop correct-by-construction asynchronous protocols. This is joint work with Mark Bickford and Robert L. Constable.
Using EventML, we have specified, synthesized, and verified safety properties of the Multi-Paxos protocol. To do so, we have automated some patterns of reasoning; and to get efficient code, we have built a process optimizer in Nuprl. We are reusing this methodology to develop other provably correct protocols, striving towards more resilient and trustworthy systems. One of our current goal is to verify Byzantine fault tolerant protocols written in C using, among other things, the Verified Software Toolchain (VST). This is joint work with Mark Bickford, Robert L. Constable, Ivana Vukotic, Marcus Volp, and Paulo Verissimo
Programming languages such as SML have sophisticated, flexible and safe type systems. Unfortunately, the type error messages for incorrect programs are confusing. Skalpel implements a promising approach to making type errors easier to understand and fix called type error slicing, in which slices (program points) containing all and only the information needed by the programmer to understand and fix a type error are identified and exhibited. Check out the web page of our project, from which you can download packages for Debian and Red-Hat-based systems as well as a web demo.
Intersection types introduce type polymorphism in a finitary way. Expansion was introduced to recover the principal typing property in such systems. The study of realisability semantics for such systems with expansion might help casting some light on the expansion mechanism.
Reducibility is a method based on realisability semantics where the idea is to interpret types by sets of λ-terms closed under some properties. This method seems promising in generalising diverse properties' proofs of the (typed or untyped) λ-calculus.