Workshop on Linking Tools for Verified Software


Venue: Microsoft Research Cambridge
Dates: November 27-28, 2008
Organisers: Jim Woodcock, Mike Gordon, Tony Hoare

Goals

Talks

 Peter O'Hearn                             Some things that (London) automatic verification can and can't do
 Georges Gonthier                          Lessons from Coq
 John Rushby                               PVS, SAL, and the ToolBus
 Tom Melham                                HOL, Forte, Prosper, and beyond
 Colin O'Halloran                          Challenges from Qinetiq
 Michał Moskal                             Verifying Concurrent C programs using VCC, Boogie and Z3
 Michael Butler                            Design and verification using Rodin
 Richard Banach                            Model Based Refinement Tools in General and Frog in Particular
 Tony Hoare                                Survey of some tools being implemented and used within Microsoft
 Daniel Kroening                           Automated theorem proving in program analysis
 Matt Kaufmann                             Verifying LabVIEW Graphical Programs with ACL2
 Rob Arthan                                Linking ProofPower to Simulink
 Daniel Kroening                           Discussions on new research and collaboration

Posters

 Yichi Zhang, Leo Freitas, Jim Woodcock    Verifying the CICS File Control API with Z/Eves
 Paul B. Jackson, Grant Olney Passmore     Improved Automation for SPARK Verification Conditions
 Grant Olney Passmore, Paul B. Jackson     RAHD: Real Algebra in High Dimensions
 Mike Dodds                                Deny-Guarantee Reasoning
 Peter Sewell + 5 others                   Ott: Effective Tool Support for the Working Semanticist
 Scott Owens                               OCamllight in Ott
 Magnus Myreen                             Proof-Producing Decompilation
 Thomas Tuerk                              A Heap of Problems  A Separation Logic Framework in HOL
 Frank Theiß                               Leo-II A Higher-Order Theorem Prover
 Rod Chapman                               Tokeneer
 Alfredo Pironti                           Spi2Java: From Security Protocol Models To Java Application Generation

Continuing discussion

Session 4 of the workshop was a discussion chaired by Daniel Kroening.
Notes on this were taken by Matt Kaufmann.

The discussion now continues online at http://verifiedsoftware.wordpress.com.
Everyone is encouraged to contribute! Posts so far include:

 A Heap of Problems
 Translating pointer code to functional programs

List of participants


Maintained by Mike Gordon.
Last updated: Mon Feb 2, 2009