Jakub Daniel
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.
- S. Anand, C.S. Pasareanu, and W. Visser. Symbolic Execution with Abstraction. Journal of Software Tools for Technology Transfer, 11(1), 2009. Google Scholar
Digital Library
- T. Ball, R. Majumdar, T. Millstein, and S.K. Rajamani. Automatic Predicate Abstraction of C Programs. In Proceedings of PLDI 2001, ACM. Google ScholarDigital Library
- D. Beyer, T.A. Henzinger, R. Jhala, and R. Majumdar. The Software Model Checker BLAST: Applications to Software Engineering, Journal of Software Tools for Technology Transfer, 9(5--6), 2007. Google ScholarDigital Library
- E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-Guided Abstraction Refinement. In Proceedings of CAV 2000, LNCS, vol. 1855. Google ScholarDigital Library
- S. Graf and H. Saidi. Construction of Abstract State Graphs with PVS. In Proceedings of CAV 1997, LNCS, vol. 1254. Google ScholarDigital Library
- G.J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering, 23(5), 1997. Google ScholarDigital Library
- Java Pathfinder: framework for verification of Java programs. http://babelfish.arc.nasa.gov/trac/jpf/.Google Scholar
- A. Khyzha, P. Parizek, and C.S. Pasareanu. Abstract Pathfinder. ACM SIGSOFT Software Engineering Notes, 37(6), 2012. Google ScholarDigital Library
- C.S. Pasareanu and N. Rungta. Symbolic PathFinder: Symbolic Execution of Java Bytecode. In Proceedings of ASE 2010, ACM. Google ScholarDigital Library
Index Terms
- Predicate abstraction in Java Pathfinder
Recommendations
Abstract pathfinder
We present Abstract Pathfinder, an extension to the Java Pathfinder (JPF) verification tool-set that supports data abstraction to reduce the large data domains of a Java program to small, finite abstract domains, making the program more amenable to ...
Combining Theorem Proving with Model Checking through Predicate Abstraction
This article presents a procedure for proving invariants of infinite-state reactive systems using a combination of two formal verification techniques: theorem proving and model checking. This method uses term rewriting on the definition of the target ...
Predicate abstraction and CEGAR for higher-order model checking
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and ImplementationHigher-order model checking (more precisely, the model checking of higher-order recursion schemes) has been extensively studied recently, which can automatically decide properties of programs written in the simply-typed λ-calculus with recursion and ...
Comments