{"id":16558,"date":"2021-09-16T15:38:08","date_gmt":"2021-09-16T19:38:08","guid":{"rendered":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/?p=16558"},"modified":"2026-03-27T08:47:15","modified_gmt":"2026-03-27T12:47:15","slug":"how-can-you-say-that-formal-verification-is-exhaustive","status":"publish","type":"post","link":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/2021\/09\/16\/how-can-you-say-that-formal-verification-is-exhaustive\/","title":{"rendered":"How Can You Say That Formal Verification Is Exhaustive?"},"content":{"rendered":"\n

As a companion to my previous post on Learn Formal the Easy Wa<\/em>y<\/a>, allow me to explain what are often the most perplexing \u2013 yet fundamental \u2013 aspects of formal analysis: formal results are good for all time, and all inputs \u2013 i.e. formal verification is exhaustive.<\/strong><\/p>\n\n\n\n

I grant that this sounds like a wildly exaggerated claim for any technology \u2013 indeed, over the years several new-to-formal customers have, um, enthusiastically shared their skepticism about this with me. However, this claim can be clearly proven (formal pun intended); but the problem is that the official academic proof can take several graduate-level lectures and math that (if you\u2019re like me) will leave you speechless and more confused than before. Fortunately, (to the chagrin of my PhD colleagues), I\u2019ve discovered an overly simplified analogy to explain how formal is exhaustive: finding solutions to the quadratic equation:<\/p>\n\n\n\n

ax2<\/sup> + bx + c = 0<\/strong><\/p>\n\n\n\n

Recall from your school days that in the above equation \u201ca\u201d, \u201cb\u201d, and \u201cc\u201d are constants, and the goal is to solve for the value(s) of variable \u201cx\u201d.<\/p>\n\n\n\n

Here is where the analogy comes in:<\/p>\n\n\n\n