Selected Tags

Click on a tag to remove it

Formal Verification libraries

Showing projects tagged as Formal Verification

  • Checker Framework

    5.6 9.7 L1 Java
    Pluggable type systems. Includes nullness types, physical units, immutability types and more.

  • CATG

    3.0 0.0 L1 Java
    Concolic unit testing engine. Automatically generates unit tests using formal methods.

  • Daikon

    2.9 8.3 L1 C
    Daikon detects likely program invariants and can generate JML specs based on those invariats.

  • OpenJML

    2.9 7.7 L1 Java
    Translates JML specifications into SMT-LIB format and passes the proof problems implied by the program to backend solvers.

  • jCUTE

    2.8 0.0 L1 Java
    Concolic unit testing engine that automatically generates unit tests. Concolic execution combines randomized concrete execution with symbolic execution and automatic constraint solving.

  • JMLOK 2.0

    2.0 0.0 L2 Java
    Detects nonconformances between code and JML specification through the feedback-directed random tests generation, and suggests a likely cause for each nonconformance detected.

  • Java Path Finder (JPF)

    - -
    JVM formal verification tool containing a model checker and more. Created by NASA.

  • Krakatoa

    - -
    Krakatoa is a front-end of the Why platform for deductive program verification. Krakatoa deals with Java programs annotated in a variant of the Java Modeling Language (JML).

  • KeY

    - -
    The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. Uses JML for specification and symbolic execution for verification.

  • Java Modeling Language (JML)

    - -
    Behavioral interface specification language that can be used to specify the behavior of code modules. It combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus. Used by several other verification tools.