GDPA  
Index for tools/publications on formal methods  

Development Phases: Verification

Contents  
  • Publications
  • Projects/Tools
  • See also
  • Publications

    1999:
    /Braberman, 1999/ Verification of Real Time Designs: Combining Scheduling Theory with Automatic Formal Verification
    /Penix, 2000/ Verification of Time Partitioning in the DEOS Scheduler Kernel

    1998:
    /Fong, 1998/ Proof Linking: An Architecture for Modular Verification of Dynamically-Linked Mobile Code

    1990:
    /Kersten, 1990/ Sichere Software (Formale Spezifikation und Verifikation vertrauenswürdiger Systeme)

    1987:
    /Loeckx, 1987/ The Foundation of Program Verification

    1982:
    /Deutsch, 1982/ Software Verification and Validation

    1976:
    /Reynolds, 1976/ Induction as the Basis for Program Verification

    1977:
    /Yeh, 1977/ Verification of Programs by Predicate Transformation

    Projects/Tools

    ACL2 - A Computational Logic for Applicative Common Lisp
    Argos
    BDD - Binary Decision Diagrams
    CIRCAL - CIRcuit CALculus
    VERSA - Verification Execution and Rewrite System for ACSR
    FormalCheck
    Kronos - verification tool
    LUSTRE - language for programming reactive systems
    Meije - verification of concurrent programs
    Model checking
    Murphi - description language and verifier tool
    PARAGON - visual specification and verification of real-time systems
    PVS - Prototype Verification System
    SGM - State Graph Manipulator
    SPARK - secure subset of Ada
    SPIN - is an automated verification tool
    UPPAAL - verification and validation tools for real-time systems
    VIS - Verification Interacting with Synthesis

    See also

    Index for tools/publications on formal methods

    GDPA Online Last Updated 01.Jan.2002 Updated by Webmaster Last Revised 01.Jan.2002 Revised by Webmaster