Our great sponsors
-
There are few tools that are both geared to mainstream programming languages and reasonable to work with. But probably the best place to start is Infer [1]. It's marketed as a static analyzer, in other words a way to prove some properties, but the separation logic at its heart is a powerful and general program proof technique.
In time, I hope and expect that the RustBelt project[2] will become a practical tool to prove Rust programs correct. It's already found some bugs in the standard library, and the main focus is currently to firm up the semantics of the language.
[1]: https://fbinfer.com/
NOTE:
The number of mentions on this list indicates mentions on common posts plus user suggested alternatives.
Hence, a higher number means a more popular project.
Related posts
- How to use Coq and C in practical software development for "verified C"?
- How to make develop C application easier?
- Meta Open-Sources A Compositional Deadlock Detector for Android Java
- infer - A static analyzer for Java, C, C++, and Objective-C open-sourced by Facebook
- infer - A static analyzer for Java, C, C++, and Objective-C open-sourced by Facebook