Ask HN: How to start with formal verification to find bugs | Hacker News Reader

Ask HN: How to start with formal verification to find bugs

16 pointstomas7899 comments

We have a large codebase of a mostly functional code. Most of the code looks roughly like this

  def CalculateX(entity1: Type1, entity2: Type2):
    when:
    | entity1 is big -> 5
    | entity1 is not big -> 6
    | entity2 is round and entity1 purple -> 5

The conditions in the pattern matching block can get quite complex. The function might be defined for all instances if Type1 and Type2 but that is not required. Reasoning about a single function is reasonably easy. But we often find a bug where a function should be defined for all combinations of its input parameters but it is calling a function which is not defined for a requested case.

We do all kinds of things to ensure it is reasonably correct but it seems like it is never enough. We are toying around with an idea of formal verification of our code. I don't know from which angle to attack this issue first. I was playing with Z3 and Coq but they are like a distinct system. What is a typical workflow of how to verify a program? Do we have to rewrite it first in a formal verification system or is it possible to use some sort of source-to-source translation? Is there a way to make sure this translation is correct? How do I find a system that will be up for the task? How do I know it is computationally tractable?

I think you’re looking at a program verification problem.

With this tool: http://viper.ethz.ch/ You essentially sprinkle your functions with pre- and post conditions (& loops), press „verify“ and it will verify the correctness of your program code.

There are multiple frontends you can use for different languages. Behind the scenes your code + annotations are converted from e.g. Python/Rust/Go to an intermediate language (Viper), which is then verified.

Isn't this just an extension of design by contract? What advantages come from using a framework like this instead of traditional assertions for contracts?

It is indeed just an extension of that very idea, developed at the same institution where design-by-contract has been introduced a few decades ago.

However, instead of crashing at runtime due to a failed assertion, you get a guarantee that your program will in fact not violate said assertions and behave correctly.

It also entails a nice speed bonus, instead of checking the assertions all the time, which could be quite a complex feat for non-trivial post-conditions, you do it once, symbolically, for all possible executions.

Didn't know about this; looks interesting. Thanks for the pointer.

> What is a typical workflow of how to verify a program?

If you mean an existing program, it is usually not done that way. Instead, you develop the program and the proofs at the same time, so they go hand and hand with each other.

If you just mean checking exhaustiveness of a case statement, compilers can often do that for you.

Which programming language are you using? It looks to me like you need exhaustiveness checking for pattern matching. Languages like Scala, OCaml, Purescript or Haskell support this out of the box.

Am I overlooking something?

I think OP wants transitive exhaustiveness checks while supporting partial base functions.

My suggestion:

Must you have partial functions? Maybe you can model your data more tightly? If your conditions are too complex, maybe you could decompose them?

A big reason I like ADTs with concise syntax is to model data with nearly¹ no room for invalid or useless data. Then all¹ functions are total and matches are checked for exhaustiveness. A nice matching syntax on top makes mistakes easy to spot.

Not sure how to help with formal verification or exhaustiveness on partial functions.

¹ I don't model everything absolutely precisely, but deviations are more of an exception rather than the rule. Then they can be made apparent and reasoned about.

I have a list of entities. The entities are partitioned by different properties (like color, speed and so on, partitions usualy cover the whole list but not always). Compilers like Haskell and Fsharp can catch exhaustiveness over individual entities or each property individually. Problems arise when they are combined. For example first case covers red and blue entities, second case covers fast entities, thirs case explicitly covers entity 1 and 2. Now the question is whether this is exhaustive. Compiler of Fsharp just tells me it is not and one has to provide the otherwise case and do something there (raise exception, return none or something). But in this case the correctness is proven only during the execution. From the outside persons point of view this is the same behavior. The program has crashed.

I as a developer can go through the cases and reason that those cases are actually exhaustive and move on. Problem is that this is time consuming and one would need to check everything every time the partitionings change (which happens).

Are you using property-based testing tools like Quickcheck?

Some Youtube videos: https://www.youtube.com/results?search_query=property+based+...

Article by author of Hypothesis, the property-based testing framework for Python: https://increment.com/testing/in-praise-of-property-based-te...

Pycon talk on how Contracts + PET gets you integration tests: https://www.hillelwayne.com/talks/beyond-unit-tests/

An article from the property-based testing series on the blog F# for Fun and Profit: https://fsharpforfunandprofit.com/posts/property-based-testi...

Reply on news.ycombinator.com