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. Martin Jonáš, Jan Strejček, Alberto Griggio. Combining Symbolic Execution with Predicate Abstraction and CEGAR. In FMCAD 2024.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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