Jan Kofroň

Contact information:

Department of Distributed and Dependable Systems
Faculty 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

• ROBUST: Verification and Bug-Hunting For Advanced Software
• The Weverca project

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

 @inproceedings{blicha_decomposing_2019,
    title = {{Decomposing Farkas Interpolants}},
    author = {Blicha, Martin and Hyvärinen, Antti E. J. and Kofroň, Jan and Sharygina, Natasha},
    year = {2019},
    booktitle = {{Tools and Algorithms for the Construction and Analysis of Systems}},
    editor = {Vojnar, Tomáš and Zhang, Lijun},
    publisher = {Springer International Publishing},
    series = {{Lecture Notes in Computer Science}},
    doi = {10.1007/978-3-030-17462-0_1},
    isbn = {978-3-030-17462-0},
    pages = {3–20},
}
 

 @inproceedings{arcaini_modelling_2018,
    title = {{Modelling the Hybrid ERTMS/ETCS Level 3 Case Study in Spin}},
    author = {Arcaini, Paolo and Ježek, Pavel and Kofroň, Jan},
    year = {2018},
    booktitle = {{Abstract State Machines, Alloy, B, TLA, VDM, and Z}},
    editor = {Butler, Michael and Raschke, Alexander and Hoang, Thai Son and Reichl, Klaus},
    publisher = {Springer International Publishing},
    series = {{Lecture Notes in Computer Science}},
    doi = {10.1007/978-3-319-91271-4_19},
    isbn = {978-3-319-91271-4},
    pages = {277–291},
    url = {https://link.springer.com/chapter/10.1007%2F978-3-319-91271-4_19},
}
 

 @article{jancik_partial_2017,
    title = {{On partial state matching}},
    author = {Jančík, Pavel and Kofroň, Jan},
    year = {2017},
    journal = {{Formal Aspects of Computing}},
    number = {5},
    doi = {10.1007/s00165-016-0413-z},
    issn = {1433-299X},
    pages = {777–803},
    url = {10.1007/s00165-016-0413-z},
    volume = {29},
}
 

 @inproceedings{jancik_pvair_2016,
    title = {{PVAIR: Partial Variable Assignment InterpolatoR}},
    author = {Jančík, Pavel and Alt, Leonardo and Fedyukovich, Grigory and Hyvärinen, Antti E. J. and Kofroň, Jan and Sharygina, Natasha},
    year = {2016},
    booktitle = {{Proceedings of FASE 2016}},
    editor = {Stevens, Perdita and Wąsowski, Andrzej},
    publisher = {Springer Berlin Heidelberg},
    series = {{Lecture Notes in Computer Science}},
    doi = {10.1007/978-3-662-49665-7_25},
    isbn = {978-3-662-49665-7},
    pages = {419–434},
    shorttitle = {PVAIR},
}
 

 @inproceedings{jancik_dead_2016,
    title = {{Dead Variable Analysis for Multi-threaded Heap Manipulating Programs}},
    author = {Jančík, Pavel and Kofroň, Jan},
    year = {2016},
    booktitle = {{Proceedings of the 31st Annual ACM Symposium on Applied Computing}},
    publisher = {ACM},
    series = {{SAC ‘16}},
    location = {New York, NY, USA},
    doi = {10.1145/2851613.2851826},
    isbn = {978-1-4503-3739-7},
    pages = {1620–1627},
    url = {http://doi.acm.org/10.1145/2851613.2851826},
}
 

 @techreport{bures_statistical_report_2015,
    title = {{Statistical Approach to Architecture Modes in Smart Cyber Physical Systems}},
    author = {Bureš, Tomáš and Hnětynka, Petr and Kofroň, Jan and Al-Ali, Rima and Škoda, Dominik},
    year = {2015},
    institution = {Department of Distributed and Dependable Systems, Charles University},
    number = {D3S-TR-2015-04},
}
 

 @incollection{combaz_correctness_2015,
    title = {{Correctness of Service Components and Service Component Ensembles}},
    author = {Combaz, Jacques and Bensalem, Saddek and Tiezzi, Francesco and Margheri, Andrea and Pugliese, Rosario and Kofroň, Jan},
    year = {2015},
    booktitle = {{Software Engineering for Collective Autonomic Systems: The ASCENS Approach}},
    editor = {Wirsing, Martin and Hölzl, Matthias and Koch, Nora and Mayer, Philip},
    publisher = {Springer International Publishing},
    series = {{Lecture Notes in Computer Science}},
    location = {Cham},
    doi = {10.1007/978-3-319-16310-9_3},
    isbn = {978-3-319-16310-9},
    pages = {107–159},
    url = {https://doi.org/10.1007/978-3-319-16310-9_3},
}
 

 @inproceedings{hauzar_framework_2015,
    title = {{Framework for Static Analysis of PHP Applications}},
    author = {Hauzar, David and Kofroň, Jan},
    year = {2015},
    booktitle = {{Proceedings of ECOOP 2015}},
    editor = {Boyland, John Tang},
    publisher = {Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik},
    series = {{Leibniz International Proceedings in Informatics (LIPIcs)}},
    location = {Dagstuhl, Germany},
    doi = {10.4230/LIPIcs.ECOOP.2015.689},
    isbn = {978-3-939897-86-6},
    pages = {689–711},
    url = {http://drops.dagstuhl.de/opus/volltexte/2015/5243},
    volume = {37},
}
 

 @incollection{abeywickrama_tools_2015,
    title = {{Tools for Ensemble Design and Runtime}},
    author = {Abeywickrama, Dhaminda B. and Combaz, Jacques and Horký, Vojtěch and Keznikl, Jaroslav and Kofroň, Jan and Lafuente, Alberto Lluch and Loreti, Michele and Margheri, Andrea and Mayer, Philip and Monreale, Valentina and Montanari, Ugo and Pinciroli, Carlo and Tůma, Petr and Vandin, Andrea and Vassev, Emil},
    year = {2015},
    booktitle = {{Software Engineering for Collective Autonomic Systems}},
    editor = {Wirsing, Martin and Hölzl, Matthias and Koch, Nora and Mayer, Philip},
    publisher = {Springer International Publishing},
    series = {{Lecture Notes in Computer Science}},
    number = {8998},
    isbn = {978-3-319-16309-3 978-3-319-16310-9},
    pages = {429–448},
    url = {http://link.springer.com/chapter/10.1007/978-3-319-16310-9_13},
}
 

 @inproceedings{jancik_interpolants_2014,
    title = {{On Interpolants and Variable Assignments}},
    author = {Jancik, Pavel and Kofroň, Jan and Rollini, Simone Fulvio and Sharygina, Natasha},
    year = {2014},
    booktitle = {{Proceedings of FMCAD 2014}},
    publisher = {FMCAD Inc},
    series = {{FMCAD ‘14}},
    location = {Austin, TX},
    doi = {10.1109/FMCAD.2014.6987604},
    isbn = {978-0-9835678-4-4},
    pages = {123–130},
    url = {http://dl.acm.org/citation.cfm?id=2682923.2682948},
}
 

 @inproceedings{hauzar_dataflow_2014,
    title = {{Data-flow Analysis of Programs with Associative Arrays}},
    author = {Hauzar, David and Kofroň, Jan and Baštecký, Pavel},
    year = {2014},
    booktitle = {{Proceedings of ESSS 2014}},
    publisher = {EPTCS},
    doi = {10.4204/EPTCS.150.6},
    url = {https://arxiv.org/abs/1405.1116},
}
 

 @inproceedings{hauzar_weverca_2014,
    title = {{WeVerca: Web Applications Verification for PHP}},
    author = {Hauzar, David and Kofroň, Jan},
    year = {2014},
    booktitle = {{Proceedings of SEFM 2014}},
    editor = {Giannakopoulou, Dimitra and Salaün, Gwen},
    publisher = {Springer International Publishing},
    series = {{Lecture Notes in Computer Science}},
    doi = {10.1007/978-3-319-10431-7_24},
    isbn = {978-3-319-10430-0},
    pages = {296–301},
    url = {https://link.springer.com/chapter/10.1007/978-3-319-10431-7_24},
    shorttitle = {WeVerca},
}
 

 @article{poch_threaded_2013,
    title = {{Threaded behavior protocols}},
    author = {Poch, Tomáš and Šerý, Ondřej and Plášil, František and Kofroň, Jan},
    year = {2013},
    journal = {{Formal Aspects of Computing}},
    number = {4},
    doi = {10.1007/s00165-011-0194-3},
    issn = {0934-5043, 1433-299X},
    pages = {543–572},
    url = {https://link.springer.com/article/10.1007/s00165-011-0194-3},
    volume = {25},
}
 

 @techreport{jancik_partial_report_2013,
    title = {{On Partial Variable Assignment Interpolants}},
    author = {Jančík, Pavel and Kofroň, Jan},
    year = {2013},
    institution = {Department of Distributed and Dependable Systems, Charles University},
    number = {D3S-TR-2013-05},
}
 

 @inproceedings{hauzar_security_2012,
    title = {{On Security Analysis of PHP Web Applications}},
    author = {Hauzar, David and Kofroň, Jan},
    year = {2012},
    booktitle = {{Proceedings of STPSA 2012}},
    doi = {10.1109/COMPSACW.2012.106},
    isbn = {978-1-4673-2714-5},
    pages = {577–582},
    url = {https://ieeexplore.ieee.org/document/6341638},
}
 

 @inproceedings{jancik_bejc_2012,
    title = {{BeJC: Checking Compliance Between Java Implementation and Behavior Specification}},
    author = {Jančík, Pavel and Parízek, Pavel and Kofroň, Jan},
    year = {2012},
    booktitle = {{Proceedings of WCOP 2014}},
    publisher = {ACM},
    series = {{WCOP ‘12}},
    location = {New York, NY, USA},
    doi = {10.1145/2304676.2304683},
    isbn = {978-1-4503-1348-3},
    pages = {31–36},
    url = {http://doi.acm.org/10.1145/2304676.2304683},
    shorttitle = {BeJC},
}
 

 @inproceedings{kucera_automated_2012,
    title = {{Automated Deployment of Hierarchical Components}},
    author = {Kučera, Tomas and Hnětynka, Petr and Kofroň, Jan},
    year = {2012},
    booktitle = {{Proceedings of SNPD 2012}},
    editor = {Lee, Roger},
    publisher = {Springer Berlin Heidelberg},
    series = {{Studies in Computational Intelligence}},
    doi = {10.1007/978-3-642-32172-6_10},
    isbn = {978-3-642-32172-6},
    pages = {117–128},
    url = {https://link.springer.com/chapter/10.1007/978-3-642-32172-6_10},
}
 

 @techreport{kofron_refinement_report_2011,
    title = {{Refinement between TBP and Java Implementation of Components}},
    author = {Kofroň, Jan and Jančík, Pavel and Parízek, Pavel},
    year = {2011},
    institution = {Department of Distributed and Dependable Systems, Charles University},
    number = {2011/5},
}
 

 @techreport{hauzar_hunting_report_2011,
    title = {{Hunting Bugs Inside Web Applications}},
    author = {Hauzar, David and Kofroň, Jan},
    year = {2011},
    institution = {Department of Informatics, KIT},
    number = {2011-26},
}
 

 @inproceedings{becker_reverse_2010,
    title = {{Reverse Engineering Component Models for Quality Predictions}},
    author = {Becker, Steffen and Hauck, Michael and Trifu, Mircea and Krogmann, Klaus and Kofroň, Jan},
    year = {2010},
    booktitle = {{Proceedings of CSMR 2010}},
    publisher = {IEEE},
    location = {Madrid, Spain},
    doi = {10.1109/CSMR.2010.34},
    isbn = {978-1-61284-369-8},
    pages = {194–197},
    url = {https://ieeexplore.ieee.org/document/5714435},
}
 

 @inproceedings{kofron_teaching_2009,
    title = {{On Teaching Formal Methods: Behavior Models and Code Analysis}},
    author = {Kofroň, Jan and Parízek, Pavel and Šerý, Ondřej},
    year = {2009},
    booktitle = {{Proceedings of TFM 2009}},
    editor = {Gibbons, Jeremy and Oliveira, José Nuno},
    publisher = {Springer Berlin Heidelberg},
    series = {{Lecture Notes in Computer Science}},
    doi = {10.1007/978-3-642-04912-5_10},
    isbn = {978-3-642-04912-5},
    pages = {144–157},
    url = {https://link.springer.com/chapter/10.1007/978-3-642-04912-5_10},
    shorttitle = {On Teaching Formal Methods},
}
 

 @article{kofron_modes_2009,
    title = {{Modes in component behavior specification via EBP and their application in product lines}},
    author = {Kofroň, Jan and Plášil, František and Šerý, Ondřej},
    year = {2009},
    journal = {{Information and Software Technology}},
    series = {{Special Section - Most Cited Articles in 2002 and Regular Research Papers}},
    number = {1},
    doi = {10.1016/j.infsof.2008.09.011},
    issn = {0950-5849},
    pages = {31–41},
    url = {http://www.sciencedirect.com/science/article/pii/S0950584908001341},
    volume = {51},
}
 

 @techreport{becker_service_report_2008,
    title = {{Service Architecture Meta Model}},
    author = {Becker, Steffen and Bulej, Lubomır and Bures, T. and Hnetynka, Petr and Kapova, Lucia and Kofron, Jan and Koziolek, Heiko and Kraft, Johan and Mirandola, Raffaella and Stammel, Johannes and Tamburrelli, Giordano and Trifu, Mircea},
    year = {2008},
}
 

 @incollection{bures_cocome_2008,
    title = {{CoCoME in SOFA}},
    author = {Bureš, Tomáš and Děcký, Martin and Hnětynka, Petr and Kofroň, Jan and Parízek, Pavel and Plášil, František and Poch, Tomáš and Šerý, Ondřej and Tůma, Petr},
    year = {2008},
    booktitle = {{The Common Component Modeling Example: Comparing Software Component Models}},
    editor = {Rausch, Andreas and Reussner, Ralf and Mirandola, Raffaela and Plášil, František},
    publisher = {Springer Berlin Heidelberg},
    series = {{Lecture Notes in Computer Science}},
    location = {Berlin, Heidelberg},
    doi = {10.1007/978-3-540-85289-6_15},
    isbn = {978-3-540-85289-6},
    pages = {388–417},
    url = {https://doi.org/10.1007/978-3-540-85289-6_15},
}
 

 @inproceedings{kofron_tbp_2008,
    title = {{TBP: Code-Oriented Component Behavior Specification}},
    author = {Kofroň, Jan and Poch, Tomáš and Šerý, Ondřej},
    year = {2008},
    booktitle = {{Proceedings of SEW 2008}},
    publisher = {IEEE},
    doi = {10.1109/SEW.2008.14},
    isbn = {978-0-7695-3617-0},
    pages = {75–83},
    url = {https://ieeexplore.ieee.org/document/5328403},
    shorttitle = {TBP},
}
 

 @inproceedings{kofron_making_2008,
    title = {{Making Components Fit: SPINing}},
    author = {Kofroň, Jan and Poch, Tomáš and Šerý, Ondřej},
    year = {2008},
    booktitle = {{Proceedings of SEW 2008}},
    doi = {10.1109/SEW.2008.10},
    isbn = {978-0-7695-3617-0},
    pages = {65–74},
    url = {https://ieeexplore.ieee.org/document/5328451},
    shorttitle = {Making Components Fit},
}
 

 @phdthesis{kofron_behavior_2007,
    title = {{Behavior Protocols Extensions}},
    author = {Kofroň, Jan},
    year = {2007},
    type = {Dissertation thesis},
    school = {Charles University},
    address = {Prague, Czech Republic},
}
 

 @inproceedings{kofron_checking_2007,
    title = {{Checking Software Component Behavior Using Behavior Protocols and Spin}},
    author = {Kofroň, Jan},
    year = {2007},
    booktitle = {{Proceedings SAC 2007}},
    publisher = {ACM},
    series = {{SAC ‘07}},
    location = {New York, NY, USA},
    doi = {10.1145/1244002.1244326},
    isbn = {978-1-59593-480-2},
    pages = {1513–1517},
    url = {http://doi.acm.org/10.1145/1244002.1244326},
}
 

 @techreport{parizek_model_report_2006,
    title = {{Model Checking of Software Components: Making Java PathFinder Cooperate with Behavior Protocol Checker}},
    author = {Parízek, Pavel and Plášil, František and Kofroň, Jan},
    year = {2006},
    institution = {Department of Software Engineering, Charles University},
    number = {2006/02},
}
 

 @techreport{adamek_component_report_2006,
    title = {{Component reliability extensions for fractal component model}},
    author = {Adamek, Jiri and Bures, Tomas and Jezek, Pavel and Kofron, Jan and Mencl, Vladimir and Parizek, Pavel and Plasil, Frantisek},
    year = {2006},
    institution = {Institute of Computer Science Academy of Sciences of the Czech Republic & France Telecom},
    number = {XX/2006},
    url = {http://kraken.cs.cas.cz/},
}
 

 @techreport{kofron_extending_report_2006,
    title = {{Extending Behavior Protocols With Data and Multisynchronization}},
    author = {Kofroň, Jan},
    year = {2006},
    institution = {Department of Software Engineering, Charles University},
    number = {2006/10},
}
 

 @article{jezek_model_2006,
    title = {{Model Checking of Component Behavior Specification: A Real Life Experience}},
    author = {Ježek, Pavel and Kofroň, Jan and Plášil, František},
    year = {2006},
    journal = {{Electronic Notes in Theoretical Computer Science}},
    series = {{Proceedings of the International Workshop on Formal Aspects of Component Software (FACS 2005)}},
    doi = {10.1016/j.entcs.2006.05.023},
    issn = {1571-0661},
    pages = {197–210},
    url = {http://www.sciencedirect.com/science/article/pii/S1571066106003859},
    volume = {160},
    shorttitle = {Model Checking of Component Behavior Specification},
}
 

 @techreport{kofron_software_report_2006,
    title = {{Software Component Verification: On Translating Behavior Protocols to Promela}},
    author = {Kofroň, Jan},
    year = {2006},
    institution = {Department of Software Engineering, Charles University},
    number = {2006/11},
}
 

 @article{mach_behavior_2005,
    title = {{Behavior Protocols Verification: Fighting State Explosion}},
    author = {Mach, Martin and Plášil, František and Kofroň, Jan},
    year = {2005},
    journal = {{International Journal of Computer and Information Science}},
    number = {1},
    issn = {1525-9293},
    pages = {22–30},
    url = {https://www.semanticscholar.org/paper/Behavior-Protocols-Verification-%3A-Fighting-State-Mach-Plasil/07450736bfcd18a475eabd1a07bc997d1fcb45ac},
    volume = {6},
    shorttitle = {Behavior Protocols Verification},
}
 

 @techreport{kofron_enhancing_report_2005,
    title = {{Enhancing Behavior Protocols with Atomic Actions}},
    author = {Kofroň, Jan},
    year = {2005},
    institution = {Department of Software Engineering, Charles University},
    number = {2005/08},
}
 

Links

Habilitation page