Meetings During the Term Break 2007

From The Programming Languages and Systems Research Group
Jump to: navigation, search
Monday, 23 July Borzoo Bonakdarpour (Michigan State University): "Exploiting Symbolic Techniques in Automated synthesis of Distributed Programs with Large State Space"
11:15 -- 12:15, CS202J Abstract: Automated formal analysis methods such as program verification and synthesis algorithms often suffer from time complexity of their decision procedures and also high space complexity known as the state explosion problem. Symbolic techniques, in which elements of a problem are represented by Boolean formulae, are desirable in the sense that they often remedy the state explosion problem and time complexity of decision procedures. Although symbolic techniques have successfully been used in program verification, their benefits have not yet been exploited in the context of program synthesis and transformation extensively. In this paper, we present a symbolic method for automatic synthesis of fault-tolerant distributed programs. Our experimental results on synthesis of classical fault-tolerant distributed problems such as Byzantine agreement and token ring show a significant performance improvement by several orders of magnitude in both time and space complexity. To the best of our knowledge, this is the first illustration where programs with large state space (beyond 10^30) is handled during synthesis.

Friday, 21 September Neil Mitchell: "Uniform Boilerplate and List Processing"
13:20 -- 14:00, CS202J Abstract: Generic traversals over recursive data structures are often referred to as boilerplate code. The definitions of functions involving such traversals may repeat very similar patterns, but with variations for different data types and different functionality. Libraries of operations abstracting away boilerplate code typically rely on elaborate types to make operations generic. The motivating observation for this paper is that most traversals have value-specific behaviour for just one type. We present the design of a new library exploiting this assumption. Our library allows concise expression of traversals with competitive performance.

Friday, 21 September Matthew Naylor: "Finding inputs that reach a target expression"
14:00 -- 14:20, CS202J Abstract: We present an automated program analysis, called Reach, to compute program inputs that cause evaluation of explicitly-marked target expressions. Reach has a range of applications including property refutation, assertion breaking, program crashing, program covering, program understanding, and the development of customised data generators. Reach is based on lazy narrowing, a symbolic evaluation strategy from functional-logic programming.

We use Reach to analyse a range of programs, and find it to be a useful tool with clear performance benefits over a method based on exhaustive input generation. We also explore different methods for bounding the search space, the selective use of breadth-first search to find the first solution quickly, and techniques to avoid evaluation that is unnecesary to reach a target.


Friday, 21 September Neil Mitchell: "Supero: Making Haskell Faster"
14:20 -- 15:00, CS202J Abstract: Haskell is a functional language, with features such as higher order functions and lazy evaluation, which allow succinct programs. These high-level features are di±cult for fast execution, but GHC is a mature and widely used optimising compiler. This paper presents a whole-program approach to optimisation, which produces speed improvements of between 10% and 60% when used with GHC, on eight benchmarks.