19th International Symposium on Formal Methods

---

KEYNOTE SPEAKERS

---

Gerwin Klein Title: "Proof Engineering Considered Essential" Time and Date: 09:00-10:00, Wednesday, 14 April, 2014 Room: LT15 Chair: Jun Sun 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. In particular, the presentation will draw a picture of what these verifications mean and how they fit together into a whole. Among these are a number of firsts: the first code-level functional correctness proof of a general-purpose OS kernel, the first non-interference proof for such a kernel at the code-level, the first binary-level functional verification of systems code of this complexity, and the first sound worst-case execution-time profile for a protected-mode operating system kernel. Taken together, these projects produced proof artefacts on the order of 400,000 lines of Isabelle/HOL proof scripts. This order of magnitude brings engineering aspects to proofs that we so far mostly associate with software and code. In the second part of the talk, I will report on our experience in proof engineering methods and tools, and pose a number of research questions that we think will be important to solve for the wider scale practical application of such formal methods in industry. Home page:http://www.cse.unsw.edu.au/~kleing/ Bio Gerwin Klein is a Senior Principal Researcher at NICTA, Australia's National Centre of Excellence for ICT Research, and Conjoint Associate Professor at UNSW in Sydney, Australia. He is leading NICTA's Formal Methods research discipline and was the leader of the L4.verified project that created the first machine-checked proof of functional correctness of a general-purpose microkernel in 2009. He joined NICTA in 2003 after receiving his PhD from Technische Universität München, Germany, where he formally proved type-safety of the Java Bytecode Verifier in the theorem prover Isabelle/HOL. His research interests are in formal verification, programming languages, and systems code. Gerwin has won a number of awards, among them an award for the best PhD thesis in Germany in 2003 for his work on bytecode verification, and together with his team the best paper award at SOSP'09 for the kernel verification work, the 2011 MIT TR-10 award for the top ten emerging technologies world-wide, and NICTA's Richard E. Newton impact award for the same.

Zhenjiang Hu Title: "Validity Checking of Putback Transformations in Bidirectional Programming" Time and Date: 09:00-10:00, Thursday, 15 April, 2014 Room: LT15 Chair: Cliff B. Jones 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 modifications 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-specification 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 definition 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 specification of our checking algorithms. Home page:http://research.nii.ac.jp/~hu/ Bio Zhenjiang Hu is a full professor of National Institute of Informatics (NII) in Japan. He received his BS and MS degrees from Shanghai Jiao Tong University in 1988 and 1991, respectively, and PhD degree from University of Tokyo in 1996. He was a lecturer (1997–1999) and an associate professor (2000–2007) in University of Tokyo, before joining NII as a full professor in 2008. His main interest is in programming languages and software engineering in general, and functional programming, parallel programming, and bidirectional model-driven software development in particular. He is the academic committee chair of the NII Shonan Meetings, an IFIP WG 2.1 member, and the steering committee members of ICFP, Haskell, APLAS, ICMT, and BX. He is also serving on the editorial board members of IEEE Transactions of Software Engineering, Science of Computer Programming, and Software and Systems Modeling.

Jim Woodcock Title: "Engineering UToPiA Formal Semantics for CML" Time and Date: 09:00-10:00, Friday, 16 April, 2014 Room: LT15 Chair: Jin Song Dong 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/ Bio Jim Woodcock is Head of Department and Professor of Software Engineering at the Department of Computer Science at the University of York. He is a joint leader of the High-Integrity Systems Engineering research group, the largest academic group of its kind in the world. He is a Fellow of the Royal Academy of Engineering and the editor-in-chief of the Springer Formal Aspects of Computing journal. His research area is in the elucidation of sound mathematical principles underlying the practice of software engineering. His research method is based on interactions between abstract theory, pilot development, industrial collaboration, consultancy, tool development, and practical evaluation. He leads the experimental strand of the International Verified Software Initiative.