Verified Software Workshop
October 17–20, 2009, Beijing, China
1980 Turing Award Winner, Principal Researcher of Microsoft Research Cambridge
Tony Hoare and his family first visited China in 1983, with Cliff Jones and family. They both gave lectures at the Graduate School of the Chinese Academy of Sciences. He has visited China three more times since 2000. He was a keynote lecturer at IFIP 2000, and an Einstein Professor of the Chinese Academy in 2006.
Tony Hoare's interest in computing was awakened in the early fifties, when he studied philosophy (together with Latin and Greek) at Oxford University, under the tutelage of John Lucas. He was fascinated by the power of mathematical logic as an explanation of the apparent certainty of mathematical truth. During his National Service (1956-1958), he studied Russian in the Royal Navy. Then he took a qualification in statistics (and incidentally) a course in programming given by Leslie Fox). In 1959, as a graduate student at Moscow State University, he studied the machine translation of languages (together with probability theory, in the school of Kolmogorov). To assist in efficient look-up of words in a dictionary, he discovered the well-known sorting algorithm Quicksort.
On return to England in 1960, he worked as a programmer for Elliott Brothers, a small scientific computer manufacturer. He led a team (including his later wife Jill) in the design and delivery of the first commercial compiler for the programming language Algol 60. He attributes the success of the project to the use of Algol itself as the design language for the compiler, although the implementation used decimal machine code. Promoted to the rank of Chief Engineer, he then led a larger team on a disastrous project to implement an operating system. After managing a recovery from the failure, he moved as Chief Scientist to the computing research division, where he worked on the hardware and software architecture for future machines. These machines were cancelled when the Company merged with its rivals, and in 1968 Tony took a chance to apply for the Professorship of Computing Science at the Queen's University, Belfast. His research goal was to understand why operating systems were so much more difficult than compilers, and to see if advances in programming theory and languages could help with the problems of concurrency. In spite of civil disturbances, he built up a strong teaching and research department, and published a series of papers on the use of assertions to prove correctness of computer programs. He knew that this was long term research, unlikely to achieve industrial application within the span of his academic career.
In 1977 he moved to Oxford University, and undertook to build up the Programming Research Group, founded by Christopher Strachey. With the aid of external funding from government initiatives, industrial collaborations, and charitable donations, Oxford now teaches a range of degree courses in Computer Science, including an external Master's degree for software engineers from industry. The research of his teams at Oxford pursued an ideal that takes provable correctness as the driving force for the accurate specification, design and development of computing systems, both critical and non-critical. Well-known results of the research include the Z specification language, and the CSP concurrent programming model. A recent personal research goal has been the unification of of a diverse range of theories applying to different programming languages, paradigms, and implementation technologies.
Throughout more than thirty years as an academic, Tony has maintained strong contacts with industry, through consultancy, teaching, and collaborative research projects. He took a particular interest in the sustenance of legacy code, where assertions are now playing a vital role, not for his original purpose of program proof, but rather in instrumentation of code for testing purposes. On reaching retirement age at Oxford, he welcomed an opportunity to go back to industry as a senior researcher with Microsoft Research in Cambridge. He hopes to expand the opportunities for industrial application of good academic research, and to encourage academic researchers to continue the pursuit of deep and interesting questions in areas of long-term interest to the software industry and its customers.
Abstract: Theory for Verified Software
Tony Hoare will present his current approach to Unifying Theories of Programming. It unifies sequential and concurrent programming, using ideas from separation logic. Every tool that is used for software verification must be based on a theory of programming (sometimes called semantics). The use of tools in combination requires the definition of an interface, based on a theory that unifies the theories on which the separate tools are based. As in other branches of Science, he hopes that this unifying theory can be simpler than the theories which it unifies. His new approach uses pictorial representations from labelled graph theory, in place of the relational calculus used in the book by Hoare and He. It should therefore be suitable for non-theorists.
Research Area Manager, Microsoft Research
Wolfram Schulte is a principal researcher at Microsoft Research Redmond and the founding manager of that lab's Research in Software Engineering area. He joined Microsoft Research in 1999 as an individual researcher.
His research concerns the practical application of formal methods. At Microsoft, he has co-lead research projects on on software analysis and verification (the Spec# and VCC projects), on software testing (the Pex, SpecExplorer, and nModel projects), on programing language and runtime system design (the AsmL, Cω, and TPL projects), and, lately, on model-driven engineering of applications for embedded systems and the cloud (the Formula and BAM project). Before joining Microsoft Research, he worked at the University of Ulm (1993-1999), at sd&m, a German software company (1992-1993), and at the Technical University Berlin (1987-1992).
He lives in Bellevue, Washington, with his wife Rita and his two children. In his spare time, he enjoys the beautiful outdoors of the Cascades.
Building Program Analyzers: A Quick Tour through Microsoft Research’s Tool Repertoire
Wolfram Schulte joined work with the RiSE team.
Modern program analysis and model-based tools are increasingly complex and multi-faceted software systems. They analyze models and programs using advanced type systems, model checking or model finding, abstract interpretation, symbolic verification or a combination there of.
In this talk he will discuss and compare 10 program analysis tools that have been successfully developed and deployed within Microsoft and beyond (Slam, ESP, Spec#, Havoc, VCC, Pex, Sage, SpecExplorer CodeContracts, Formula). It turns out that most of these analyzers build on generic infrastructure, most of which is available for academic research. Major components of the infrastructure are an easily customizable compiler/runtime system (CCI and extended reflection), a simple intermediate language targeted for analysis of imperative programs (Boogie), and powerful logic inference engines for abstract interpretation (Clousot) or logic formulas (Z3).
With every analyzer build there is a new opportunity, and with every solution there is a new challenge problem. Thus, They also summarize 10 challenges in program analysis which hopefully triggers new aspiring directions in our joint quest of building verified software.
Professor of Software Engineering, Department of Computer Science, University of York
Jim Woodcock holds the Anniversary Chair in Software Engineering at the University of York. Previously, he was Professor of Software Engineering at the University of Oxford, where he founded its Centre of Excellence in Software Engineering.
His current research interests include the Grand Challenge in Verified Software; industrial-scale, evidence-based, software and hardware engineering; unifying theories of programming; verifying models of railway signalling; and timebands in real-time systems.
His research team won the Queen's Award for Technological Achievement in 1992 for its work with IBM. He was the academic consultant for the first product certified to ITSEC Level E6 (in 1998, now equivalent to Common Criteria EAL7), and he served for over ten years as an advisor on secure systems to the British and US governments. In 2002, he won the Rudolf Christian Carl Diesel Prize from the Society for Design and Process Science.
He is an active participant in the international Grand Challenge in Verified Systems, and the moderator for the UK Grand Challenge in Dependable Systems Evolution. He is Joint Editor-in-Chief of the Formal Aspects of Computing Journal; he has served on more than sixty international conference programme committees, and has chaired fifteen of them. He has given invited papers and keynote speeches at over thirty conferences, and is the author of nearly 200 scientific papers and books. He is currently a Visiting Professor at Trinity College Dublin, the Federal Universities of Pernambuco and Rio Grande do Norte in Brazil, and a Visiting Fellow at the University of Oxford. He has twice served as the Formal Methods Europe Lecturer on lecture tours in South America, and twice for the British Council in Central Europe and North Africa. He is a director of the British Council UK-India workshops on embedded systems. He has acted as a consulting software engineer for many organisations, including AWE, British Energy, DEC, General Dynamics, IBM, LDRA, Logica, Praxis, QinetiQ, and the UK Health & Safety Executive. He is a Chartered Fellow of the British Computer Society.
Abstract: Experiments in the Grand Challenge in Verified Software
Jim Woodcock will describe some experiments conducted as part of pilot projects in the Verified Software Initiative (VSI). He begins by recounting the background to the VSI and its six initial pilot projects, and give an update on the current progress of each project. He describes two of these in greater detail: the Tokeneer ID Station and the POSIX-compliant flash file-store.
Tokeneer was developed by Praxis High Integrity Systems and SPRE for the U.S. National Security Agency, and it has been acclaimed by the US National Academies as representing best practice in software development. To date, only two errors have been found in Tokeneer, and the entire project archive has been released for experimentation within the VSI. He describes the first experiment using the Tokeneer archive, where the objective is to investigate the dependability claims for Tokeneer as a security-critical system. The experiment uses a model-based testing technique that exploits formal methods and tools to discover 12 anomalous scenarios. Jim and his team discuss four of these anomalies.
The POSIX-compliant flash file-store project was suggested by Holzmann and Joshi. Flash file-stores form an important component of modern space-craft, and the failure of this component threatened the Mars Rover missions. This led to an initial interest in creating a trusted component, mechanically verified from the specification of the POSIX-compliant interface all the way down to the flash-translation layer (FTL) managing the hardware. Jim describes two experiments in verifying an algorithm in the FTL for multi-sector reading (MSR), a core logic used in newer flash management software. An MSR function was recently added to the FTL for an existing flash-memory product. However, this function caused numerous errors in spite of extensive testing and debugging efforts, to the extent that the developers seriously considered removing the feature. Jim describes two experiments carried out to analyse this particular MSR function. One involves concolic testing, and the other involves specification extraction, theorem proving, and auto-coding.
Professor, Software Engineering Institute, East China Normal University
Member of Chinese Academy of Sciences
Jifeng He graduated in 1965 from Fudan University majoring in mathematics. He is currently the Dean of the Institute of Software of East China Normal University.
Prof. He's research interests include Credible and Information Security Theory, Formal Method, Concurrent Programming, Theory, Embedded system design methods and tools, Hybrid system hardware and software co-design Computer Software and Theory. He was elected a Member of Chinese Academy of Sciences in 2005.
Abstract: Trustworthy Software in China
In this talk, they will discuss the current state, progress and future of the research on trustworthy software project in China. This project has been launched by NSFC for a seven-year one that focuses on the fundamental theories and techniques for trustworthy computing. We also would like to discuss how to strength the international cooperation on this field.
Researcher, Institute of Software, Chinese Academy of Sciences
Member of Chinese Academy of Sciences
Huimin Lin received PhD in Computer Science from the Institute of Software, Chinese Academy of Sciences, in 1986. He is currently the chairman of the Academic Committee of the Institute of Software, Chinese Academy of Sciences, and the director of the State Key Laboratory of Computer Science.
Prof. Lin's research interests include concurrency, model checking, and formal methods. He was elected a Member of Chinese Academy of Sciences in 1999.
Abstract: Research on Verification at Laboratory of Computer Science
As a state key laboratory, the Laboratory of Computer Science at the Institute of Software, Chinese Academy of Sciences, is committed to fundamental research on computer software and computer science in general. Formal approaches to producing correct, trust-worthy software systems, either sequential or concurrent, is a major research area of the laboratory. In this talk I'll review some current research activities on software verification in the laboratory, including correctness proving and model checking
Professor, Behang University
Member of Chinese Academy of Sciences
Wei Li, was born in June1943, Beijing. He graduated in 1966 from Peking University majoring Mathematics and Mechanical Engineering, received PhD in Computer Science from University of Edinburgh, in 1983. He was president of Beihang University from Jan. 2002 to May 2009.
Prof. Li's research interests include Practical concurrent language operational semantics, Amendment calculus formal system, Formal theory sequence and its limit, Formal axiomatic process. He was elected a Member of Chinese Academy of Science in 1997
Researcher, Institute of Software, Chinese Academy of Sciences
Member of Chinese Academy of Sciences
Chaochen Zhou is a Professor at the Computer Science Laboratory, Institute of Software, Chinese Academy of Sciences. He graduated from Department of Mathematics and Mechanics, Peking University in 1958, and finished his postgraduate study on Mathematical Logic in 1967 at Institute of Computing Technology, CAS. In 1993, he was elected as a Member of Chinese Academy of Sciences, and in 2000 as a Fellow of Third World Academy of Sciences.
He has been interested in Formal Methods for many years, in particular in CSP and formal design of real-time systems. Currently he is interested in applying computer algebra to program verification.
Professor, School of Computer Science and Engineering, The University of New South Wales
Gernot Heiser holds the John Lions Chair of Operating Systems at the University of New South Wales (UNSW), and leads the Secure Embedded Systems (ERTOS) group at NICTA, Australia's National Centre of Excellence for ICT Research. He joined NICTA at its creation in 2002, and before that was a full-time member of academic staff at UNSW from 1991. His past work included the Mungi single-address-space operating system, several un-broken records in IPC performance, and the best-ever reported performance for user-level device drivers.
In 2006, Gernot with a number of his students founded Open Kernel Labs, now the market leader in secure operating-systems and virtualization technology for mobile wireless devices. The company's OKL4 operating system, a descendent of L4 kernels developed by his group at UNSW and NICTA, is deployed in more than 300 million mobile phones. This includes the Motorola Evoke, the first (and to date only) mobile phone running a high-level OS (Linux) and a modem stack on the same processor.
In a former life, Gernot developed semiconductor device simulators and models of device physics for such simulators, and pioneered the use of three-dimensional device simulation for the characterisation and optimisation of high-performance silicon solar cells.
Abstract: 8,700 LoC, 1 Microkernal, 0 Bugs
This talk reports on a project to design, implement and formally verify a complete operating-system kernel. Over the last five years the ERTOS team at NICTA developed seL4, a member of the L4 microkernel family aimed at use in security- and safety-critical embedded systems. The key design goals were the seemingly conflicting requirements of (i) performance comparable with the fastest L4 kernels, and (ii) suitability for full formal verification, meaning the mathematical proof of functional correctness. These goals were achieved in mid-2009. In addition, some simple security properties were proved.
To the best of the team's knowledge, this represents the first ever complete formal verification of a general-purpose operating system kernel, leave alone a high-performance system. The talk will outline the approach taken to the design, implementation and verification of seL4, and will discuss some of the lessons learned.
Professor, Computing Laboratory, University of Oxford
Daniel Kroening received the M.E. and doctoral degrees in computer science from the University of Saarland, Saarbruecken, Germany, in 1999 and 2001, respectively. He joined the Model Checking group in the Computer Science Department at Carnegie Mellon University, Pittsburgh PA, United States, in 2001 as a Post-Doctorate.
He was appointed as an assistant professor at the Swiss Technical Institute (ETH) in Zurich, Switzerland, in 2004. Since 2007, he is a Reader at the Computing Laboratory at Oxford University and a fellow of Magdalen College, Oxford. His research interests include automated formal verification of hardware and software systems, decision procedures, embedded systems, and hardware/software co-design.
Abstract: Model Checking C++ Programs that use the STL
Daniel Kroening presents a formalization of the most relevant abstract data types provided by the standard template library (STL). He also provides an operational model, and outline the proof that the operational model is conservative with respect to our formalization. He concludes with experimental evidence that this model enables the automated verification of significant C++ programs.
Associate Professor, Computer Science and Electrical Engineering, Stanford University
Dawson Engler is an Associate Professor in Computer Science and Electrical Engineering at Stanford University. He received his PhD from the Massachusetts Institute of Technology (MIT) for his work on the exokernel operating system, and his undergraduate degree from University of Arizona. His research focuses on developing techniques to find interesting bugs in real code, including static analysis, implementation level model checking, and symbolic execution. The tools he has developed have found thousands of errors in open-source systems and the static work formed the basis of a company, Coverity. In 2006, he won the Weiser award and in 2009, the Hopper award.
Abstract: Automatically executing almost all statements with all values in real programs
Dawson will talk about a tool they built, KLEE, which uses a variant of symbolic execution to automatically generate test cases that execute most statements in real programs. KLEE is a sound tool, with no approximations in its constraints, yet works well in practice. In their experiments, it achieved 95 percent average coverage on more than 150 widely-used, complex, and environmentally-intensive programs. This coverage significantly beat that of the developer's own hand-written tests and found numerous errors, which KLEE generated concrete inputs to demonstrate.
He will also discuss how to use KLEE to verify path correctness with little manual work in the case where there are two or more implementations of the same interface. There may also be some discussion about the relative tradeoffs of static versus dynamic tools and academia versus industry.
Researcher, Microsoft Research Redmond
Ethan Jackson is a researcher in RiSE (Research in Software Engineering) at Microsoft Research Redmond. He researches formal methods for model-based development of complex software systems. This work encompasses domain-specific languages, model transformations, and correct-by-construction techniques; application areas include embedded and cyber-physical systems. Ethan received his PhD from the Institute for Software Integrated Systems (ISIS) at Vanderbilt University and joined Microsoft Research in 2007.
Abstract: Generalizing Design-Space Exploration with FORMULA
Design-space exploration (DSE) is the exploration of design alternatives prior to implementation. The power to operate on the space of possible designs decisions makes DSE useful for many software engineering tasks, including rapid prototyping, optimization, and system integration. Despite its potential, DSE is not widely used in software engineering. Instead its use occurs primarily in software/hardware co-design and software product lines.
In this presentation Ethan Jackson describes a novel framework, called FORMULA, for generalizing DSE techniques: Design spaces are specified as domain specific languages (DSLs) with expressive constraints. Next, a symbolic execution engine generates quantifier free formulas whose solutions are non-trivial designs. These formulas are evaluated by the state-of-the-art satisfiability modulo theories (SMT) solver Z3. A novel exploration algorithm guides the solver towards distinctly different designs. Finally, automated graph layout is used to present design variants immediately upon exploration.
Vania Joloboff is Research Director at LIAMA, Beijing, working in the FORMES research collaborative project between INRTIA and Tsinghua University. Prior to joining INRIA in 2007, Dr. Joloboff was Chief Technical Officer at Silicomp Group. Vania Joloboff is Research Director at LIAMA, Beijing, working in the FORMES research collaborative project between INRTIA and Tsinghua University. Prior to joining INRIA in 2007, Dr. Joloboff was Chief Technical Officer at Silicomp Group.
Formerly, Vania Joloboff has been Technical Director at the Open Software Foundation Research Institute, heading development of the Embedded Java technology and OSF Motif technology. OSF/Motif has become the worldwide standard IEEE 1295 and was included in the CDE desktop solution from HP, IBM and Sun. He contributed to the X Window standard specifications, in particular the internationalization specifications to support Asian languages.
Prior to joining OSF, he founded and directed the Bull Research Center at Sophia-Antipolis, a lab that distributed the open source GWM software.
Dr. Joloboff has been Part-Time Professor at University of Grenoble and University of Nice. He graduated from Ecole des Mines (France) and received a doctorate degree from University of Grenoble (France).
Dr. Joloboff contributed to several standards, including IEEE 1295, IEEE P1201, and ISO 20970. He was elected Chairman of the J-Consortium for year 2003.
Abstract: The FORMES Project
FORMES (FORmal Methods for Embedded Systems) is a cooperation project between INRIA (France) and Tsinghua University (China) also supported by funding from China NSFC and France ANR.
The FORMES project aims at addressing the challenges of embedded systems design and certification with a new approach, combining fast hardware simulation techniques with advanced formal methods for verification.
The talk will describe the verification and simulation tools used in the project, those under construction, and expand on the faced challenges.