Automatic verification of pointer programs using monadic second-order logic

We present a technique far automatic verification of pointer programs based an a decision procedure for the monadic second-order logic on finite strings, We are concerned with a while-fragment of Pascal, which includes; recursively-defined painter structures but excludes pointer arithmetic. We define a logic of stores with interesting basic predicates such as pointer equality, tests far nil pointers, and garbage cells, as well as reachability along pointers. We present a complete decision procedure for Hoare triples based on this logic over loop-free code. combined with explicit loop in variants, the decision procedure allows us to answer surprisingly detailed questions about small but non-trivial programs. II a program fails to satisfy a certain property, then we can automatically supply can initial store that provides a counterexample. Our technique has been fully and efficiently implemented far linear linked fists, and it extends in principle to tree structures,The resulting system can be used to verify extensive properties gf smaller pointer programs and could be particularly useful in a teaching environment.