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
• Programming in Python

Projects

Current

• SNAPPY: Scalable Techniques for Analysis of Complex Properties of Computer Systems

Past

• ROBUST: Verification and Bug-Hunting For Advanced Software
• 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.

 @article{bures_targeting_2021,
    title = {{Targeting uncertainty in smart CPS by confidence-based logic}},
    author = {Bureš, Tomáš and Hnětynka, Petr and Plášil, František and Škoda, Dominik and Kofroň, Jan and Ali, Rima Al and Gerostathopoulos, Ilias},
    year = {2021},
    journal = {{Journal of Systems and Software}},
    doi = {10.1016/j.jss.2021.111065},
    issn = {01641212},
    url = {https://linkinghub.elsevier.com/retrieve/pii/S016412122100162X},
    volume = {181},
}
 

 @article{blicha_using_2021,
    title = {{Using linear algebra in decomposition of Farkas interpolants}},
    author = {Blicha, Martin and Hyvärinen, Antti E. J. and Kofroň, Jan and Sharygina, Natasha},
    year = {2021},
    journal = {{International Journal on Software Tools for Technology Transfer}},
    doi = {10.1007/s10009-021-00641-z},
    issn = {1433-2787},
    url = {https://doi.org/10.1007/s10009-021-00641-z},
}
 

 @article{bures_language_2020,
    title = {{A language and framework for dynamic component ensembles in smart systems}},
    author = {Bures, Tomas and Gerostathopoulos, Ilias and Hnetynka, Petr and Plasil, Frantisek and Krijt, Filip and Vinarek, Jiri and Kofron, Jan},
    year = {2020},
    journal = {{International Journal on Software Tools for Technology Transfer}},
    number = {4},
    doi = {10.1007/s10009-020-00558-z},
    issn = {1433-2779, 1433-2787},
    pages = {497--509},
    url = {http://link.springer.com/10.1007/s10009-020-00558-z},
    volume = {22},
}
 

 @inproceedings{husak_optimizing_2020,
    title = {{Optimizing Transformations of Dynamic Languages Compiled to Intermediate Representations}},
    author = {Husák, Robert and Zavoral, Filip and Kofroň, Jan},
    year = {2020},
    booktitle = {{2020 International Symposium on Theoretical Aspects of Software Engineering}},
    publisher = {The Institute of Electrical and Electronics Engineers, Inc.},
    isbn = {978-1-72814-086-5},
    pages = {145--152},
    url = {https://conferences.computer.org/tasepub/pdfs/TASE2020-5dIM65sOjiD1UBvCxlbFGt/408600a145/408600a145.pdf},
}
 

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

 @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}},
    number = {1},
    doi = {10.1007/s10703-019-00342-z},
    issn = {1572-8102},
    pages = {33--71},
    url = {https://doi.org/10.1007/s10703-019-00342-z},
    volume = {55},
}
 

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

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

 @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},
    volume = {29},
}