Can you overload if-else-blocks? (for bounded model checking)

General Usage
1

Recently we had a really hard-to-debug error in our code, so I was thinking about doing formal verification - especially bounded model checking - for julia.

I thought that translating a piece of Julia code to an equivalent SMT formula, could work about the same way as forward autodiff:

  • have a custom type for the input variables (just like ForwardDiff.Dual)
  • overload the functions inside to produce an SMT encoding (instead of a derivative)

However, I don’t know if this approach will be able to handle if-elseif-else statements.
Are these statements just functions (since they return a value) that I can overload?
And if so, how can I overload them?

1 Like
2

No they can’t be since function evaluate their arguments before they are called.

For true formal verification you likely need to work on the IR level, i.e. write a custom interpreter of sorts. IIRC, the topic arose on this forum before but I can’t find a good thread.

In the meantime you can try Supposition.jl by @Sukera which maybe gets you close enough to what you want :slight_smile: See also the announcement of Supposition.jl for a brief discussion about formal verification.
Anyways @Sukera is probably one of the best folks around here to discuss formal verification

1 Like
3

Your intuition is pretty much on point from my POV, and you’ve also hit the same problem that people in the AD world encounter: branches mess up everything.

Basically, no, you can’t overload if from inside julia, since it’s not a function. See also this previous discussion about much the same topic.

That being said, you could theoretically build an interpreter of julia IR using the abstract interpretation framework, which ends up emitting not llvm IR, but SMT statements that you’d then feed to an existing solver like z3 or the like (or maybe some other solver, depending in what exactly you’re interested in).

Practically speaking though, this is still super difficult. The abstract interpreter interface is sparsely documented at best, and translating things like x::Foo = ... into an SMT clause is challenging, not to mention then actually proving useful properties. Specifications unfortunately don’t compose and even if they would do that cleanly, it’s still super difficult (if you only read one of these links, read this one) and complex to prove even comparatively simple things.

2 Likes