Software Verification and Analysis Using Z3
research.nccgroup.com
Software Verification and Analysis Using Z3
1–10 of 43 posts
Re: Software Verification and Analysis Using Z3
#2This may be a dumb question, but how do I know that the model is accurate?
Re: Software Verification and Analysis Using Z3
#3Is there any introductory course for these kind of stuff?
Re: Software Verification and Analysis Using Z3
#4This may be a dumb question, but how do I know that the model is accurate?
[deleted]
Re: Software Verification and Analysis Using Z3
#5This may be a dumb question, but how do I know that the model is accurate?
Do the opposite: generate the program from the model
Re: Software Verification and Analysis Using Z3
#6This may be a dumb question, but how do I know that the model is accurate?
That's not a dumb question! The accuracy of one's underlying models is an outstanding problem in verification.
Re: Software Verification and Analysis Using Z3
#7This may be a dumb question, but how do I know that the model is accurate?
The age old problem of verification vs. validation. Verification is about whether or not you built something right. Validation is about whether or not you built the right thing. This article is about using Z3 to pursue the former, the latter is an entirely different issue.
Re: Software Verification and Analysis Using Z3
#8This may be a dumb question, but how do I know that the model is accurate?
Do the opposite: generate the program from the model
Which, in turn, requires trusting or proving the soundness of your program generator and only proves that your incorrect original program is exactly as incorrect as the model that verifies it.
Automating the stronger proof (that the model is exactly as correct as the original program, and that the model is correct) hasn't been solved in the general case, to the best of my knowledge.
Re: Software Verification and Analysis Using Z3
#9First time I see Z3 in the wild. Bonus points for the CLI friendly model checker, but lisp syntax... is less legible than TLA+ imho. Gotta give it a try someday to see for myself if the experience of creating the spec is better.