formal-verification.md

Bookmarks tagged [formal-verification]

^{www.codever.land/bookmarks/t/formal-verification}

CATG

^{https://github.com/ksen007/janala2}

Concolic unit testing engine. Automatically generates unit tests using formal methods.

• tags: java, formal-verification
• source code

---

Checker Framework

^{https://types.cs.washington.edu/checker-framework}

Pluggable type systems. Includes nullness types, physical units, immutability types and more.

• tags: java, formal-verification

---

Daikon

^{https://plse.cs.washington.edu/daikon}

Detects likely program invariants and generates JML specs based on those invariants.

• tags: java, formal-verification

---

Java Path Finder (JPF)

^JPF

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

• tags: java, formal-verification

---

JMLOK 2.0

^{http://massoni.computacao.ufcg.edu.br/home/jmlok}

Detects inconsistencies between code and JML specification through feedback-directed random tests generation, and suggests a likely cause for each nonconformance detected.

• tags: java, formal-verification

---

KeY

^{https://key-project.org}

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

• tags: java, formal-verification

---

OpenJML

^{https://openjml.github.io}

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

• tags: java, formal-verification

---