Program Verification Using Traps

In this chapter, a verification method based both on linear algebra and on traps in the sense of the previous chapters is presented. It is fast, useful for a sizeable class of systems, and applicable to computer programs via a translation into Petri nets. Similar to testing, the technique is semi-exact. In contrast to testing, it is based on overapproximating, rather than underapproximating, the state space of a system.