Research

The goal of my research is to develop methods and tools for practical program verification and debugging. I am especially interested in techniques that scale to large multi-threaded programs, detect bugs in real code efficiently, and do not report many false warnings. My current projects focus on (1) incremental analysis, verification and debugging of multithreaded programs, (2) static analysis of Java programs and its usage for improving scalability of software verification, and (3) using randomization to improve performance of error detection techniques based on state space traversal.

Recent publications

• P. Parízek and O. Lhoták. Fast Detection of Concurrency Errors by State Space Traversal with Randomization and Early Backtracking. International Journal on Software Tools for Technology Transfer, accepted, published online, Springer, 2018
• P. Parízek. Hybrid Partial Order Reduction with Under-Approximate Dynamic Points-To and Determinacy Information. FMCAD 2016, IEEE
• P. Parízek. Fast Error Detection with Hybrid Analyses of Future Accesses. SAC 2016, MUSEPAT track, ACM
• P. Parízek. Hybrid Analysis for Partial Order Reduction of Programs with Arrays. VMCAI 2016, LNCS, vol. 9583
• J. Daniel and P. Parízek. PANDA: Simultaneous Predicate Abstraction and Concrete Execution. HVC 2015, LNCS, vol. 9434
• 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
• J. Daniel and P. Parízek. Predicate Abstraction in Program Verification: Survey and Current Trends. ICCSW 2014, OpenAccess Series in Informatics (OASIcs), vol. 43
• P. Parízek and P. Jančík. Approximating Happens-Before Order: Interplay between Static Analysis and State Space Traversal. SPIN 2014, ACM
• J. Daniel, P. Parízek, and C.S. Pasareanu. Predicate Abstraction in Java Pathfinder. Java Pathfinder Workshop 2013, ACM SIGSOFT Software Engineering Notes, vol. 39, issue 1
• A. Khyzha, P. Parízek, and C.S. Pasareanu. Abstract Pathfinder. Java Pathfinder Workshop 2012, ACM SIGSOFT Software Engineering Notes, vol. 37, issue 6
• P. Parízek and O. Lhoták. Predicate Abstraction of Java Programs with Collections. OOPSLA 2012, ACM
• P. Parízek and O. Lhoták. Identifying Future Field Accesses in Exhaustive State Space Traversal. ASE 2011, IEEE CS
• P. Parízek and O. Lhoták. Randomized Backtracking: Next Steps. Java Pathfinder Workshop 2011
• P. Jančík, J. Kofroň, and P. Parízek. Advanced Debugging with JPF-Inspector. Java Pathfinder Workshop 2011
• P. Parízek and O. Lhoták. Randomized Backtracking in State Space Traversal. SPIN 2011, LNCS, vol. 6823
• T. Kalibera, P. Parízek, M. Malohlava, and M. Schoeberl. Exhaustive Testing of Safety Critical Java. JTRES 2010, ACM
• P. Parízek and F. Plášil. Assume-Guarantee Verification of Software Components in SOFA 2 Framework. IET Software, vol. 4, issue 3, IET, 2010
• P. Parízek and T. Kalibera. Efficient Detection of Errors in Java Components Using Random Environment and Restarts. TACAS 2010, LNCS, vol. 6015

     Complete list (DBLP)

Software

• Soothsharp: C# front-end to the Viper verification framework, https://github.com/soothsilver/soothsharp
• JPF-Inspector: GDB-like debugger that allows the developer to control and inspect execution of a Java program under Java Pathfinder, https://github.com/d3sformal/jpf-inspector
• PANDA: Predicate abstraction in dynamic analysis, https://github.com/d3sformal/panda
• JPF-static: Practical verification using static analysis and Java Pathfinder, http://d3s.mff.cuni.cz/projects/formal_methods/jpf-static
• J2BP: Predicate abstraction of Java programs, http://d3s.mff.cuni.cz/~parizek/j2bp
• RTEmbed: Java Pathfinder extension for verification of Java programs for embedded and real-time platforms, http://d3s.mff.cuni.cz/~parizek/rtembed
• COMBAT: Component Behavior Analysis Toolset, http://d3s.mff.cuni.cz/projects/formal_methods/combat

Teaching

• NSWI132: Program Analysis and Code Verification
  • Lectures: Thu 10:40-12:10 in S10
  • Labs: Thu 12:20-13:50 in S10
• NSWI126: Advanced Tools for Software Development and Monitoring (in Czech)
  • Lectures: Mon 15:40-17:10 in SU2
• NSWI133: Commercial Workshops (in Czech)
  • Seminars: Wed 17:20-18:50 in S9