5 ms·
Formal Verification Tool Competitions
- zomglings 7y agoTermination competitions seem fascinating. Are they restricted to certain subclasses of programs where the Halting Problem is solvable? Or are they more focused on bounded termination - Will this general program terminate in at most N steps? Are there techniques that help answer this question in compressed time?
- veselin 7y agoThey overapproximate. This means that may say something probably doesn't terminate even if it terminates. The idea is that if it says it terminates, then there is a proof it does.
- zomglings 7y agoDo they know beforehand a value of N so that the proofs have depth < N?
- lou1306 7y agoNot necessarily. For instance, CBMC has been participating in the Termination category with an approach based on Bounded model checking, an underapproximation technique. Thus, they always produce correct result, but their analysis might not terminate (or may terminate with an "unknown" verdict).
- lou1306 7y agoThere is no general algorithm to determine termination. You can still write an algorithm that gives correct answers, but may not terminate (sound), or one that always terminates but might produce wrong answers (complete). A termination analyzer for, say, C programs is either one of the other. Anyway, SV-COMP's benchmarks are all available at [1]: Termination benchmarks are within the eponymous directories, so feel free to take a look! [1] https://github.com/sosy-lab/sv-benchmarks/tree/master/c https://github.com/sosy-lab/sv-benchmarks/tree/master/c
- zomglings 7y agoThanks for the link (looking at it now), and for the terminology (sound, complete). The trivial algorithm to determine termination is to just run the code. This algorithm is sound but not complete, and is not interesting from the point of view of a termination competition. Very curious about complete but unsound approaches. First instinct is to just determine some rules that allow you to prune paths in the control flow of a program (e.g. prune away bounded loops). This doesn't help with recursion, though. If we were dealing with recursive functions with constrained argument types, I can see rules like "for two calls, integer argument is moving closer to base case" being effective. Generalizing this still feels like it would be magical to me (which means I don't understand it at all).
- lou1306 7y agoYou're welcome. It's always nice to see HN talk about program verification! > Very curious about complete but unsound approaches A common approach is over-approximation, i.e. you create a model of the program whose set of traces is a superset of the actual traces. If that model is terminating, then the program also is. Otherwise, you cannot draw any conclusion (as the non-terminating traces in the model might be spurious). Some examples of over-approximating techniques are abstract interpretation and predicate abstraction.
- mpoteat 7y agoIt's kind of a shame that this subset of research is kind of stuck on C as a standard. I feel like higher abstraction languages would potentially be easier to reason about, as well as personally more useful to me. Sure I know C11 but it's just not a tool that solves the problems I'm interested in.
- zbobet2012 7y agoUh, tons of modern verifable languages exist. See idris or f* for example. They are actually quite good.
- GeorgeWBasic 7y agoUh, he was saying they should be used in this instead of C.
- adrianN 7y agoA lot of embedded code is written in C. A lot of safety critical code is embedded code. This is unlikely to change in the next decade or two.
- irundebian 7y agoThe problem is that in safety critical contexts you are using special subsets of C (e. g. like in MISRA C). I would probably make more sense to analyze languages like Ada/SPARK or Rust which already have some safety considerations respected in their designs.