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)
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".
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.
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".
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.
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.
Learning
- Glossary
- Books:
- Courses
- Learning Tools
- Bugs And Learned Lessons
- Cheatsheets
Tools / Services / Tests
- Code complexity
- Quality Assurance Tools
- Test Runners
- Testing-As-A-Service
- Conformance Test Suites
- Test Infrastructure
- Fault injection
- TTCN-3
- Continuous Integration
- Speedup your CI
- Performance
- Formal Specification
- Toy Projects
- Test Impact Analysis
- Formats
Functional testing
- Automated testing
- By type:
WIP sections
Community
Links