About Me


I am a post-doctoral researcher at the Embedded Systems unit of Fondazione Bruno Kessler, Trento, Italy. 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.


Research Interests

Selected Publications

In reverse chronological order:

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

  2. 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.

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

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

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

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

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

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

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

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

  11. Martin Jonáš, Jan Strejček. Solving quantified bit-vector formulas using binary decision diagrams. In SAT 2016.

You can find all my publications on Google Scholar or DBLP.


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, IJCAR 2022, TACAS 2022, FMCAD 2021, TACAS 2021, CONCUR 2020, LICS 2020, TACAS 2020, TACAS 2019, and STACS 2019.