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 am currently employed as a postdoctoral researcher at the Chair of Computer Architecture at the University of Freiburg.
My Curriculum Vitae is available here.
News
- 2026-01-13: I have presented the paper Input-based Three-Valued Abstraction Refinement (collaboration with Stefan Ratschan) at the VMCAI 2026 conference!
- 2025-12-17: Version 0.7.1 of machine-check released with a proof-of-concept RISC-V system crate and other minor improvements.
- 2025-10-29: Version 0.7.0 of machine-check released with more expressive properties and a new equality domain.
- 2025-09-01: I am now working at the University of Freiburg! Many exciting things await.
- 2025-08-26: Version 0.6.0 of machine-check released with support for parametric verification and μ-calculus properties.
- 2025-06-15: Version 0.5.0 of machine-check released with new features such as support for division operations and an experimental dual-interval domain.
- 2025-06-06: I have successfully defended my dissertation thesis and acquired the title of doctor (Ph.D.) at the Czech Technical University in Prague.
- 2025-03-31: Version 0.4.0 of machine-check released with a new website created for it.
- 2025-01-01: 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, S. Ratschan. Input-based Three-Valued Abstraction Refinement. 27th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2026). | [pdf] [doi] [arxiv] [artefact] [slides] |
| J. Onderka. Formal Verification of Machine-Code Systems by Translation of Simulable Descriptions. 13th Mediterranean Conference on Embedded Computing (MECO 2024). | [pdf] [doi] [slides] |
| J. Onderka, S. Ratschan. Fast Three-Valued Abstract Bit-Vector Arithmetic. 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022). | [pdf] [doi] [artefact] [slides] |
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