Pavel Parízek, Ph.D.

Assistant Professor

I'm currently on academic leave at University of Waterloo,
but I still read e-mail sent to the address below.

Department of Distributed and Dependable Systems
Faculty of Mathematics and Physics
Charles University in Prague
Malostranske namesti 25
118 00 Prague 1
Czech Republic

E-mail: pavel.parizek at d3s.mff.cuni.cz
Phone: (+420) 2 2191 4235
Fax: (+420) 2 2191 4323
Office: room 204, 2nd floor

[Research] [Projects] [Software] [Publications] [Education] [Teaching]

Research Interests

Behavior specification and verification of software components
- Modeling and generation of reasonable artificial environment for model checking of Java components
- Efficient construction of environment assumptions for verification based on assume-guarantee reasoning
- Automated extraction of component behavior specification from the code
Automated verification and analysis of programs
- Verification of Java programs for embedded and real-time platforms (e.g., compliant with RTSJ)
- Static analysis of Java source code and byte code

Projects

Q-ImPrESS: Quality Impact Prediction for Evolving Service-oriented Software, http://www.q-impress.eu
ITEA/OSIRIS: Open source platform and infrastructure for run-time integration of services, http://www.itea-osiris.org
Common Component Modeling Example (CoCoME), http://www.cocome.org
Component Reliability Extensions (CRE) for Fractal Component Model, http://kraken.cs.cas.cz/ft/public/public_index.phtml

Software

RTEmbed: Java PathFinder extension for verification of Java programs for embedded and real-time platforms, http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/rtembed
COMBAT: Component Behavior Analysis Toolset, http://dsrg.mff.cuni.cz/projects/combat
BPEL checker, http://dsrg.mff.cuni.cz/projects/bpelchecker
Environment Generator for Java PathFinder, http://dsrg.mff.cuni.cz/projects/envgen

Publications

Journal Papers

P. Parizek and F. Plasil. Assume-Guarantee Verification of Software Components in SOFA 2 Framework, IET Software, volume 4, issue 3, IET, Jun 2010

Refereed Conference/Workshop Proceedings

T. Kalibera, P. Parizek, M. Malohlava, and M. Schoeberl. Exhaustive Testing of Safety Critical Java, JTRES 2010, ACM, Aug 2010
P. Parizek and T. Kalibera. Efficient Detection of Errors in Java Components Using Random Environment and Restarts, TACAS 2010, LNCS, vol. 6015, Mar 2010
P. Parizek and N. Yuldashev. Extraction of Component-Environment Interaction Model Using State Space Traversal, SAC 2010, SE track, ACM, Mar 2010
T. Kalibera, P. Parizek, G. Haddad, G. Leavens, and J. Vitek. Challenge Benchmarks for Verification of Real-time Programs, PLPV'10, ACM, Jan 2010
P. Parizek and T. Kalibera. Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs, FMICS 2009, LNCS, vol. 5825, Nov 2009
J. Kofron, P. Parizek, and O. Sery. On Teaching Formal Methods: Behavior Models and Code Analysis, TFM 2009, LNCS, vol. 5846, Nov 2009
P. Parizek, J. Adamek, and T. Kalibera. Automated Construction of Reasonable Environment for Java Components, FESCA 2009, ENTCS, vol. 253, issue 1, Oct 2009
P. Parizek and J. Adamek. Checking Session-Oriented Interactions between Web Services, EUROMICRO SEAA 2008, IEEE CS, Sep 2008
P. Parizek and F. Plasil. Modeling of Component Environment in Presence of Callbacks and Autonomous Activities, TOOLS EUROPE 2008, LNBIP, vol. 11, Jun 2008
P. Parizek and F. Plasil. Partial Verification of Software Components: Heuristics for Environment Construction, EUROMICRO SEAA 2007, IEEE CS, Aug 2007
P. Parizek and F. Plasil. Modeling Environment for Component Model Checking from Hierarchical Architecture, FACS'06, ENTCS, vol. 182, Jun 2007
P. Parizek and F. Plasil. Specification and Generation of Environment for Model Checking of Software Components, FESCA 2006, ENTCS, vol. 176, issue 2, May 2007
P. Parizek, F. Plasil, and J. Kofron. Model Checking of Software Components: Combining Java PathFinder and Behavior Protocol Model Checker, SEW 2006, IEEE CS, Jan 2007

Book Chapters

T. Bures, M. Decky, P. Hnetynka, J. Kofron, P. Parizek, F. Plasil, T. Poch, O. Sery, and P. Tuma. CoCoME in SOFA, The Common Component Modeling Example: Comparing Software Component Models, Springer-Verlag, LNCS, vol. 5153, Aug 2008
L. Bulej, T. Bures, T. Coupaye, M. Decky, P. Jezek, P. Parizek, F. Plasil, T. Poch, N. Rivierre, O. Sery, and P. Tuma. CoCoME in Fractal, The Common Component Modeling Example: Comparing Software Component Models, Springer-Verlag, LNCS, vol. 5153, Aug 2008

Other

P. Parizek. Formal Verification of Components in Java, Ph.D. thesis, advisor: Frantisek Plasil, Sep 2008

Education

Ph.D. in Software Systems, Faculty of Mathematics and Physics, Charles University, 2008
RNDr. (similar to Ph.D. candidate) in Computer Science, Faculty of Mathematics and Physics, Charles University, 2007
Mgr. (MSc equivalent) in Computer Science, Faculty of Mathematics and Physics, Charles University, 2005

Teaching

Past teaching:
- NSWE001: Embedded and Real-Time Systems - labs (summer 2010)
- NPRG043: Recommended Programming Practices - labs (summer 2010)
- NSWI132: Program Analysis and Code Verification (winter 2008-2009)
- NPRG013: Java - labs (winter 2009)
- NSWI126: Software Development and Monitoring Tools (winter 2008)
- NSWI096: Internet - labs (winter 2007, summer 2008)
- NPRG033: Individual Software Project - specification (summer 2006-2008)
- NPRG034: Individual Software Project - implementation (winter 2006-2008)
Supervised master theses:
- Nodir Yuldashev: Using Java PathFinder for Construction of Abstractions of Java Programs (Dec 2006 - May 2009)
- Pavel Jancik: Checking Compliance of Java Implementation with TBP Specification (Apr 2009 - Sep 2010)