About Me
I am an assistant professor at Faculty of Informatics of Masaryk University, Brno, Czech Republic. Before that, I had been a post-doctoral researcher at the Embedded Systems unit of Fondazione Bruno Kessler, Trento, Italy for three years. My main research interests are SAT/SMT solving of (quantified) bit-vectors and program analysis and verification. Other fields of computer science I am interested in but in which I do not conduct research, include functional programming, and theorem proving.
Contact
Research Interests
- Computational logic
- Satisfiability modulo theories
- Hardware and software verification
Teaching
The courses for which I am either a lecturer or a seminar tutor:
- Algorithms and Data Structures II
- Computability and Complexity
- Mathematical Foundations of Computer Science
- Model Checking
- Non-Imperative Programming
- Satisfiability and Automated Reasoning
- Seminar on Functional Programming
- Teaching Lab
Selected Publications
In reverse chronological order:
M. Jonáš, J. Strejček, M. Trtík. Gray-Box Fuzzing in Local Space. In ASE 2026 (to appear).
M. Jonáš, L. Petřivalská, J. Šárník. On the Complexity of Word-Level Model Checking with Arrays. In FMCAD 2026 (to appear).
A. Štěpková, M. Jonáš, J. Strejček. Program Reversal for Error Reachability Analysis. In ISSRE 2026 (to appear).
O. Huvar, N. Beneš, M. Jonáš, D. Šafránek, S. Pastva. Inference of qualitative models from steady-state data via weighted MaxSMT. In CMSB 2026. Paper
O. Huvar, M. Jonáš, S. Pastva. SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology. In SAT 2026. Paper
M. Jonáš, A. Kučera, V. Kůr, J. Mačák, V. Řehák. Multiagent Stochastic Shortest Path Problem. In IJCAI 2026. Paper (extended version)
J. Horák, M. Jonáš. BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability. In TACAS 2026. Paper
M. Jonáš, A. Kučera, V. Kůr, J. Mačák. Steady-State Strategy Synthesis for Swarms of Autonomous Agents. In IJCAI 2025. Paper
M. Jonáš, J. Strejček, A. Griggio. Combining Symbolic Execution with Predicate Abstraction and CEGAR. In FMCAD 2024. Paper
M. Jonáš, J. Strejček. Truncating abstraction of bit-vector operations for BDD-based SMT solvers. In Theoretical Computer Science 1008. Paper
M. Jonáš, J. Strejček, M. Trtík, L. Urban. Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage. In TACAS 2024. Paper
A. Griggio, M. Jonáš. Kratos2: An SMT-Based Model Checker for Imperative Programs. In CAV 2023. Paper Slides
M. Bozzano, A. Cimatti, A. Griggio, M. Jonáš, G. Kimberly. Analysis of Cyclic Fault Propagation via ASP. In LPNMR 2022. Paper
M. Bozzano, A. Cimatti, A. Griggio, M. Jonáš. Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation. In TACAS 2022. Paper
F. Bigarella, A. Cimatti, A. Griggio, A. Irfan, M. Jonáš, M. Roveri, R. Sebastiani, P. Trentin. Optimization Modulo Non-linear Arithmetic via Incremental Linearization. In FroCoS 2021. Paper
M. Bozzano, A. Cimatti, A. Fernandes Pires, A. Griggio, M. Jonáš, G. Kimberly. Efficient SMT-Based Analysis of Failure Propagation. In CAV 2021. Paper
J. Mrázek, M. Jonáš, J. Barnat. Reconfiguring Metamorphic Robots via SMT: Is It a Viable Way? In IROS 2021. Paper
M. Jonáš, J. Strejček. Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. In SAT 2020. Paper
M. Jonáš, J. Strejček. Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors. In CAV 2019. Paper
M. Jonáš, J. Strejček. Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? In LPAR 2018. Paper
M. Jonáš, J. Strejček. Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers. In ICTAC 2018. Paper
M. Jonáš, J. Strejček. On the complexity of the quantified bit-vector arithmetic with binary encoding. In Information Processing Letters 135. Paper
M. Jonáš, J. Strejček. On Simplification of Formulas with Unconstrained Variables and Quantifiers. In SAT 2017. Paper
M. Jonáš, J. Strejček. Solving quantified bit-vector formulas using binary decision diagrams. In SAT 2016. Paper
You can find all my publications on Google Scholar or DBLP.
Education
| Year | Degree | University |
|---|---|---|
| 2019 | PhD in Theoretical Computer Science | Masaryk University, Brno, Czech Republic |
| 2014 | Master’s degree in Theoretical Computer Science | Masaryk University, Brno, Czech Republic |
| 2012 | Bachelor’s degree in Applied Computer Science | Masaryk University, Brno, Czech Republic |
Academic Service
- SMT-COMP 2026 Organizer
- FMCAD 2026 Program Committee
- FASE 2026 Program Committee
- SMT-COMP 2025 Chair
- FMCAD 2025 Program Committee
- CADE 2025 Program Committee
- ATVA 2024 Artifact Evaluation Committee Co-Chair
- SMT-COMP 2024 Organizer
- TACAS 2024 Artifact Evaluation Committee
- FMCAD 2023 Student Forum Program Committee
- SMT 2023 Program Committe
- CAV 2023 Artifact Evaluation Committee
- TACAS 2023 Artifact Evaluation Committee
- FMCAD 2022 Sponsorship Chair and Webmaster
- CAV 2022 Artifact Evaluation Committee
- SMT 2021 Program Committe
- TACAS 2020 Artifact Evaluation Committee
- VMCAI 2020 Artifact Evaluation Committee
- TACAS 2019 Artifact Evaluation Committee
- TAP 2019 Artifact Evaluation Committee
I have also been a reviewer for JAIR, LICS 2024, CONCUR 2023, TACAS 2023, FMCAD 2022, IJCAR 2022, TACAS 2022, FMCAD 2021, TACAS 2021, CONCUR 2020, LICS 2020, TACAS 2020, TACAS 2019, and STACS 2019.
References
- Alessandro Cimatti, Head of Center for Digital Industry, Fondazione Bruno Kessler
- Alberto Griggio, Senior Researcher, Fondazione Bruno Kessler
- Jan Strejček, Full Professor, Masaryk University