The LOng Lunch seminar
This seminar series is intended to foster discussion of research within the group and wider department by encouraging the presentation of work in progress. Where an abstract has been given it is reproduced below in the history of the talks.
2012-11-20: Olivier Serre, "Reflection and Selection for higher-order recursion schemes: some applications to logic and program verification"
In this talk I will introduce the concepts of reflection (aka global model-checking) and selection (aka strategy synthesis) for infinite trees. I will explain why these two problems are decidable when considering infinite trees generated by higher-order recursion schemes.
I will then present several consequences of those results:
- decidability of mu-calculus with back modalities against transition graphs of collapsible pushdown automata
- possibility to avoid divergent computations in recursion schemes
- definability of choice functions for trees generated by recursion schemes
2012-11-15: Anthony Lin, "Verifying programs with counters"
It is well-known that Minsky's counter machines are Turing-complete and so static analysis problems for this model are generally undecidable. Many decidable subclasses of counter machines are known, e.g., vector addition systems with states, lossy counter machines. In this talk, we are going to look at one decidable restriction introduced by O. Ibarra in 1979 wherein only executions of the counter machines with a fixed r (r is a given natural number) number of reversals between non-incrementing and non-decrementing modes for each counter are considered. In this way, we can talk about reversal-bounded version of each static analysis problem (e.g. reversal-bounded reachability). In fact, we extend this model with an unbounded pushdown stack so as to capture function calls. The main result that I plan to talk about is that reversal-bounded reachability for counter machines with a pushdown stack can be efficiently reduced to satisfiability over quantifier-free Presburger formulas, which can be handled by highly-optimized SMT solvers like Microsoft Z3. We have implemented a prototype of the reduction and used it for detecting some interesting memory leakage bugs in Linux device drivers. This is a joint work with Matthew Hague that was published in CAV'11 and CAV'12.
2012-10-23: Martin Lester, "Information Flow Analysis for a Dynamically Typed Functional Language with Staged Metaprogramming"
2012-10-23: Sebastian Maneth, "Hierarchies of Languages generated by Macro Tree Transducers"
The first part of the talk gives an overview of results about macro tree transducers (MTTs). MTTs were invented in the context of programming languages and syntax-directed semantics. There exists a strong relationship between logic and MTTs: the tree translations definable in MSO logic are precisely the macro tree translations of linear size increase. This is a generalization of Buechi's theorem from string to trees and from languages to translations. The second (technical) part of the talk presents a technique, the so called bridge theorem, that is useful in proving strictness of hierarchies. We apply a bridge theorem to show strictness of the hierarchy of output languages of compositions of MTTs. The theorem also implies strictness (at each level) of the IO-hierarchy.
2012-04-24: Neil Jones, "Size Change Termination for the Untyped Lambda Calculus"
2012-03-13: Emanuele D'Osualdo, "Verifying Actor Model Concurrency II"
We present an approach to verify Erlang-style concurrent programs automatically, using a combination of static analysis and infinite-state model checking. Erlang is a higher-order, concurrent and dynamically-typed functional language with pattern-matching algebraic data types, augmented with process creation and message-passing primitives. Since reachability is undecidable we perform an abstraction of the semantics of the Erlang program at hand, and then algorithmically verify coverability, a weaker form of reachability, in the abstract model. The abstract model is in the form of a Vector Addition System (VAS), an infinite state system which enjoys decidability of many interesting verification problems. The abstraction algorithm works in two conceptual steps: in order to handle higher-order computation and synchronization we perform a CFA-like analysis (defined following Van Horn & Might's methodology); exploiting the "flat" but sound representation of the control-flow generated by the analysis we can generate the rules of a VAS that simulates the original program. The generated VAS explicitly models a weak form of message-passing synchronization and dynamic process creation. We show that our method can prove mutual exclusion in a simple Erlang program which spawns an arbitrary number of processes that access a shared resource. To our knowledge, our procedure is the first that can verify a large fragment of Erlang by transformation to a decidable infinite-state system which simulates the input program.
2012-03-06: Steven Ramsay, "A New Abstraction Technique for Functional Programs"
Unlike imperative programs, where the control flow is determined by the truth of predicates over the program variables, the control flow of functional programs is almost entirely determined by pattern matching over algebraic data types. Since the latter is inherently less expressive, we might expect control flow abstractions for functional programs to be cheaper whilst still being sufficiently accurate to facilitate the proof of interesting properties. I will talk about some work in progress developing a new control flow abstraction for functional programs which is set in Cousot and Cousot's framework of abstract interpretation. In an analogy with predicate abstraction for imperative programs, the abstraction is parameterised by a finite set of patterns (rather than predicates) and program rules are abstracted by constructing most general common instances (rather than weakest preconditions). An obvious set of patterns with which to instantiate the parameter in the abstraction is the set of patterns occurring in the program. Time permitting, I can talk about a construction over sets of patterns which is best seen as a categorical limit and which, when applied to the patterns occuring in the program, yields a completeness result.
2012-01-31: David Hopkins, "Observational Equivalence checking for Call-By-Value programs"
He has recently implemented a tool HECTOR for checking observational equivalence of LazyRML (a higher-order functional language with state). He will be contrasting HECTOR with its predecessor HOMER and running us through examples and implementation issues.
2012-01-24: Diana Fischer, "Model Checking the Quantitative mu-Calculus on Initialised Linear Hybrid Systems"
In this talk, we consider the model-checking problem for a quantitative extension of the modal mu-calculus on a class of hybrid systems. Qualitative model checking has been proved decidable and implemented for several classes of systems, but this is not the case for quantitative questions that arise naturally in this context. Recently, quantitative formalisms that subsume classical temporal logics and additionally allow to measure interesting quantitative phenomena were introduced. We show how a powerful quantitative logic, the quantitative mu-calculus, can be model-checked with arbitrary precision on initialised linear hybrid systems.
2011-11-22: Martin Avanzini, "Termination and Complexity Analysis of Term Rewrite Systems"
Term rewriting is an abstract but powerful model of computation that underlies much of declarative programming. In rewriting, termination is a long standing research field. In this talk, I will give an introduction on state-of-the-art termination analysis in the context of term rewriting, in particular I will give an overview of the dependency pair framework. Dependency pairs are nowadays used in virtually all termination provers for term rewrite systems. I am currently working on complexity analysis of rewrite systems. Here one crucial insight is that inspecting a termination proof often reveals information about the complexity of the analyzed TRS. If time allows, I will give a brief overview of this relatively young line of research.
2011-11-15: Rastislav Lenhardt, "Unambiguous Buchi automata"
A unified approach for model-checking fragments of LTL and two variable first order logic on non-deterministic and probabilistic systems. This is joint work with Michael Benedikt and James Worrell.
2011-11-08: Robin Neatherway and Steven Ramsay, "Abstraction-refinement for functional programs"
2011-10-25: Chang Yan, "Reputation systems"
2011-10-18: Michael Vanden Boom, "Further explorations in the cost world"
2011-09-14: Robin Neatherway, "A syntax-directed approach to model checking higher-order recursion schemes"
2011-09-13: Martin Lester, "Verifying Liveness Properties of ML Programs"
2011-08-16: Lihao Liang, "Formal analysis of low-level programs with prioritised interrupts"
We study the stack boundedness problem of a generic language called the Interrupt Calculus that contains essential constructs for programming low-level software with both static and dynamic prioritised interrupts. We show that for a restricted class of low-level programs with static interrupts, stack boundedness can be decided in EXPTIME, whereas the complexity is 2-EXPTIME in the general case. However, the complexity for deciding stack boundedness of programs with dynamic prioritised interrupts is much higher.
2011-08-09: Emanuele D'Osualdo, "Verifying Actor Model Concurrency"
We present an approach to verify Erlang-style concurrent programs automatically, using a combination of static analysis and infinite-state model checking. Erlang is a higher-order, concurrent and dynamically-typed functional language with pattern-matching algebraic data types, augmented with process creation and message-passing primitives. We introduce Communicating Pattern-Matching Recursion Schemes (CPMRS) as a simple and accurate model of computation for the formal analysis of Erlang programs. We use CPMRSs to analyse the reachability problem of higher-order programs that spawn a fixed number of processes, each equipped with an unbounded mailbox. Since the problem is undecidable, our strategy is to compute an over-approximation of the reachable program points. The approximation has three stages. First we perform a binding analysis of the input program (qua CPMRS) to obtain a sound approximant that uses only a finite set of messages. Then we apply a CPS transformation, followed by a flow analysis a la Jones and Andersen, to produce a program that is shallow (i.e. it does not construct any term) and has order 0 (i.e. no call stack is needed). Consequently we obtain an Erlang-like Channel System (ECS) that simulates the input program. A novel communicating system, ECS uses unbounded non-lossy channels, and message passing is not FIFO but rather by Erlang-style pattern matching. Since ECS are a (new) instance of well-structured transition systems, their reachability problem is decidable. We show that our method can prove mutual exclusion in a simple Erlang program which spawns two processes that access a shared resource. To our knowledge, our procedure is the first that can verify a large fragment of Erlang by transformation to a decidable infinite-state system which simulates the input program.
2011-08-02: Michael Vanden Boom, "Weak Cost Monadic Logic over Infinite Trees"
Colcombet recently introduced cost MSO, a quantitative extension to MSO in which sentences define functions from some domain (like words or trees) to the natural numbers extended with a special infinity symbol. By only considering these functions up to a boundedness relation (which ignores exact values but preserves boundedness properties over all subsets of the domain), a rich "theory of regular cost functions" can be developed which parallels the theory of regular languages. For instance, cost MSO can be characterized using automata and games (known as B/S automata and games).
Colcombet and Loeding have developed this theory over finite words and finite trees. I will describe my work extending this theory to infinite trees when restricting to cost WMSO (where second-order quantification is interpreted over finite sets). A crucial ingredient in the proofs is the fact that finite-memory strategies suffice in certain weak B-games which correspond to this weak version of the logic.
2011-07-21: Dulma Rodriguez, "A Type System for Static Heap-Space Analysis of Java-like Programs"
2011-07-19: Steven Ramsay, "The continuation passing style transformation"
2011-07-07: Robin Neatherway, "A new algorithm for model checking HORS"
2011-06-28: Chris Broadbent, "Collapsible Pushdown Automata, First-Order Logic and Generalised Prefix Rewriting"
Collapsible pushdown automata are devices that precisely capture the expressive power of terms in the simply typed lambda calculus with recursion. Higher-order automata are machines endowed with a stack of stacks of stacks of ... stacks generalising standard pushdown automata whose stacks consist of atomic elements. Collapsible pushdown automata extend these with additional structure in the form of `links' between atomic elements and higher-order stacks.
In this talk we consider the transition graphs of these machines. It is known that the transition graphs of higher-order automata without links have decidable MSO theories whilst CPDA render it undecidable even at just order-2. This left open the question of first-order logic and CPDA graphs, which was first addressed by Kartzow (STACS, 2010) in which he showed that order-2 CPDA are tree automatic (can have their relations and domain encoded as regular tree languages) and consequently have decidable first-order theories.
We will present some strong undecidability results for first-order logic for order-3 CPDA graphs and above. Some of these are surprisingly strong; for example order-4 CPDA graphs do not even admit the decidability of first-order sentences without any quantifier alternation whatsoever! If time permits we will also describe a characterisation of 2-CPDA graphs in terms of prefix rewrite systems over Alur et al's nested words. We include a neat characterisation of what it means for an order-2 automaton to have links in this alternative setting. It can also be viewed as a nice generalisation of the characterisation of (order 1) pushdown graphs using prefix rewriting over conventional words.