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
PGP fingerprint: F650 D7C8 48AC 23FE 7993 3AA8 02C6 7055 43C8 3F4D

Research interests and activities

• Interpolation-based Code Model Checking
• Static Analysis of Programs

Teaching

• I have no fixed office hours (konzultační hodiny). Please send me an email to arrange for a meeting!

• System Behavior Models and Verification
• Java Labs
• Program Semantics
• Mobile Devices Programming
• Programming in Python

Projects

We are looking for students to join us on the projects below. All levels of studies are highly welcome, starting from the second-year bachelor students.

Current

• AIDE: Advanced Analysis and Verification for Advanced Software

Past

• SNAPPY: Scalable Techniques for Analysis of Complex Properties of Computer Systems
• 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{alali_guide_2022,
    title = {{A guide to design uncertainty-aware self-adaptive components in Cyber--Physical Systems}},
    author = {Al-Ali, Rima and Bulej, Lubomír and Kofroň, Jan and Bureš, Tomáš},
    year = {2022},
    journal = {{Future Generation Computer Systems}},
    doi = {10.1016/j.future.2021.10.027},
    issn = {0167-739X},
    pages = {466--489},
    url = {https://www.sciencedirect.com/science/article/pii/S0167739X21004234},
    volume = {128},
}
 

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

 @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{blicha_summarization_2022,
    title = {{Summarization of branching loops}},
    author = {Blicha, Martin and Kofroň, Jan and Tatarko, William},
    year = {2022},
    booktitle = {{Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing}},
    publisher = {Association for Computing Machinery},
    series = {{SAC '22}},
    location = {New York, NY, USA},
    doi = {10.1145/3477314.3507042},
    isbn = {978-1-4503-8713-2},
    pages = {1808--1816},
    url = {https://doi.org/10.1145/3477314.3507042},
}
 

 @article{blicha_using_2022,
    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 = {2022},
    journal = {{International Journal on Software Tools for Technology Transfer}},
    number = {1},
    doi = {10.1007/s10009-021-00641-z},
    issn = {1433-2787},
    pages = {111--125},
    url = {https://doi.org/10.1007/s10009-021-00641-z},
    volume = {24},
}
 

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

 @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{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{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{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{husak_peachpie_2022,
    title = {{PeachPie: Mature PHP to CLI compiler}},
    author = {Husák, Robert and Míšek, Jakub and Zavoral, Filip and Kofroň, Jan},
    year = {2022},
    journal = {{Journal of Computer Languages}},
    doi = {10.1016/j.cola.2022.101152},
    issn = {2590-1184},
    pages = {1--29},
    url = {https://www.sciencedirect.com/science/article/pii/S2590118422000491},
    shorttitle = {PeachPie},
}
 

 @inproceedings{husak_slicito_2023,
    title = {{Slicito: Using Computational Notebooks for Program Comprehension}},
    author = {Husák, Robert and Kofroň , Jan and Zavoral, Filip},
    year = {2023},
    booktitle = {{2023 IEEE/ACM 31st International Conference on Program Comprehension (ICPC)}},
    doi = {10.1109/ICPC58990.2023.00019},
    pages = {64--68},
    shorttitle = {Slicito},
}
 

 @inproceedings{husak_using_2022,
    title = {{Using Procedure Cloning for Performance Optimization of Compiled Dynamic Languages}},
    author = {Husá k, Robert and Kofroň, Jan and Míšek, Jakub and Zavoral, Filip},
    year = {2022},
    booktitle = {{Proc. of the 17th International Conference on Software Technologies}},
    publisher = {SciTePress},
    doi = {10.5220/0011272300003266},
    isbn = {978-989-758-588-3},
    pages = {175--186},
}
 

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