Jan Kofroň

Associate 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. Please send me an email in advance!

• System Behavior Models and Verification
• Java Labs
• Program Semantics
• Developing Applications for Mobile Devices

Projects

Current

• ROBUST: Verification and Bug-Hunting For Advanced Software
• SNAPPY: Scalable Techniques for Analysis of Complex Properties of Computer Systems

Past

• The Weverca project
• 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.

 @inproceedings{husak_handling_2019,
    title = {{Handling Heap Data Structures in Backward Symbolic Execution}},
    author = {Husák, Robert and Kofroň, Jan and Zavoral, Filip},
    year = {2019},
    booktitle = {{Pre-proceedings for TAPAS 2019}},
    location = {Portugal},
    url = {https://staticanalysis.org/tapas2019/talks/tapas19-pre.pdf},
}
 

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