AUTOMATIC VERIFICATION OF POINTER-PROGRAMS USING MONADIC 2ND-ORDER LOGIC

We present a technique far automatic verification of pointer programs based an a decision procedure for the monadic second-order logic on fi nite 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 predica tes such as pointer equality, tests far nil pointers, and garbage cell s, as well as reachability along pointers. We present a complete decis ion procedure for Hoare triples based on this logic over loop-free cod e. combined with explicit loop in variants, the decision procedure all ows us to answer surprisingly detailed questions about small but non-t rivial programs. II a program fails to satisfy a certain property, the n we can automatically supply can initial store that provides a counte rexample. Our technique has been fully and efficiently implemented far linear linked fists, and it extends in principle to tree structures,T he resulting system can be used to verify extensive properties gf smal ler pointer programs and could be particularly useful in a teaching en vironment.