Welcome

I am a formal verification researcher, especially interested in formal verification of machine-code systems, for which I am developing the tool machine-check. I am also interested in processor design and signal processing (both analog and digital), especially in the context of audio.

I have succesfully finished my doctorate at the Czech Technical University in Prague in 2025. I am currently looking for a postdoc position. My Curriculum Vitae is available here.

News

• 06-15-2025: I have released the version 0.5.0 of machine-check with new features such as support for division operations and an experimental dual-interval domain.
• 06-06-2025: I have successfully defended my dissertation thesis and acquired the title of doctor (Ph.D.) at the Czech Technical University in Prague.
• 31-03-2025: I have released the version 0.4.0 of machine-check and created a new website for it.
• 01-01-2025: My project machine-check has been selected for the NLnet NGI Zero Grant.

Projects

I am the creator of machine-check, a formal verification tool for digital systems. Intended especially for verification of machine-code programs by writing a processor description. Feasibility of verification is enhanced via Three-valued Abstraction Refinement. I have created a processor description for the AVR ATmega328P microcontroller used in Arduino UNO R3, available as machine-check-avr.

I also contributed to the CPAchecker software verification tool. I added support for the standard C functions memset, memcpy, and memmove, and improved the handling of quantifiers.

Publications

• J. Onderka. Formal Verification of Machine-Code Systems by Translation of Simulable Descriptions. Proceedings of the 13th Mediterranean Conference on Embedded Computing (MECO 2024), Institute of Electrical and Electronic Engineers, Budva, Montenegro, 2024. DOI: 10.1109/MECO62516.2024.10577942.
• J. Onderka, S. Ratschan. Fast Three-Valued Abstract Bit-Vector Arithmetic. Proceedings of the 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022), pp. 242-262, 2022. Springer Nature Switzerland, Cham, 2022. ISBN: 978-3-030-94583-1. DOI: 10.1007/978-3-030-94583-1_12

Preprints

• J. Onderka, S. Ratschan. Input-based Three-valued Abstraction Refinement (preprint). arXiv:2408.12668 [cs.LO]. https://arxiv.org/abs/2408.12668.

Awards

• The 13th Mediterranean Conference on Embedded Computing (MECO 2024), The Best Paper in Software and Algorithms (Formal Verification of Machine-Code Systems by Translation of Simulable Descriptions).

Contact

You can contact me at [email protected]. For added privacy and security, consider using PGP. My public PGP key is available here. The fingerprint is:

8855 8822 0CF1 8429 0712  D5F5 BA33 C977 4C99 DCDD