Software Verification and Analysis Using Z3 • Hacker News Board

Re: Software Verification and Analysis Using Z3

#41

Post by the-smug-one » Sun, Jan 31, 2021, 11:58 AM UTC

iso8859-1 wrote: post #37

tromoi21 wrote: post #33

The author of Z3, Leo de Moura, released Lean 4 milestone 1 about 3 weeks ago: https://github.com/leanprover/lean4 Lean 4 is a functional programming language and theorem prover that compiles to C. A lot of research went into making Lean 4 blazingly fast https://leanprover.github.io/publications/ Galois inc reproduced benchmarks by the Lean 4 devs that show that Lean 4 regularly outperforms the C++ stdlib. This is an…

but how is Lean related to Z3? model checking and dependently typed programming are totally orthogonal, right?

I don't know about that. You can obviously use them for similar things. Namely, proving properties about your software.

Here's a good blog post talking about type theory vs logics: https://ucsd-progsys.github.io/liquidhaskell-blog/2019/10/20...

Re: Software Verification and Analysis Using Z3

#42

Post by the-smug-one » Sun, Jan 31, 2021, 12:05 PM UTC

nextos wrote: post #20

sempron64 wrote: post #11

Earlier quoted context omitted.

I’m just starting to investigate using formal analysis in practice and I think a much more practical topic is the symbolic execution frameworks which can analyze programs and feed them to theorem solvers like Z3. The most useful and accessible symbolic execution package I’ve found so far is KLEE https://klee.github.io/ If anyone else has recommendations for tools or beginner material I’m all ears!

There's some nice literature. I got into the field 15 years ago and there were practically no good textbooks. Things are way better now: https://avigad.github.io/formal_methods_in_education/ Nielson & Nielson have the standard textbook in static program analysis that is used everywhere. But it's quite unfriendly as it's written using abstract algebra. They've recently released two textbooks that are much gentler. Act…

>My dream is to implement some kind of framework that enables quick DSL creation along with lightweight formal methods support to verify programs written in each DSL.

There's work in this area using monads. Specifically, Darais (from Galois) et al show in "Abstracting Definitional Interpreters" how given a definitional interpreter you can easily create all sorts of abstractions using a stack of monad transformers. The best part of it all is that your particular chosen stack remains valid when moved between interpreters of different languages.

Your dream of varied static analysis can be achieved using monad transformers, definitional interpreters written in the required style, and Racket's DSL-creation system.

Re: Software Verification and Analysis Using Z3

#43

Post by nextos » Sun, Jan 31, 2021, 11:14 PM UTC

the-smug-one wrote: post #42

nextos wrote: post #20

Earlier quoted context omitted.

There's some nice literature. I got into the field 15 years ago and there were practically no good textbooks. Things are way better now: https://avigad.github.io/formal_methods_in_education/ Nielson & Nielson have the standard textbook in static program analysis that is used everywhere. But it's quite unfriendly as it's written using abstract algebra. They've recently released two textbooks that are much gentler. Act…

>My dream is to implement some kind of framework that enables quick DSL creation along with lightweight formal methods support to verify programs written in each DSL. There's work in this area using monads. Specifically, Darais (from Galois) et al show in "Abstracting Definitional Interpreters" how given a definitional interpreter you can easily create all sorts of abstractions using a stack of monad transformers. Th…

Thanks. I'm quite familiar with all the work from David Van Horn, including the paper you cited. I also think it's the way forward.