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

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.

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

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.

Verilog

EBMC 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. Hence if satisfiable, the tool produces a counterexample demonstrating violation of the property. EBMC employs CBMC for the last two steps of the above described verification chain, i.e. SAT encoding and satisfiability checking.