[Club2] Chris Poskitt's talk next week (on Monday)

[Andrei Popescu]

Dear All, 
The coming Monday, Chris will give us a talk on a language for manipulating graphs and associated verification techniques.   
Chris PoskittHoare-Style Verification of Graph Programs====================================================Mon. Oct. 24, 15:00, MI 00.09.055 ("Alan Turing")
GP (for Graph Programs) is an experimental, nondeterministic programming language which allows one to manipulate graphs at a high level of abstraction. The language frees programmers from low-level data structures, allowing them to model problems as graphs, and solve them by manipulating the graphs directly in a rule-based manner. While the language allows for a more natural way of working with graph-like structures and problems, to reason about the correctness of programs however would previously have required the construction of ad hoc proofs. Recent work at York has led to a Hoare logic proof system for the language, the assertions of which are expressed by "E-conditions", a graphical notation for expressing structural properties and relations between labels. The axiom schemata and inference rules have been shown to be sound in the sense of partial correctness.
This talk will begin with a brief introduction to GP, before exploring our proposed assertion language, the proof rules, an example correctness proof for a graph colouring program, and alluding to some open problems and ongoing work. Finally, the talk will explore how Isabelle might further our project: discussion of this issue is especially welcome (and encouraged!).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20111018/e30af7f3/attachment.html>