You Don't Know Jack About Formal Verification

Re:You Don't Know Jack About Formal Verification by teach on Tuesday June 30, 2026 @12:54PM (#48735548)

I'm quite certain I formally verified that two processes were both able to get into the critical section WITH THE ALGORITHM I WAS VERIFYING, but this was 35 years ago, so details are fuzzy.

Remember that this is long before Wikipedia and even before Google, so I have no idea where I'd have gotten the alleged Baker's algorithm from.

Also you're right that this isn't much of an issue in practice, but that's not what formal verification is about, now is it? :)

[ Parent | on HN ]

Re:You Don't Know Jack About Formal Verification by codebje on Wednesday July 01, 2026 @07:05PM (#48754303)

Formal verification should definitely be about the software you're verifying exhibiting the properties you desire under the conditions you specify.

Formal verification at the undergraduate level, if you even see it, would be about running software on a spherical cow, though.

[ Parent | on HN ]