81–82 of 82 posts
Rules like avoiding recursion and loop upper bounds are partly justified by helping code analyzers to prove executions are bounded. Does anyone have experience performing formal static analysis on code? And if so, are there any open-source examples of the state-of-the-art tools being used on nontrivial problems? I've been looking at this recently, but I've never seen a proof of reasonably standard function like, say,…
Rules like avoiding recursion and loop upper bounds are partly justified by helping code analyzers to prove executions are bounded. Does anyone have experience performing formal static analysis on code? And if so, are there any open-source examples of the state-of-the-art tools being used on nontrivial problems? I've been looking at this recently, but I've never seen a proof of reasonably standard function like, say,…
Take a look at dafny [1] and F* [2]. Both are open-source and it appears that both of them are able to prove code to be correct with considerably less proof code than traditional interactive theorem provers (such as Coq or Isabelle), mostly thanks to the use of an SMT solver (Z3, in both cases) to aid in proving. Both languages are being used in Project Everest [3], which is building a formally verified HTTPS stack,…