3 ms·

Correctness on iterative and recursive processes

• nickpsecurity 9y ago
  Have you tried SPARK Ada? It was first to be designed to automate proofs of common attributes such as immunity to lots of code injections or crashes that happen in C. They have both automated and interactive proving for other conditions you put in as preconditions, invariants, and postconditions. Need more people building reusable specs and code in such languages. Others from Microsoft are VCC compiler and Dafny language. From CompSci, Frama-C and Jave Modeling Language.
  • bor0 9y ago
    Not really. I've only done some Haskell and finishing "How to prove it". Doing proofs for hobby but I'll check those tools. Thanks!
    • nickpsecurity 9y ago
      If you do functional, check out Certified Programmjng with Dependent Types by Chlipala, Programming with Proofs by same, and Concrete Semantics. For tooling, QuickCheck and QuickSpec are interesting.