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
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
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