Verified Software Repository Report

Introduction

The Verified Software Repository (VSR) is a first step towards the realisation of the goals of the Verified Software Challenge. It will maintain and develop an evolving collection of state-of-the-art tools, together with a representative portfolio of real programs and specifications on which to test, evaluate, and develop the tools. It will contribute initially to the inter-working of tools, and eventually to their integration. It will promote transfer of the relevant technology to industrial tools and into software engineering practice. It will build on the recognised achievements of practical formal development of safety-critical computer applications, and contribute to the international initiative in verified software, covering theory, tools, and experimental validation. The repository will retaian a central role as the challenge develops.

The VSR is described more fully in the journal paper The verified software repository: a step towards the verifying compiler. In the UK, an EPSRC-funded project (VSR-net) is helping to plan the repository. Further details about VSR-net can be found through its wiki.

The Verified Software Repository panel (Juan Bicarregui, Joseph Kiniry, Tiziana Margaria, Leonardo de Moura, David Naumann, Sam Owre, John Rushby, Natarajan Shankar, Bernhard Steffen, and Jim Woodcock) met at SRI in Menlo Park on the 2nd and 3rd of February 2006, and then again on the 1st and 2nd of April. This report outlines a road map for setting up, populating, and maintaining a repository.

Goals of the Panel

• To create a road map for building a repository of verified software, verification tools, benchmarks, challenge problems, models, specifications, and case studies.
• Coordinating the activities involved in setting up the repository and creating the processes for curating and maintaining the repository.
• Generating publicity to broaden the participation in the development of the repository.

Goals of the Repository

• To accelerate the development of verification technology through the development of better tools, greater interoperability, and realistic benchmarks.
• To provide a focus for the verification community to ensure that the research results are relevant, replicable, complementary, and cumulative, and promote meaningful collaboration between complementary techniques.
• To provide open access to the latest results and educational material in areas relevant to verification research.
• Collect a significant body of verified code (specifications, assertions, derivations, proofs, models, implementations) that addresses challenging applications.
• Identify key metrics for evaluating the scale, efficiency, depth, amortization, and reusability of the technology.
• Enumerate challenge problems and areas for verification, preferably ones that require multiple techniques.
• Identifying (and eventually standardizing) formats for representing and exchanging specifications, programs, test cases, proofs, and benchmarks, to support tool interoperability and comparison.
• Defining quality standards for the contents of the repository.

Funding

• NSF, NASA
• EU 7th framework: Open platforms, complex systems.
• DFG, BMBF
• SFI, Enterprise Ireland
• China
• EPSRC
• Commercial sponsors: Microsoft, Cisco, Intel, AMD, IBM, TCS. Commercial funding could be used to support Prize money, meetings, travel, fellowships.

People

