The pointer assertion logic engine

摘要: We present a new framework for verifying partial specifications of programs in order to catch type and memory errors check data structure invariants. Our technique can verify large class structures, namely all those that be expressed as graph types. Earlier versions were restricted simple special cases such lists or trees. Even so, our current implementation is fast the previous specialized tools.Programs are annotated with Pointer Assertion Logic, notation expressing properties program store. work logical tradition by encoding formulas monadic second-order logic. Validity these checked MONA tool, which also provide explicit counterexamples invalid formulas.To make verification decidable, requires loop function call In return, highly modular: every statement given analyzed only once.The main target applications safety-critical data-type algorithms, where cost annotating invariants justified value being able automatically complex program.