Analysis tools logo
0

VeriFast

A tool for modular formal verification of correctness properties of single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic. To express rich specifications, the programmer can define inductive datatypes, primitive recursive pure functions over these datatypes, and abstract separation logic predicates.

Github:
    24124171562013
Workflow integration:
  • Type: cli
    cli

Official VeriFast Homepage

https://github.com/verifast/verifast

MIT License

Maintained

Alternative Tools

  • 61Semgrep
  • 0Sys