Invited Speakers

Javier Esparza, Technical University München, Germany
Title: Solving Fixed-Point Equations by Derivation Tree Analysis
Abstract: Fixed-point equations over semirings are the mathematical foundation of program analysis, and have many other applications, e.g. in probability theory. These equations can be formally assigned context-free grammars in a natural way: for instance, the equation X = aXX + bX + c, where a, b, c are semiring elements, is assigned the grammar X -> aXX | bX | c with a, b, c as terminals. We show how by examining the derivation trees of this grammar we can obtain interesting algorithms for computing (or at least approximating) the least solution of the equation, when the semiring satisfies certian conditions.
Joint work with Michael Luttenberger.

Philippa Gardner, Imperial College London, UK
Title: Abstract Local Reasoning about Program Modules
Abstract:Local resource reasoning provides modular reasoning about programs, based on the analysis of a program’s use of resource. This style of reasoning was first introduced in Separation Logic, a program logic for reasoning about C-programs: e.g. Microsoft device driver code and Linux. Separation Logic was extended with abstract predicates to provide course-grained reasoning about program modules, and generalised to Context Logic to provide fine-grained reasoning about program modules.
In this talk, I will describe recent work on reasoning about program modules, using the W3C XML update library DOM as the running example. In particular, I will present an axiomatic specification of DOM using Context Logic, and verify DOM implementations by introducing locality-preserving and locality-breaking translations between the abstract DOM specification and the concrete implementations. I will conclude by describing two pieces of on-going work: work on fine-grained reasoning about concurrent modules using concurrent abstract predicates with Dodds, Parkinson and Vafeiadis at Cambridge; and work on local reasoning about Javascript with Maffeis at Imperial.
Joint work with Thomas Dinsdale-Young and Mark Wheelhouse.

Gopal Gupta, University of Texas at Dallas, USA
Title: Infinite Computation, Co-induction and Computational Logic
Abstract: We give an overview of the coinductive logic programming paradigm. We discuss its applications to modeling \omega-automata, model checking, verification, non-monotonic reasoning, developing SAT solvers, etc. We also discuss future research directions.
Joint work with Neda Saeedloei, Brian DeVries, Richard Min, Kyle Marple and Feliks Kluzniak.