Automatic Verication of Programs with Indirection
Kyndylan Nienhuis
Abstract:
In the first part we prove the correctness of an existing verification
algorithm, namely counterexample-driven abstraction refinement. To be
able to state the correctness of the algorithm, we modify it such that
it verifies programs that have a formal semantics. We use
propositional dynamic logic and we give a denotational semantics and
an equivalent structural operational semantics.
Then we consider a deterministic fragment of propositional dynamic
logic. We improve the efficiency of the algorithm by exploiting
determinism when present and we prove that this algorithm terminates
on incorrect deterministic programs. Note that the algorithm will not
always terminate on correct deterministic programs, since verification
is undecidable in general.
Finally, we consider programs with indirection and we show that the
introduced algorithms verify these programs inefficiently. We propose
symbolic execution as an alternative way of computing path constraints
to circumvent this inefficiency. Furthermore, the variant of symbolic
execution we define removes indirection from symbolic terms which
enables us to use a theorem prover that does not handle indirection.