Jacob Abraham (Texas), Jean-Raymond Abrial (ETH Zurich), Luca de Alfaro (UCSC), Andrew Appel (Princeton), Clark Barrett (NYU), Gilles Barthe (INRIA), David Basin (ETH Zurich), Sergey Berezin (Synopsis), Ramesh Bhardwaj, Juan Bicarregui (Rutherford Lab), Mark Bickford(Cornell), Paul Boca (Celoxica), Egon Boerger (Pisa), Jonathan Bowen (LSBU), Guillaume Brat, Ed Brinksma (Twente), Michael Butler (Southampton), Ana Cavalcanti (York), Marsha Chechik (Toronto), Alessandro Cimatti (Trento), Ernie Cohen (Microsoft), Byron Cook (Microsoft), Patrick Cousot (Paris), Karl Crary (CMU), Jim Davies (Oxford), Rance DeLong (Santa Clara), John Derrick (Sheffield), Kevin Driscoll, William Farmer (McMaster), Kokichi Futatsugi (JAIST), Chris George (Macau), Chris Gill (Washington), Helen Gill (NSF), Michael Goldsmith (Formal Systems), Sol Greenspan (MIT), Wolfgang Grieskamp (Microsoft), Orna Grumberg (Technion), Jim Grundy (Intel), Josh Guttman (Mitre), Masami Hagiya (Tokyo), Anthony Hall, John Harrison (Intel), Alan Hartman (IBM), John Hatcliff (Kansas), Klaus Havelund (Kestrel), He Jifeng (Macau), Connie Heitmeyer (NRL), Mike Hinchey (NASA), Gerard Holzmann (JPL), Alan Hu (British Columbia), Hardi Hungar (Oldenburg), Bart Jacobs (Nijmegen), Cliff Jones (Newcastle), Joe Kiniry (UCD), Daniel Kroening (ETHZ), Mark Lawford (McMaster), Gary Leavens (Iowa), Rustan Leino (Microsoft), Xavier Leroy (INRIA), Karl Levitt (UCDavis), Peter Lindsay (Queensland), Zhiming Liu (Macau), Rupak Majumdar (UCLA), Pete Manolios (GATech), Tiziana Margaria (Potsdam), Brad Martin (Kestrel), Bertrand Meyer (ETHZ), Paul Miner (NASA), J Moore (Texas), Greg Morrissett (Harvard), Peter Mueller (ETHZ), Markus Muller-Olm (Dortmund), Cesar Munoz (NASA), Dave Musser (Rensselaer), Dave Naumann (Stevens), George Necula (Berkeley), Tobias Nipkow (Munich), Colin O'Halloran (QinetiQ), Peter O'Hearn (Queen Mary), Richard Paige (York), Paritosh Pandya (TIFR), Wolfgang Paul (Saarbrucken), Alexandre Petrenko (Riga), Lee Pike (Galois Connections), Amir Pnueli (Weizmann), Alexander Pretschner (ETHZ), Sriram Rajamani (Microsoft), Silvio Ranise (LORIA), Mike Reed (Macau), Jakob Rehof (Microsoft), Tom Reps (Wisconsin), Grigore Rosu (Illinois), John Rushby (SRI), Vlad Rusu (INRIA), Augusto Sampaio (UFPE), Steve Schneider (Surrey), Carsten Schuermann (Copenhagen), Wolfram Schulte (Microsoft), Sanjit Seshia (Berkeley), Peter Sestoft (Copenhagen), N. Shankar (SRI), Natasha Sharygina (CMU), Ofer Shtrichman (Technion), Joseph Sifakis (CNRS), Eli Singerman (SRI), Henny Sipma (Stanford), Mary Lou Soffa (Virginia), Bernhard Steffen (Dortmund), Mark-Oliver Stehr (SRI), Scott Stoller (New York), Aaron Stump (Washington), Cesare Tinelli (Iowa), Mark Utting (Waikato), Ralph Wachter (ONR), Virginie Wiels (CERT), Jim Woodcock (York), Joakim von Wright (Turku), Steve Zdancewic (Penn), Jian Zhang.

Invite these people to participate in the VSR report with specific responsibilities.

Content

• Tools
  • Integrated verification environments (e.g., Spec#, ESC/Java2)
  • Language front-ends
  • Static Analyzers
  • Test case generators
  • Theorem Provers
  • Model Checkers
  • Graphical User Interfaces
  • Program Synthesizers
  • Integrated Builds
• Benchmarks
• Case Studies
  • Mondex case study A research collaboration grew out of a comparison of Alloy, B, OCL, VDM, and Z in Daniel Jackson's book, using a hotel swipe-card system. Mondex is an electronic wallet; a sanitised specification and rigorous hand proof appears in Oxford PRG-126. See also The Mondex Workshop, the Perfect Developer version, and the Augsburg technical report.
  • Electronic voting
• Interoperability
  • Interchange formats, mappings between models, logics, glue code.
  • Models: state machines, automata, timed automata, hybrid automata, abstractions.
  • Language syntax and semantics: Logics, specification languages, programming languages.
  • Representations of proofs, test cases, counterexamples.
• Verified libraries: STL, openSSL, core Java, Bouncy castle, openPGP, glibc, GMP.
• Tutorials
• Advanced search capability
• Ontologies
• Keywords
• Forums
• Challenge problems: File synchronization, File system, web server, kernel, TCP/IP, SSL, compression, theorem prover kernel, cache consistency, separation kernel, compilers, virtual machines, build tools, fault-tolerant architectures, model reduction for hybrid systems, aspect extraction, scale/parametricity.
• Generic properties: Absence of runtime errors, data consistency, timing behavior, accuracy, type correctness, termination, translation validation, serializability, memory leaks, information hiding, representation independence, information flow.

Planning and Road Map

• Years 1 to 5: Benchmarking, static analysis, and specifications. Individual tool development with opportunistic integration. Small properties of big systems and big properties of small system. Logics for heaps, security, resources, modularity, weak memory models. Multiple code views. Engagement with early adopters.
  • Year 1: One paradigmatic example of code from specs, assertions from code, assertions from test, verification condition generation, and theorem proving. Initial case studies. User community.
• Years 5 to 10: Integrated tool development, medium-scale/medium-degree verification, loosely coupled to tightly coupled integration, workflows involving multiple tools. Engagement with industry.
• Years 10 to 15: Large-scale applications, tool validation, embedded verification, novel models of programming. Developing a broad user base.