Contact information:
Department of Distributed and Dependable SystemsFaculty of Mathematics and Physics
Charles University
Malostranské náměstí 25
118 00 Praha 1
Czech Republic
E-mail: jan.kofron@d3s.mff.cuni.cz
Phone: +420 951 554 285
Office: 309, 3rd floor
Education
- Ph.D. in Software Systems, Faculty of Mathematics and Physics, Charles University, 2007
- RNDr. in Software Systems, Faculty of Mathematics and Physics, Charles University, 2005
- Mgr. (MSc. equivalent) in Computer Science, Faculty of Mathematics and Physics, Charles University, 2003
Research interests and activities
- Interpolation-based Code Model Checking
- Static Analysis of Programs
Teaching
- My office hours (konzultační hodiny) are Thursday, 14:00 – 15:00.
- System Behavior Models and Verification
- Java Labs
- Program Semantics
- Developing Applications for Mobile Devices
Projects
Current
Past
- Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures
- The Q-ImPrESS project
- The SOFA 2 project
- The OSMOSE project, hosted by ObjectWeb
- Component Reliability Extension for Fractal, a project funded by France Telecom, R & D
- CoCoME – Common Component Modeling Example contest
- The ASCENS project
Publications
Martin Blicha, Antti E. J. Hyvärinen, Jan Kofroň, Natasha Sharygina:
Decomposing Farkas Interpolants, in Tools and Algorithms for the Construction and Analysis of Systems, ISBN: 978-3-030-17462-0, pp. 3-20
DOI: 10.1007/978-3-030-17462-0_1, 2019
Decomposing Farkas Interpolants, in Tools and Algorithms for the Construction and Analysis of Systems, ISBN: 978-3-030-17462-0, pp. 3-20
DOI: 10.1007/978-3-030-17462-0_1, 2019
Paolo Arcaini, Pavel Ježek, Jan Kofroň:
Modelling the Hybrid ERTMS/ETCS Level 3 Case Study in Spin, in Abstract State Machines, Alloy, B, TLA, VDM, and Z, ISBN: 978-3-319-91271-4, pp. 277-291
DOI: 10.1007/978-3-319-91271-4_19, 2018
Modelling the Hybrid ERTMS/ETCS Level 3 Case Study in Spin, in Abstract State Machines, Alloy, B, TLA, VDM, and Z, ISBN: 978-3-319-91271-4, pp. 277-291
DOI: 10.1007/978-3-319-91271-4_19, 2018
Pavel Jančík, Jan Kofroň:
On partial state matching, in Formal Aspects of Computing 29(5), pp. 777-803
DOI: 10.1007/s00165-016-0413-z, 2017
On partial state matching, in Formal Aspects of Computing 29(5), pp. 777-803
DOI: 10.1007/s00165-016-0413-z, 2017
Pavel Jančík, Jan Kofroň:
Dead Variable Analysis for Multi-threaded Heap Manipulating Programs, in Proceedings of the 31st Annual ACM Symposium on Applied Computing, ISBN: 978-1-4503-3739-7, pp. 1620–1627
DOI: 10.1145/2851613.2851826, 2016
Dead Variable Analysis for Multi-threaded Heap Manipulating Programs, in Proceedings of the 31st Annual ACM Symposium on Applied Computing, ISBN: 978-1-4503-3739-7, pp. 1620–1627
DOI: 10.1145/2851613.2851826, 2016
Pavel Jančík, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Jan Kofroň, Natasha Sharygina:
PVAIR: Partial Variable Assignment InterpolatoR, in Proceedings of FASE 2016, ISBN: 978-3-662-49665-7, pp. 419-434
DOI: 10.1007/978-3-662-49665-7_25, 2016
PVAIR: Partial Variable Assignment InterpolatoR, in Proceedings of FASE 2016, ISBN: 978-3-662-49665-7, pp. 419-434
DOI: 10.1007/978-3-662-49665-7_25, 2016
David Hauzar, Jan Kofroň:
Framework for Static Analysis of PHP Applications, in Proceedings of ECOOP 2015, ISBN: 978-3-939897-86-6, pp. 689–711
DOI: 10.4230/LIPIcs.ECOOP.2015.689, 2015
Framework for Static Analysis of PHP Applications, in Proceedings of ECOOP 2015, ISBN: 978-3-939897-86-6, pp. 689–711
DOI: 10.4230/LIPIcs.ECOOP.2015.689, 2015
Tomáš Bureš, Petr Hnětynka, Jan Kofroň, Rima Al-Ali, Dominik Škoda:
Statistical Approach to Architecture Modes in Smart Cyber Physical Systems, Technical report no. D3S-TR-2015-04, Department of Distributed and Dependable Systems, Charles University, , 2015
Statistical Approach to Architecture Modes in Smart Cyber Physical Systems, Technical report no. D3S-TR-2015-04, Department of Distributed and Dependable Systems, Charles University, , 2015
Jacques Combaz, Saddek Bensalem, Francesco Tiezzi, Andrea Margheri, Rosario Pugliese, Jan Kofroň:
Correctness of Service Components and Service Component Ensembles, in Software Engineering for Collective Autonomic Systems: The ASCENS Approach, ISBN: 978-3-319-16310-9, pp. 107-159, 2015
Correctness of Service Components and Service Component Ensembles, in Software Engineering for Collective Autonomic Systems: The ASCENS Approach, ISBN: 978-3-319-16310-9, pp. 107-159, 2015
Dhaminda B. Abeywickrama, Jacques Combaz, Vojtěch Horký, Jaroslav Keznikl, Jan Kofroň, Alberto Lluch Lafuente, Michele Loreti, Andrea Margheri, Philip Mayer, Valentina Monreale, Ugo Montanari, Carlo Pinciroli, Petr Tůma, Andrea Vandin, Emil Vassev:
Tools for Ensemble Design and Runtime, in Software Engineering for Collective Autonomic Systems, ISBN: 978-3-319-16309-3 978-3-319-16310-9, pp. 429-448, 2015
Tools for Ensemble Design and Runtime, in Software Engineering for Collective Autonomic Systems, ISBN: 978-3-319-16309-3 978-3-319-16310-9, pp. 429-448, 2015
David Hauzar, Jan Kofroň:
WeVerca: Web Applications Verification for PHP, in Proceedings of SEFM 2014, ISBN: 978-3-319-10430-0, pp. 296-301
DOI: 10.1007/978-3-319-10431-7_24, 2014
WeVerca: Web Applications Verification for PHP, in Proceedings of SEFM 2014, ISBN: 978-3-319-10430-0, pp. 296-301
DOI: 10.1007/978-3-319-10431-7_24, 2014
David Hauzar, Jan Kofroň, Pavel Baštecký:
Data-flow Analysis of Programs with Associative Arrays, in Proceedings of ESSS 2014,
DOI: 10.4204/EPTCS.150.6, 2014
Data-flow Analysis of Programs with Associative Arrays, in Proceedings of ESSS 2014,
DOI: 10.4204/EPTCS.150.6, 2014
Pavel Jancik, Jan Kofroň, Simone Fulvio Rollini, Natasha Sharygina:
On Interpolants and Variable Assignments, in Proceedings of FMCAD 2014, ISBN: 978-0-9835678-4-4, pp. 123–130
DOI: 10.1109/FMCAD.2014.6987604, 2014
On Interpolants and Variable Assignments, in Proceedings of FMCAD 2014, ISBN: 978-0-9835678-4-4, pp. 123–130
DOI: 10.1109/FMCAD.2014.6987604, 2014
Pavel Jančík, Jan Kofroň:
On Partial Variable Assignment Interpolants, Technical report no. D3S-TR-2013-05, Department of Distributed and Dependable Systems, Charles University, , 2013
On Partial Variable Assignment Interpolants, Technical report no. D3S-TR-2013-05, Department of Distributed and Dependable Systems, Charles University, , 2013
Tomáš Poch, Ondřej Šerý, František Plášil, Jan Kofroň:
Threaded behavior protocols, in Formal Aspects of Computing 25(4), pp. 543-572
DOI: 10.1007/s00165-011-0194-3, 2013
Threaded behavior protocols, in Formal Aspects of Computing 25(4), pp. 543-572
DOI: 10.1007/s00165-011-0194-3, 2013
Tomas Kučera, Petr Hnětynka, Jan Kofroň:
Automated Deployment of Hierarchical Components, in Proceedings of SNPD 2012, ISBN: 978-3-642-32172-6, pp. 117-128
DOI: 10.1007/978-3-642-32172-6_10, 2012
Automated Deployment of Hierarchical Components, in Proceedings of SNPD 2012, ISBN: 978-3-642-32172-6, pp. 117-128
DOI: 10.1007/978-3-642-32172-6_10, 2012
David Hauzar, Jan Kofroň:
On Security Analysis of PHP Web Applications, in Proceedings of STPSA 2012, ISBN: 978-1-4673-2714-5, pp. 577-582
DOI: 10.1109/COMPSACW.2012.106, 2012
On Security Analysis of PHP Web Applications, in Proceedings of STPSA 2012, ISBN: 978-1-4673-2714-5, pp. 577-582
DOI: 10.1109/COMPSACW.2012.106, 2012
Pavel Jančík, Pavel Parízek, Jan Kofroň:
BeJC: Checking Compliance Between Java Implementation and Behavior Specification, in Proceedings of WCOP 2014, ISBN: 978-1-4503-1348-3, pp. 31–36
DOI: 10.1145/2304676.2304683, 2012
BeJC: Checking Compliance Between Java Implementation and Behavior Specification, in Proceedings of WCOP 2014, ISBN: 978-1-4503-1348-3, pp. 31–36
DOI: 10.1145/2304676.2304683, 2012
Jan Kofroň, Pavel Jančík, Pavel Parízek:
Refinement between TBP and Java Implementation of Components, Technical report no. 2011/5, Department of Distributed and Dependable Systems, Charles University, , 2011
Refinement between TBP and Java Implementation of Components, Technical report no. 2011/5, Department of Distributed and Dependable Systems, Charles University, , 2011
David Hauzar, Jan Kofroň:
Hunting Bugs Inside Web Applications, Technical report no. 2011-26, Department of Informatics, KIT, , 2011
Hunting Bugs Inside Web Applications, Technical report no. 2011-26, Department of Informatics, KIT, , 2011
Steffen Becker, Michael Hauck, Mircea Trifu, Klaus Krogmann, Jan Kofroň:
Reverse Engineering Component Models for Quality Predictions, in Proceedings of CSMR 2010, ISBN: 978-1-61284-369-8, pp. 194-197
DOI: 10.1109/CSMR.2010.34, 2010
Reverse Engineering Component Models for Quality Predictions, in Proceedings of CSMR 2010, ISBN: 978-1-61284-369-8, pp. 194-197
DOI: 10.1109/CSMR.2010.34, 2010
Jan Kofroň, Pavel Parízek, Ondřej Šerý:
On Teaching Formal Methods: Behavior Models and Code Analysis, in Proceedings of TFM 2009, ISBN: 978-3-642-04912-5, pp. 144-157
DOI: 10.1007/978-3-642-04912-5_10, 2009
On Teaching Formal Methods: Behavior Models and Code Analysis, in Proceedings of TFM 2009, ISBN: 978-3-642-04912-5, pp. 144-157
DOI: 10.1007/978-3-642-04912-5_10, 2009
Jan Kofroň, František Plášil, Ondřej Šerý:
Modes in component behavior specification via EBP and their application in product lines, in Information and Software Technology 51(1), pp. 31-41
DOI: 10.1016/j.infsof.2008.09.011, 2009
Modes in component behavior specification via EBP and their application in product lines, in Information and Software Technology 51(1), pp. 31-41
DOI: 10.1016/j.infsof.2008.09.011, 2009
Jan Kofroň, Tomáš Poch, Ondřej Šerý:
TBP: Code-Oriented Component Behavior Specification, in Proceedings of SEW 2008, ISBN: 978-0-7695-3617-0, pp. 75-83
DOI: 10.1109/SEW.2008.14, 2008
TBP: Code-Oriented Component Behavior Specification, in Proceedings of SEW 2008, ISBN: 978-0-7695-3617-0, pp. 75-83
DOI: 10.1109/SEW.2008.14, 2008
Jan Kofroň, Tomáš Poch, Ondřej Šerý:
Making Components Fit: SPINing, in Proceedings of SEW 2008, ISBN: 978-0-7695-3617-0, pp. 65-74
DOI: 10.1109/SEW.2008.10, 2008
Making Components Fit: SPINing, in Proceedings of SEW 2008, ISBN: 978-0-7695-3617-0, pp. 65-74
DOI: 10.1109/SEW.2008.10, 2008
Steffen Becker, Lubomír Bulej, Tomáš Bureš, Petr Hnětynka, Lucia Kapova, Jan Kofroň, Heiko Koziolek, Johan Kraft, Raffaella Mirandola, Johannes Stammel, Giordano Tamburrelli, Mircea Trifu:
Service Architecture Meta Model, Technical report no. , , , 2008
Service Architecture Meta Model, Technical report no. , , , 2008
Tomáš Bureš, Martin Děcký, Petr Hnětynka, Jan Kofroň, Pavel Parízek, František Plášil, Tomáš Poch, Ondřej Šerý, Petr Tůma:
CoCoME in SOFA, in The Common Component Modeling Example: Comparing Software Component Models, ISBN: 978-3-540-85289-6, pp. 388-417, 2008
CoCoME in SOFA, in The Common Component Modeling Example: Comparing Software Component Models, ISBN: 978-3-540-85289-6, pp. 388-417, 2008
Jan Kofroň:
Checking Software Component Behavior Using Behavior Protocols and Spin, in Proceedings SAC 2007, ISBN: 978-1-59593-480-2, pp. 1513–1517
DOI: 10.1145/1244002.1244326, 2007
Checking Software Component Behavior Using Behavior Protocols and Spin, in Proceedings SAC 2007, ISBN: 978-1-59593-480-2, pp. 1513–1517
DOI: 10.1145/1244002.1244326, 2007
Jiri Adamek, Tomáš Bureš, Pavel Ježek, Jan Kofroň, Vladimir Mencl, Pavel Parízek, František Plášil:
Component reliability extensions for fractal component model, Technical report no. XX/2006, Institute of Computer Science Academy of Sciences of the Czech Republic & France Telecom, , 2006
Component reliability extensions for fractal component model, Technical report no. XX/2006, Institute of Computer Science Academy of Sciences of the Czech Republic & France Telecom, , 2006
Pavel Ježek, Jan Kofroň, František Plášil:
Model Checking of Component Behavior Specification: A Real Life Experience, in Electronic Notes in Theoretical Computer Science 0(0), pp. 197-210
DOI: 10.1016/j.entcs.2006.05.023, 2006
Model Checking of Component Behavior Specification: A Real Life Experience, in Electronic Notes in Theoretical Computer Science 0(0), pp. 197-210
DOI: 10.1016/j.entcs.2006.05.023, 2006
Jan Kofroň:
Extending Behavior Protocols With Data and Multisynchronization, Technical report no. 2006/10, Department of Software Engineering, Charles University, , 2006
Extending Behavior Protocols With Data and Multisynchronization, Technical report no. 2006/10, Department of Software Engineering, Charles University, , 2006
Pavel Parízek, František Plášil, Jan Kofroň:
Model Checking of Software Components: Making Java PathFinder Cooperate with Behavior Protocol Checker, Technical report no. 2006/02, Department of Software Engineering, Charles University, , 2006
Model Checking of Software Components: Making Java PathFinder Cooperate with Behavior Protocol Checker, Technical report no. 2006/02, Department of Software Engineering, Charles University, , 2006
Jan Kofroň:
Software Component Verification: On Translating Behavior Protocols to Promela, Technical report no. 2006/11, Department of Software Engineering, Charles University, , 2006
Software Component Verification: On Translating Behavior Protocols to Promela, Technical report no. 2006/11, Department of Software Engineering, Charles University, , 2006
Martin Mach, František Plášil, Jan Kofroň:
Behavior Protocols Verification: Fighting State Explosion, in International Journal of Computer and Information Science 6(1), pp. 22-30, 2005
Behavior Protocols Verification: Fighting State Explosion, in International Journal of Computer and Information Science 6(1), pp. 22-30, 2005
Jan Kofroň:
Enhancing Behavior Protocols with Atomic Actions, Technical report no. 2005/08, Department of Software Engineering, Charles University, , 2005
Enhancing Behavior Protocols with Atomic Actions, Technical report no. 2005/08, Department of Software Engineering, Charles University, , 2005