Date Added: Nov 2009
Logics that involve collections (sets, multisets), and cardinality constraints are useful for reasoning about unbounded data structures and concurrent processes. To make such logics more useful in verification this paper extends them with the ability to compute direct and inverse relation and function images. The authors establish decidability and complexity bounds for the extended logics. Deductive verification of software often involves proving the validity of formulas in expressive logics. Verification condition generation produces such formulas directly from annotated source code, whereas predicate abstraction techniques generate many formulas during fixpoint computation.