Title: "Proof Engineering Considered Essential"
Time and Date: 09:00-10:00, Wednesday, 14 April, 2014
Abstract: In this talk, I will give an overview of the various formal verification projects around the evolving seL4 microkernel, and discuss our experience in large scale proof engineering and maintenance.
Title: "Validity Checking of Putback Transformations in Bidirectional Programming"
Time and Date: 09:00-10:00, Thursday, 15 April, 2014
Abstrat: A bidirectional transformation consists of pairs of transformations |a forward transformation get produces a target view from a source, while a putback transformation put puts back modifications on the view to the source| satisfying sensible roundtrip properties. Existing bidirectional approaches are get-based in that one writes (an artifact resembling) a forward transformation and a corresponding backward transformation can be automatically derived. However, the unavoidable ambiguity that stems from the under-specification of put often leads to unpredictable bidirectional behavior, making it hard to solve nontrivial practical synchronization problems with existing bidirectional transformation approaches. Theoretically, this ambiguity problem could be solved by writing put directly and deriving get, but diff erently from programming with get it is easy to write invalid put functions. An open challenge is how to check whether the definition of a putback transformation is valid, while guaranteeing that the corresponding unique get exists. In this paper, we propose, as far as we are aware, the rst safe language for supporting putback-based bidirectional programming. The key to our approach is a simple but powerful language for describing primitive putback transformations. We show that validity of putback transformations in this language is decidable and can be automatically checked. A particularly elegant and strong aspect of our design is that we can simply reuse and apply standard results for treeless functions and tree transducers in the specification of our checking algorithms.Home page:http://research.nii.ac.jp/~hu/
Title: "Engineering UToPiA Formal Semantics for CML"
Time and Date: 09:00-10:00, Friday, 16 April, 2014
Abstract: We describe the semantic domains for Compass Modelling Language (CML), using Hoare & He’s Unifying Theories of Program- ming (UTP). CML has been designed to specify, design, compose, sim- ulate, verify, test, and validate industrial systems of systems. CML is a semantically heterogeneous language, with state-rich imperative con- structs based on VDM, communication and concurrency based on CSP, object orientation with object references, and discrete time based on Timed CSP. A key objective is to be semantically open, allowing further paradigms to be added, such as process mobility, continuous physical models, and stochastic processes. Our semantics deals separately with each paradigm, composing them with Galois connections, leading to a natural contract language for all constructs in all paradigms. The result is a compositional formal definition of a complex language, with the indi- vidual parts being available for reuse in other language definitions. The work backs our claim that use of UTP scales up to industrial-strength languages: Unifying Theories of Programming in Action (UToPiA).Home page: http://www-users.cs.york.ac.uk/~jim/