Proofs of soundness of type systems are typically based on small-step operational semantics, because of the inability of big-step operational semantics to distinguish stuck from non-terminating computations.
In this talk I will present two techniques to prove type soundness with big-step semantics.
The former is based on the notion of coinductive big-step semantics, obtained by interpreting the semantics rules coinductively, and by considering non-well-founded values. The corresponding proof of soundness is rather involved, since it requires showing that the set of proof trees defining the semantic judgment forms a complete metric space when equipped with a specific distance function.
A simpler approach consists in approximating at arbitrary depth the possibly infinite derivations of the coinductive semantics with infinite sequences of finite derivations; in this way, type soundness can be proved by standard mathematical induction.
Finally, I will briefly discuss interesting research directions to overcome some of the limitations of the presented techniques.
Slides
Many of the modern program verifiers are based on the predicate abstraction with CEGAR method, The method looks for a sufficient inductive invariant to prove the given property of the given program by iteratively accumulating predicates that are obtained by analyzing spurious counterexamples, and predicate refinement heuristics like Craig interpolation are used for this purpose. In this talk, we overview our recent work on predicate refinement heuristics in CEGAR. Specifically, we show that a certain strategy for choosing predicates can guarantee the convergence of CEGAR at a modest cost. We also show that choosing small refinements guarantees fast convergence under certain conditions.
Slides
Finite state machines are a great specification formalism: they are intuitive and simple to understand, and can be used to describe all sorts of systems, or properties of systems, that we want to verify.
Coming up with accurate state machine models can be a lot of work. However, state machine inference provides a great technique to automatically reverse-engineer application using just black-box testing.? This can provide formal models of existing code for free, as a useful first step to rigorous specification and then verification of this code. We will show this using case studies of bank cards, internet banking tokens, and TLS implementations.
Slides
This talk aims to characterize modular reasoning for object-oriented (OO) programs that use subtyping and dynamic dispatch. It gives a semantic characterization of supertype abstraction using two different semantics for a Java-like OO language. The first semantics is an accurate semantics of the language’s behavior. The second semantics mimics supertype abstraction, using static type information and method specifications to determine what a program should do. The validity of supertype abstraction is defined as having this second semantics accurately predict the behavior of programs with the dynamic semantics.
This talk is based on joint work with David A. Naumann of Stevens Institute of Technology, and is based on our paper “Behavioral Subtyping, Specification Inheritance, and Modular Reasoning” published in ACM TOPLAS, 37(4):13:1-13:88, Aug. 2015. (See http://doi.acm.org/10.1145/2766446.) The work of Gary Leavens was supported by NSF grants CNS-0808913, CCF-0916350, CCF-0916715, CCF-1017262, and CNS-1228695 David Naumann’s work was supported in part by NSF grants CCF-0915611 and CNS-1228930.
Slides
