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 analysis, 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.
Recent publications
- C. Artho, P. Parízek, D. Qu, V. Galgali, and P. Yi. JPF: From 2003 to 2023. TACAS 2024, LNCS, vol. 14571
- 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
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