Abstract
We present our ongoing effort to implement predicate abstraction in Abstract Pathfinder, which is an extension of Java Pathfinder. Our approach builds upon existing abstraction techniques that have been proposed mainly for low-level programs in C. We support predicates over variables having numerical data types. The main challenges that we have addressed include (1) the design of the predicate language, (2) support for arrays, (3) finding predicates affected by a given statement, (4) aliasing between variables, (5) propagating values of predicates over method call boundaries, and (6) computing weakest preconditions for complex predicates. We describe our solution to these challenges and selected details about the implementation. We also discuss our future plans and research ideas.