The goal of this project is to design practical verification techniques for multi-threaded programs based on specific combinations of static and dynamic analyses. We implement all proposed techniques using WALA and Java Pathfinder, and evaluate them on Java bytecode programs.
Related Publications
- P. Parízek and O. Lhoták. Identifying Future Field Accesses in Exhaustive State Space Traversal. ASE 2011, IEEE CS
- P. Parízek and P. Jančík. Approximating Happens-Before Order: Interplay between Static Analysis and State Space Traversal. SPIN 2014, ACM
- P. Parízek and O. Lhoták. Model Checking of Concurrent Programs with Static Analysis of Field Accesses. Science of Computer Programming, vol. 98, part 4, Elsevier, 2015
- P. Parízek. Hybrid Analysis for Partial Order Reduction of Programs with Arrays. VMCAI 2016, LNCS, vol. 9583
- P. Parízek. Fast Error Detection with Hybrid Analyses of Future Accesses. SAC 2016, MUSEPAT track, ACM