Invited Speakers

Javier Esparza, Technical University München, Germany
Title: Solving FixedPoint Equations by Derivation Tree Analysis
Abstract: Fixedpoint 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 contextfree 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 Cprograms: e.g. Microsoft device driver code and Linux. Separation Logic was extended with abstract predicates to provide coursegrained reasoning about program modules, and generalised to Context Logic to provide finegrained 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 localitypreserving and localitybreaking translations between the abstract DOM specification and the concrete implementations. I will conclude by describing two pieces of ongoing work: work on finegrained 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 DinsdaleYoung and Mark Wheelhouse. 
Gopal Gupta, University of Texas at Dallas, USA
Title: Infinite Computation, Coinduction and Computational Logic
Abstract: We give an overview of the coinductive logic programming paradigm. We discuss its applications to modeling \omegaautomata, model checking, verification, nonmonotonic 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.