Formal Verification Tool Competitions | Hacker News Reader

Formal Verification Tool Competitions

alastairreid.github.io

67 pointsmatt_d12 comments

It'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.

A 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.

The 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.

Uh, tons of modern verifable languages exist. See idris or f* for example.

They are actually quite good.

Uh, he was saying they should be used in this instead of C.

Termination 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?

There 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

Thanks 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).

You'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.

They 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.

Not 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).

Do they know beforehand a value of N so that the proofs have depth < N?

Reply on news.ycombinator.com