Difference between revisions of "Current events"

From The Programming Languages and Systems Research Group
Jump to: navigation, search
(Meetings in Spring 2007)
Line 17: Line 17:
Details of [[Meetings| meetings in previous years]] are available.
Details of [[Meetings| meetings in previous years]] are available.
== Meetings in Spring 2007 ==  
== Meetings in Summer 2007 ==  
{{EListEntry|312|Thursday, 18 January|12:15 -- 13:15, CS202J|Neil Mitchell|Playing with Haskell data|Often when programming with complex data most of the code is "boilerplate" - boring code which navigates through the data to find the interesting bit and perform some operation on it. This talk describes the 'Play' approach for Haskell, which allows this boilerplate code to be written once, and then reused to perform a variety of traversals and queries upon the data.}}
{{EListEntry|322a|Thursday, 03 May|12:20 -- 12:40, CS202J|Ian Boden|Animating Simulated Annealing with Lego Mindstorms|This project explores the physical animation of simulated annealing using Lego Mindstorms, and assesses the suitability of this approach to algorithm animation for use as an interactive teaching aid.}}
{{EListEntry|313|Thursday, 25 January|12:15 -- 13:15, CS202J|Leo Freitas|FDR Explorer|We describe the internal structures of FDR, the refinement model checkerfor Hoare's Communicating Sequential Processes (CSP), as well as an Application Programming Interface (API) allowing one to interact more closely with, and have fine grained control over, FDR's behaviour and data structures. FDR stands for Failures Divergences Refinement.
{{EListEntry|322b|Thursday, 03 May|12:40 -- 13:00, CS202J|Ben Mitchel|Animation of Garbage Collection Algorithms using Lego Mindstorms|}}
With such information it is possible to create optimised CSP code to perform refinement checks that are more space/time efficient, hence enabling the analysis of more complex and data intensive specifications. This information is very valuable for both CSP users and tools that automatically generate CSP code, such as those related to security analysis generating test-cases as CSP processes. We present examples of using the tool, which include advanced features like FDR's transparent functions that can be used to considerably compress the state space to be checked. Finally, we show how one can transform FDR's graph format into a graph notation (e.g. JGraph), hence enabling visualisation of Labelled Transition Systems (LTS) of CSP specifications.}}
{{EListEntry|314|Thursday, 01 February|12:15 -- 13:15, CS202J|Ian Toyn|Formal Validation of Hierarchical State Machines against Expectations|This PLASMA talk is a practice for a conference presentation. The paper explains some analyses that can be performed on a hierarchical finite state machine to validate that it performs as intended. Intentions are captured per state as expectations on input values. The analyses determine whether the expectations are consistent, and the conditions under which the state machine conforms to the expectations. The presentation uses an example to explain the formal analyses.}}
The list above contains only talks for which at least a speaker and a title are available. The full schedule with incomplete talks and empty slots is available under [[Meetings_in_Summer_2007|Meetings in Summer 2007]].
{{EListEntry|315|Thursday, 08 February|12:15 -- 13:15, CS202J|Matthew Naylor|Embedded Functional-Logic Programming|Functions are a great programming abstraction, but *relations* are more general.  We will show how relations can be described in a plain functional language using a library that we have developed for functional-logic programming in Haskell.  We will compare the library with the dedicated functional-logic language Curry, and discuss the extent to which functional-logic programming can be supported without the need for a dedicated language.
The original aim of this work was to show a nice way to implement Wired, a relational language for circuit design that is being developed at Chalmers University.  Subsequently, we have found another application for the work in the design and implementation of Reach, a very cool program analysis invented by Colin Runciman.  We will briefly discuss the use of functional-logic techniques in these two applications.}}
{{EListEntry|316|Thursday, 15 February|12:15 -- 13:15, CS202J|Leo Freitas|POSIX and the Grand Challenge|We describe ongoing work on a second grand challenge for the verified software repository. This work is the specification, refinement, and proof a minimal file store interface for flash memory devices adhering to a POSIX interface that was proposed by NASA's Jet Propulsion Laboratory to be used in the next (Mars) missions. The aim is to provide a proof correct version of file system related (POSIX) API's as part of the formalisation of UNIX (the whole of POSIX).
Part of the challenge is in addressing not only correct functionality, but critical levels of fault tolerance due to the nature of the environment the software is expected to run in. In this talk, we present the current status of this work and where we aim to go in the next two years. We also want to foment curiosity in the community for those interested in joining in this effort.
Links: [http://www.cs.york.ac.uk/plasma/talkrelated/316-slides.pdf slides] (PDF)}}
{{EListEntry|317|Thursday, 22 February|12:15 -- 13:15, CS202J|Jan Tobias Muehlberg|Towards a Simulation-based Verification of Memory Safety Properties for Object Code Programs|While most of us (as long as we are not writing Haskell code) got used to gaps between our intention and the code we write, we usually do not think about mismatches between our intention and the compiler's understanding of the language we are programming in. However, computers do not execute source-code programs and one of the greatest hazards in programming still arises from the use of pointer operations in unsafe programming languages such as C: If a program dereferences an invalid pointer, the program will either crash or behave in an undefined way. Unfortunately, these errors are common, difficult to debug and not covered by today's software verification systems.
In this talk I will give an overview of my ongoing work on developing a simulation-based framework for the validation of safety properties for pointer operations in object code programs. After defining the properties of interest, I will show how data-flow analysis and program slicing can be employed in order to generate program abstractions that preserve interesting memory safety properties and make efficient program simulation possible. Running examples are taken from the thrilling domain of Linux device drivers.
Links: [http://www.cs.york.ac.uk/plasma/talkrelated/317.pdf slides] (PDF)}}
{{EListEntry|318|Thursday, 01 March|12:15 -- 13:15, CS202J|Matthew Naylor, Jan Tobias Muehlberg|FUN with Lego Mindstorms|In this talk, we will present how Lego Mindstorms robots can serve as a delightful example for the development of safety-critical embeded software systems. We will give a brief overview of Esterel's SCADE suite and show how it can be used to design programs for Lego robots, to prove safety properties for these programs and to generate C source code that actually runs on the Mindstorms RCX. In addition to this, Matthew will explain how the whole stuff can be done using Haskell. The talk is based on our experience from the Reactive Systems Design module.
Links: [http://www.cs.york.ac.uk/plasma/talkrelated/318.pdf slides] (PDF)}}
{{EListEntry|319|Thursday, 08 March|12:15 -- 13:15, CS202J|Emil Axelsson (Chalmers University of Technology, Göteborg, Sweden)|Low-level hardware design and library reuse in Haskell|I will present Wired -- a domain-specific language for low-level hardware design in Haskell. One of the big strengths of the current implementation is its simplicity due to reuse of other libraries. Wired is built on the following three (Haskell) libraries: (1) LP for general-purpose logic programming, (2) Lava for functional hardware description, and (3) RLava for relational hardware description. I will present these libraries one by one, and show each of their roles in the Wired library. I will also give a (semi-) realistic example of a parallel prefix circuit. In just a few lines, we will be able to capture the full circuit, including cell placement and wire routing.
Links: [http://www.cs.york.ac.uk/plasma/talkrelated/wired.pdf slides] (PDF)}}
{{EListEntry|320|Thursday, 15 March|12:15 -- 13:15, CS119N|Neil Mitchel and Greg Manning|Random BCTCS Stuff|
Neil Mitchel: "First Order Haskell" -- Haskell is a higher order programming language, with functions as first class data values. Haskell has explicit lambdas, currying, monads and type classes - all of which introduce higher order functions into a program. While these higher order functions serve to make code more compact, they can prove awkward when it comes to program analysis. This talk describes a method for removing all higher order functions from a Haskell program, keeping the structure of the original program where possible.
Greg Manning: "The GP Project: Environment and Implementation" -- GP (for Graph Programs) is a rule-based programming language for solving graph problems at a high level of abstraction, freeing programmers from dealing with low-level data structures. The core of GP consists of just three constructs: single-step application of a set of conditional graph-transformation rules, application of a rule set as long as possible, and sequential composition of programs. The addition of a few powerful branching and iterating constructs make the language much easier to use whilst preserving the simple semantics.
As the implementation of GP nears maturity, we will discuss the overall structure of the components and some of the issues which have arisen in the development of this highly non-deterministic graph-transformation based system.}}
The list above contains only talks for which at least a speaker and a title are available. The full schedule with incomplete talks and empty slots is available under [[Meetings_in_Spring_2007|Meetings in Spring 2007]].
== Other events ==
== Other events ==

Revision as of 15:00, 30 April 2007

Thursday, 15 March Neil Mitchel and Greg Manning: "Random BCTCS Stuff"

Regular group meetings

During term time we meet each week to discuss topical issues. A discussion may be initiated by a short talk given by a member or guest of the group.

Talks can be booked by contacting Jan Tobias Muehlberg. Suitable topics are:

  • Any subject related to programming languages and systems
  • Work in progress to discuss, or ideas you've been mulling over
  • Reports on a paper you read, a recent conference, workshop or visit to another institution, which you think may interest other members of the group
  • Practice for a talk you will be giving at a conference or workshop to obtain feedback from your colleagues

Details of meetings in previous years are available.

Meetings in Summer 2007

Thursday, 03 May Ian Boden: "Animating Simulated Annealing with Lego Mindstorms"
12:20 -- 12:40, CS202J Abstract: This project explores the physical animation of simulated annealing using Lego Mindstorms, and assesses the suitability of this approach to algorithm animation for use as an interactive teaching aid.

Thursday, 03 May Ben Mitchel: "Animation of Garbage Collection Algorithms using Lego Mindstorms"
12:40 -- 13:00, CS202J Abstract:

The list above contains only talks for which at least a speaker and a title are available. The full schedule with incomplete talks and empty slots is available under Meetings in Summer 2007.

Other events

Thursday, 31 August 2006 Jonathan Ezekiel: "Can Saturation be Parallelised? On the Parallelisation of a Symbolic State-Space Generator"
14:430 -- 15:00, PDMC, Bonn (satellite of CONCUR) Abstract: Symbolic state-space generators are notoriously hard to parallelise. However, the Saturation algorithm implemented in the SMART verification tool differs from other sequential symbolic state-space generators in that it exploits the locality of firing events in asynchronous system models.

This paper explores whether event locality can be utilised to efficiently parallelise Saturation on shared-memory adrchitectures. Conceptually, we propose to parallelise the firing of events within a decision diagram node, which is technically realised via a thread pool. We discuss the challenges involved in our parallel design and conduct experimental studies on its prototypical implementation. On a dual-processor dual-core PC, our studies show speed-ups for several example models, e.g., of up to 50% for a Kanban model, when compared to running our algorithm only on a single core. (Joint work with Gerald Luettgen and Radu Siminiceanu)

Sunday, 27 August 2006 Jan Tobias Muehlberg: "BLASTing Linux Code"
About 11:45, FMICS, Bonn (satellite of CONCUR) Abstract: Computer programs can only run reliably if the underlying operating system is free of errors. In this paper we evaluate, from a practitioners point of view, the utility of the popular software model checker BLAST for revealing errors in Linux kernel code. The emphasis is on important errors related to memory safety in and locking behaviour of device drivers. Our conducted case studies show that, while BLAST's abstraction and refinement techniques are efficient and powerful, the tool has deficiencies regarding usability and support for analysing pointers, which are likely to prevent kernel developers from using it. (Joint work with Gerald Luettgen)

Links: slides, paper and additional material

Sunday, 2 April 2006 Greg Manning: "The York Abstract Machine"
About 2pm, GT-VMT, Vienna (satellite of ETAPS) Abstract: We introduce the York Abstract Machine (YAM) for implementing the graph programming language GP and, potentially, other graph transformation languages. The advantages of an abstract machine over a direct interpreter for graph transformation rules are better efficiency, use as a common target for compiling both future versions of GP and other languages, and portability of GP programs to different platforms.