Re:Proofs and Refutations Using Z3
by nickpsecurity on Thursday February 15, 2018 @04:13PM
(#16387681)
I said that about TLA+'s model checking. With things like Verasco, I figured a verified model checker could be done. As usual, I also searched for examples with SPIN since (a) they're used for similar things and (b) more people used SPIN in the past. Found this:
Lammich was a name I recognized immediately for his work converting functional data structures to imperative ones in Isabelle/HOL. He and his collaborators have done quite a few interesting things so I'll just leave you the whole list:
Far as lightweight methods, I recently summarized some recommendations with supporting case studies on Schneier's blog based on a message I sent someone trying to sell management on verification. It's a draft that I'm getting feedback on from various people rather than something I'm 100% solid on. The SPARK work combined with their book is still one of easiest methods in terms of automation achieved for covering specific properties that are often significant.
https://www21.in.tum.de/~lammich/pub/nfm2016_por.pdf
Lammich was a name I recognized immediately for his work converting functional data structures to imperative ones in Isabelle/HOL. He and his collaborators have done quite a few interesting things so I'll just leave you the whole list:
https://www21.in.tum.de/~lammich/
Far as lightweight methods, I recently summarized some recommendations with supporting case studies on Schneier's blog based on a message I sent someone trying to sell management on verification. It's a draft that I'm getting feedback on from various people rather than something I'm 100% solid on. The SPARK work combined with their book is still one of easiest methods in terms of automation achieved for covering specific properties that are often significant.
https://www.schneier.com/blog/archives/2018/02/friday_squid_...