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.