Simple Software Verification, Part 3: Karnaugh Maps
home // page // verification
s
Ben Laposky, Oscilon
Technical Tips

Simple Software Verification, Part 3: Karnaugh Maps

(Image by Ben Laposky) Series Parts Part 1 – Execution Tables Part 2 – Trace Tables Part 3 – Karnaugh Maps Welcome to the third and final article in this mini-series on software validation. In this article we’re going to discuss state machines, what desirable properties they should possess, and then I’ll demonstrate a simple tool for verifying them called Karnaugh Maps. Identifying State Machines As a general rule of thumb, you can identify a program that is a potential…

Technical Tips

Simple Software Verification, Part 2: Trace Tables

(Image by Leonardo Solaas) Series Parts Part 1 – Execution Tables Part 2 – Trace Tables Part 3 – Karnaugh Maps Welcome back! In the previous article I explained why you might be interested in software verification techniques and then showed you how to use Execution Tables to verify your software for specific cases. In this article, we’ll generalize Execution Tables into a format that will allows us to create simple inductive proofs about our loops. Trace Tables To demonstrate this…

Technical Tips

Simple Software Verification, Part 1: Execution Tables

Series Parts Part 1 – Execution Tables Part 2 – Trace Tables Part 3 – Karnaugh Maps (Image by Manfred Mohr) Introduction If you’re a software developer, and you work somewhere even remotely sane, then chances are good you employ some form of automated testing in your day-to-day practice. Automated testing is a wonderful and extremely valuable tool, but there is nevertheless something slightly fanatical and suspicious about the claims of those who prescribe it as the strategy for managing software quality. Namely, experience teaches us that…