Model checking integrations with programming languages

With model checking integrations with programming languages, I mean the following things:

• model extraction from program
• program generation from model
• model checking of programs without creating model (like CBMC)

See also https://github.com/johnyf/tool_lists/blob/main/verification_synthesis.md

C/C++

Modex can be used to mechanically extract verification models from implementation level C code. The model extractor is guided by a user-defined test-harness, specified in a separate file with extension ".prx".

CBMC - is a Bounded Model Checker for C and C++ programs. It sup­ports C89, C99, most of C11/C17 and most compi­ler exten­sions pro­vided by gcc, clang, and Visual Studio.

ESBMC is an open-source, permissively licensed, context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs. It does not require the user to annotate the programs with pre- or postconditions, but allows the user to state additional properties using assert-statements, that are then checked as well. Furthermore, ESBMC provides two approaches (lazy and schedule recording) to model check multi-threaded programs. It converts the verification conditions using different background theories and passes them directly to an SMT solver.

Erlang

erlang-verifier - LTL model checking of Core-Erlang using term rewriting techniques.

Go

Goose is a subset of Go equipped with a semantics in Coq, as well as a translator to automatically convert Go programs written in Go to a model in Coq. The model plugs into Perennial for carrying out verification of concurrent storage systems.

PGo is a source to source compiler that translates Modular PlusCal specifications (which use a superset of PlusCal) into Go programs.

Gomela - tool developed for "Bounded verification of message passing concurrency in Go programs".

Gomela-ase21 - the tool-chain implemented as part of paper "Automated Verification of Go Programs via Bounded Model Checking".

Lua

BMCLua extends the features of ESBMC, which is a context-bounded model checker for embedded C/C++ software, for the Lua programming language. The ESBMC tool implements Bounded Model Checking (BMC) and k-induction techniques based on Satisfiability Modulo Theories (SMT) solvers. See "BMCLua: Verification of Lua Programs in Digital TV Interactive Applications" -- Francisco A. Januario, Lucas C. Cordeiro, Vicente F. Lucena Jr., and Eddie B. de Lima Filho".

ESBMC?

Ocaml

coq-of-ocaml aims to enable formal verification of OCaml programs unicorn. The more you prove, the happier you are. By transforming OCaml code into similar Coq programs, it is possible to prove arbitrarily complex properties using the existing power of Coq. The sweet spot of coq-of-ocaml is purely functional and monadic programs. Side-effects outside of a monad, like references, and advanced features like object-oriented programming, may never be supported. By sticking to the supported subset of OCaml, you should be able to import millions of lines of code to Coq and write proofs at large. Running coq-of-ocaml after each code change, you can make sure that your proofs are still valid. The generated Coq code is designed to be stable, with no generated variable names for example. We recommend organizing your proof files as you would organize your unit-test files.

Python

pyModelChecking - is a small Python model checking package. Currently, it is able to represent Kripke structures, CTL, LTL, and CTL* formulas, and it provides model checking methods for LTL, CTL, and CTL*. In future, it will hopefully support symbolic model checking. Documentation.

Deal: Deal has a built-in formal verifier. That means, deal turns your code into a formal theorem and then proves that it is formally correct (or finds a counter-example when it is not). Turning wild Python code into mathematical expressions is hard, so application of the verifier is limited. Still, you should try it. It will work for only 1% of your code, but when it does work, it finds actual bugs.

ESBMC

Verilog

hw-cbmc is a bounded model checker for the Verilog language (and other HW specification languages). The verification is performed by synthesizing a transition system from the Verilog, unwinding the loops (up to a certain bound), and then producing a SAT formula. The formula encodes the circuit and the negation of the property under verification.

Java

JCBMC is a Bounded Model Checker for Java programs. It checks runtime exceptions and user-definded assertions. The verification is performed by unwinding the loops in the program and passing the resulting formula to a decision procedure.