About Me

avatar

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

Teaching

The courses for which I am either a lecturer or a seminar tutor:

Selected Publications

In reverse chronological order:

  1. Adéla Štěpková, Martin Jonáš, Jan Strejček. Program Reversal for Error Reachability Analysis. In ISSRE 2026 (to appear).

  2. Ondřej Huvar, Nikola Beneš, Martin Jonáš, David Šafránek, Samuel Pastva. Inference of qualitative models from steady-state data via weighted MaxSMT. In CMSB 2026 (to appear).

  3. Ondřej Huvar, Martin Jonáš, Samuel Pastva. SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology. In SAT 2026 (to appear).

  4. Martin Jonáš, Antonín Kučera, Vojtěch Kůr, Jan Mačák, Vojtěch Řehák. Multiagent Stochastic Shortest Path Problem. In IJCAI 2026 (to appear). Paper (extended version)

  5. Jakub Horák, Martin Jonáš. BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability. In TACAS 2026. Paper

  6. Martin Jonáš, Antonín Kučera, Vojtěch Kůr, Jan Mačák. Steady-State Strategy Synthesis for Swarms of Autonomous Agents. In IJCAI 2025. Paper

  7. Martin Jonáš, Jan Strejček, Alberto Griggio. Combining Symbolic Execution with Predicate Abstraction and CEGAR. In FMCAD 2024. Paper

  8. Martin Jonáš, Jan Strejček. Truncating abstraction of bit-vector operations for BDD-based SMT solvers. In Theoretical Computer Science 1008. Paper

  9. Martin Jonáš, Jan Strejček, Marek Trtík, Lukáš Urban. Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage. In TACAS 2024. Paper

  10. Alberto Griggio, Martin Jonáš. Kratos2: An SMT-Based Model Checker for Imperative Programs. In CAV 2023. Paper Slides

  11. Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Martin Jonáš, Greg Kimberly. Analysis of Cyclic Fault Propagation via ASP. In LPNMR 2022. Paper

  12. Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Martin Jonáš. Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation. In TACAS 2022. Paper

  13. Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Martin Jonáš, Marco Roveri, Roberto Sebastiani, Patrick Trentin. Optimization Modulo Non-linear Arithmetic via Incremental Linearization. In FroCoS 2021. Paper

  14. Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, Alberto Griggio, Martin Jonáš, Greg Kimberly. Efficient SMT-Based Analysis of Failure Propagation. In CAV 2021. Paper

  15. Jan Mrázek, Martin Jonáš, Jiří Barnat. Reconfiguring Metamorphic Robots via SMT: Is It a Viable Way? In IROS 2021. Paper

  16. Martin Jonáš, Jan Strejček. Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. In SAT 2020. Paper

  17. Martin Jonáš, Jan Strejček. Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors. In CAV 2019. Paper

  18. Martin Jonáš, Jan Strejček. Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? In LPAR 2018. Paper

  19. Martin Jonáš, Jan Strejček. Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers. In ICTAC 2018. Paper

  20. Martin Jonáš, Jan Strejček. On the complexity of the quantified bit-vector arithmetic with binary encoding. In Information Processing Letters 135. Paper

  21. Martin Jonáš, Jan Strejček. On Simplification of Formulas with Unconstrained Variables and Quantifiers. In SAT 2017. Paper

  22. Martin Jonáš, Jan 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

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