---------------------------------------------------------------------- INVITED TALK An Invitation to Tensorial Logic Paul-Andre Mellies (CNRS, Univ. Paris 7) Tensorial logic is a primitive logic which refines linear logic and unifies it with game semantics and linear continuations. The purpose of this introductory talk is to explain the fundamental principles of the logic, as well as the connections to the various polarized variants of linear logic which emerged in the past twenty years. A notion of tensorial proof net will be also discussed, together with extensions of the logic to local stores and other side effects. ----------------------------------------------------------------------
A Proposal for Weak-Memory Local Reasoning Ian Wehrman (University of Texas at Austin) and Josh Berdine (Microsoft Research) Program logics are logics designed to facilitate specification and correctness reasoning for software programs. Most program logics make the strong assumption that all threads agree on the value of shared memory at all times. This assumption can be unsound though for programs with races, like many concurrent data structures. Verification of these difficult programs must take into account the weaker models of memory provided by the architectures on which they execute. In this paper, we describe progress toward a program logic for local reasoning about racy concurrent programs executing on a weak, x86-like memory model. ----------------------------------------------------------------------
INVITED TALK Bedrock: Higher-Order and Automated Proofs about Low-Level Programs Adam Chlipala (Harvard University) In this talk, I'll begin by showing how starting from higher-order logic makes it possible to simplify the definition of Hoare logic (including separation logic). With a simpler system that is much more expressive, what's not to like? The conventional wisdom is that proofs in such a setting are too hard to automate, making verification intractable. The second part of my talk will try to debunk that idea, through presentation of Bedrock, a Coq library that I've been working on. Bedrock makes Coq look like a classical program verifier that operates on structured assembly programs annotated with invariants and simple proof hints. Tactic support automates most reasoning about machine states, using a take on separation logic that is higher-order and computational. Bedrock has been used to lower proof size by multiple orders of magnitude, compared to past work that proved similar theorems in Coq. ----------------------------------------------------------------------
System Level Games: Taking semantics out of context Dan R. Ghica (University of Birmingham) and Nikos Tzevelekos (University of Oxford) We revisit a standard convention in programming language semantics, that the execution context must be defined by the programming language syntax. We argue that it is too restric- tive to model real systems and we discard it, choosing to model the context of execution itself operationally, based on direct knowledge of the whole ambient system. The resulting seman- tics is both operational and modular, and is formulated using techniques adapted from open bisimulation and game semantics. Concretely, we model a low-level programming language similar to C and show both surprising attacks on data privacy and integrity and non-trivial equivalences. We believe a system-level semantics is a first and required step in the promotion of semantic- directed techniques for the verification of realistic systems, especially regarding security prop- erties in a low-level setting. ----------------------------------------------------------------------
The Journey of Biorthogonal Logical Relations to the Realm of Assembly Code Guilhem Jaber (ENS Cachan and Ecole des Mines de Nantes) and Nicolas Tabareau (INRIA) Logical relations appeared to be very fruitful for the devel- opment of modular proofs of compiler correctness. In this field, logical relations are parametrized by a high-level type system, and are even sometimes directly relating low level pieces of code to high-level pro- grams. All those works rely crucially on biorthogonality to get exten- sionality and compositionality properties. But the use of biorthogonality in the definitions also complicates matters when it comes to operational correctness. Most of the time, such correctness results amount to show an unfolding lemma that makes reduction more explicit than in a biorthog- onal definition. Unfortunately, unfolding lemmas are not easy to derive for rich languages and in particular for assembly code. In this paper, we focus on three different situations that enable to reach step-by-step the assembly code universe: the use of Curry-style polymorphism, the pres- ence of syntactical equality in the language and finally an ideal assembly code with a notion of code pointer. ----------------------------------------------------------------------
A Practical Logic Framework for Verifying Safety Properties about Executables Lu Zhao (Univ. of Utah), Guodong Li (Univ. of Utah), John Regehr (Univ. of Utah) We present a novel practical logic framework for automat- ically verifying safety properties about executables. The logic uses a simple construct to handle arbitrary jumps and has a hierarchical structure to enable modular and scalable reasoning. It uses a parameterized instruction semantics making it flexible to verify different safety properties. In addition, it facilitates proof automation; by developing an interprocedural abstract interpretation, we are able to au- tomate the entire process of verifying safety properties. We implemented this framework in the HOL theorem prover and automatically proved safety properties of sandboxed ARM executables. ----------------------------------------------------------------------
Precision and the Conjunction Rule in Concurrent Separation Logic Alexey Gotsman (IMDEA), Josh Berdine (Microsoft Research), Byron Cook (Microsoft Research) Concurrent separation logic is a Hoare logic for modular reasoning about concurrent heap- manipulating programs synchronising via locks. It achieves modular reasoning by partitioning the program state into thread-local and lock-protected parts, and assigning resource invariants to the latter. Surprisingly, the logic is unsound unless resource invariants are precise, i.e., unambigu- ously carve out an area of the heap. The counterexample showing the unsoundness involves the conjunction rule. However, to date it has been an open question whether concurrent separation logic without the conjunction rule is sound when the restriction on resource invariants is dropped: all the published proofs have the precision restriction baked in. In this paper we present a single proof that shows the soundness of the logic with imprecise resource invariants, but without the conjunction rule, as well as its classical version, where resource invariants are required to be precise and the conjunction rule is included. Our proof yields a precise and direct formulation of O'Hearn's Separation Property and provides a semantic analysis of the logic that is much more elementary than previous proofs. ----------------------------------------------------------------------