Associate professor
Department of Distributed and Dependable SystemsFaculty of Mathematics and Physics
Charles University, Czech Republic
E-mail: parizek@d3s.mff.cuni.cz
Phone: +420 95155 4148
Office: 309, 3rd floor, Malá Strana
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 F. Kliber. Checking Just Pairs of Threads for Efficient and Scalable Incremental Verification of Multithreaded Programs. Java Pathfinder Workshop 2022, ACM SIGSOFT Software Engineering Notes, vol. 48, issue 1
- A. Čižmárik and P. Parízek. SharpDetect: Dynamic Analysis Framework for C#/.NET Programs. RV 2020, LNCS, vol. 12399
- R. Kápl and P. Parízek. Endicheck: Dynamic Analysis for Detecting Endianness Bugs. TACAS 2020, LNCS, vol. 12079
- K. Storey, E. Mercer, and P. Parízek. A Sound Dynamic Partial Order Reduction Engine for Java Pathfinder. Java Pathfinder Workshop 2019, ACM SIGSOFT Software Engineering Notes, vol. 44, issue 4
- P. Parízek. BUBEN: Automated Library Abstractions Enabling Scalable Bug Detection for Large Programs with I/O and Complex Environment. ATVA 2019, LNCS, vol. 11781
- 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, vol. 21, issue 4, Springer, 2019
- 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
Software
- BUBEN: Automated generator of library abstractions for scalable bug detection in large Java programs with Java Pathfinder, https://github.com/d3sformal/buben
- 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