Overview

The charter for the Tools/Interoperability panel is to develop a road map for verification tools and formats for interoperability between these tools. Here are some of the tool classes (feel free to add/delete/edit/rearrange):

1. Specification languages and logics: These are used for capturing the requirements at a high level of abstraction. Examples of these include Z, VDM, PVS, B, ASM, etc. These need not be executable. Specification logics include various Hoare logics, temporal logics with real-time and hybrid extensions, process algebras, and automata.

1. Programming languages: The code that is claimed to be verified is captured in one of these executable languages. This code need not be directly verified but could be generated from some higher-level representation. Examples include C, C++, Java, Eiffel, Common Lisp, oCaml, Haskell, etc.
2. Assertion languages: Code verification requires assertions that are inserted at control points, and contracts that capture pre/post-condition claims at entry and exit points to procedures and methods. These assertions are typically in a side-effect free subset of the corresponding programming language, as illustrated by JML.
3. Parsers and syntax analyzers: These ensure that the input specifications, code, assertions, etc., are syntactically well-formed, and render the input into abstract syntax or an intermediate form that is amenable to analysis. The CIL format for C is an instance.
4. Semantic analyzers: The Verified Software project should use a range of automation from highly automated tools to carry out analyses that show the absence of common runtime errors and establish useful invariants and generate test cases, to semi-automated tools that check assertions, contracts, refinement, and specifications. The semantic analyzers here include type checkers, static and dynamic analyzers, and test case generators. These include ASTREE, WPDS, TVLA, CCured, Polyspace, and BANE.
5. Theorem provers: Deductive capabilities can be used to discharge the proof obligations that arise in semantic analysis and in the development of specifications and proofs, and in bounded model checking and test generation. Theorem proving support can range from highly efficient decision procedures to proof search tools and interactive proof checkers. Examples include decision procedures like CVC-Lite, ICS, Yices, UCLID, and Barcelogic, proof search procedures like Vampyre, E, Otter, Snark, and SATURATE, and interactive proof checkers like ACL2, HOL, HOL-Lite, Coq, Isabelle, and PVS.
6. Model checkers: Model checking used to analyze finite-state systems and their extensions for temporal properties and state equivalence. Examples include SPIN, SMV, nuSMV, SAL, Bandera, Cadena, Java Pathfinder, Blast, and CMC, and timed/hybrid model checkers like UPPAAL, Kronos, HyTech, and Chiron.
7. Code generators: These compile executable high-level specifications to running code in some programming language. Systems like Isabelle, HOL, ACL2, and PVS support such code generation. Various model checkers also support some degree of code generation. They also have the reverse capability so that they can convert low-level code into checkable models.
8. Implementation languages: Only a few languages are used in implementing analysis tools. These include C/C++, Java, Lisp, oCaml, Haskell, Prolog, and Twelf, and also scripting languages like Scheme, Python, and Ruby.
9. Libraries: These provide the most useful and flexible functionality for building useful formal applications. Libraries include BDD packages like CUDD, polyhedral and arithmetic manipulation packages such as Omega, linear programming packages, SAT solvers, and ASD+SDF.
10. Program synthesis frameworks: KIDS/Specware and other examples that target the interactive development of code by composing high-level descriptions.
11. Verification Environments: ESC/Java, ESC/Java2, Spec#, are examples of integrated verification environments for analyzing annotated code.

comments:

theorem provers --erniec, Tue, 28 Mar 2006 01:04:05 -0800 reply
I think you probably meant to list the prover Vampire (the Manchester resolution prover) rather than Vampyre (a Nelson-Oppen prover from one of Necula's classes). Why George couldn't choose another name for his prover is beyond me...

vampyre --rupak, Thu, 30 Mar 2006 21:18:19 -0800 reply
I am afraid I am to blame for the name. it was meant as a joke (vampyre was supposed to expand to "verifying and mechanically proving your ridiculous examples" as a dig to George's rather comprehensive test suite). at the time we did not know about the other vampire, which I am sure has a more dignified etymology. :)