Jan Kofroň

Assistant professor

Department of Distributed and Dependable Systems
Faculty of Mathematics and Physics
Charles University, Czech Republic

E-mail: jan.kofron@d3s.mff.cuni.cz
Phone: +420 951 554 285
Office: 309, 3rd floor, Malá Strana

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 (last five years)

Full list of publications is available here.

 @article{arcaini_validation_2019,
    title = {{Validation of the Hybrid ERTMS/ETCS Level 3 using Spin}},
    author = {Arcaini, Paolo and Kofroň, Jan and Ježek, Pavel},
    year = {2019},
    journal = {{International Journal on Software Tools for Technology Transfer}},
    doi = {10.1007/s10009-019-00539-x},
    issn = {1433-2787},
    url = {https://doi.org/10.1007/s10009-019-00539-x},
}
 

 @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},
}
 

 @article{husak_askthecode_2019,
    title = {{AskTheCode: Interactive Call Graph Exploration for Error Fixing and Prevention}},
    author = {Husák, Robert and Kofroň, Jan and Zavoral, Filip},
    year = {2019},
    journal = {{Electronic Communications of the EASST}},
    number = {0},
    doi = {10.14279/tuj.eceasst.77.1109},
    issn = {1863-2122},
    url = {https://journal.ub.tu-berlin.de/eceasst/article/view/1109},
    volume = {77},
    shorttitle = {AskTheCode},
}
 

 @article{jancik_exploiting_2019,
    title = {{Exploiting partial variable assignment in interpolation-based model checking}},
    author = {Jančík, Pavel and Kofroň, Jan and Alt, Leonardo and Fedyukovich, Grigory and Hyvärinen, Antti E. J. and Sharygina, Natasha},
    year = {2019},
    journal = {{Formal Methods in System Design}},
    doi = {10.1007/s10703-019-00342-z},
    issn = {1572-8102},
    url = {https://doi.org/10.1007/s10703-019-00342-z},
}
 

 @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_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},
}
 

 @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},
}
 

 @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},
}
 

 @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},
}
 

 @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},
}
 

 @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},
}