News for hackers. Stuff that matters.

A comment on Software Verification and Analysis Using Z3. Parent comment

Re:Software Verification and Analysis Using Z3 by 1337_d00dZ on Saturday January 30, 2021 @07:15PM (#25974401)
Do the opposite: generate the program from the model
[ Parent | on HN ]
Re:Software Verification and Analysis Using Z3 by woodruffw on Saturday January 30, 2021 @07:20PM (#25974441)
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.

[ Parent | on HN ]