# Martin Jonáš

I was a Ph.D. student at the Faculty of Informatics, Masaryk University, Brno. My supervisor was Jan Strejček. Since November 2019, I have been post-doctoral researcher at Fondazione Bruno Kessler, Trento, Italy.

## Contact

## Research

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 don't conduct research, include functional programming, (dependent) type theory and theorem proving.
## Projects

**Q3B**: I am the main developer of Q3B, an SMT solver for quantified-bit vector theory based on binary decision diagrams.

## PhD Thesis

## Publications

- M. Jonáš and J. Strejček:
**Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?**, in Proceedings of LPAR 2018, EPiC Series in Computing 57, pages 488-497, 2018. [link, PDF]
- M. Jonáš and J. Strejček:
**Abstraction of Bit-Vector Operations for BDD-based SMT Solvers**, in Proceedings of ICTAC 2018, volume 11187 of LNCS, pages 273-291. Springer, 2018. [DOI link, corrected version PDF, corresponding data]
- M. Jonáš and J. Strejček:
**On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoding**, Information
Processing Letters 135:57-61, 2018. [DOI link, PDF]
- M. Jonáš and J. Strejček:
**On Simplification of Formulas with Unconstrained Variables and Quantifiers**, in Proceedings of SAT 2017, volume 10491 of LNCS, pages 364-379, Springer, 2017. [DOI link, preprint PDF]
- M. Chalupa, M. Vitovská, M. Jonáš, J. Slaby, and J. Strejček:
**Symbiotic 4: Beyond Reachability (Competition Contribution)**, in Proceedings of TACAS 2017, volume 10206 of LNCS, pages 385-389. Springer, 2017. [DOI link, preprint PDF]
- J. Mrázek, M. Jonáš, V. Štill, H. Lauko, J. Barnat:
**Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)**, in Proceedings of TACAS 2017, volume 10206 of LNCS, pages 390-393. Springer, 2017. [DOI link]
- M. Jonáš and J. Strejček:
**Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams**, in Proceedings of SAT 2016, volume 9710 of LNCS, pages 267-283. Springer, 2016. [DOI link, preprint PDF]
- M. Chalupa, M. Jonáš, J. Slaby, J. Strejček, and M. Vitovská:
**Symbiotic 3: New Slicer and Error-Witness Generation (Competition Contribution)**, in Proceedings of TACAS 2016, volume 9636 of LNCS, pages 946-949. Springer, 2016. [DOI link, preprint PDF]

## Teaching

I have been seminar tutor for the following courses at FI MUNI:
## Service

- TACAS 2019, 2020 Artifact Evaluation Committee
- VMCAI 2020 Artifact Evaluation Committee
- TAP 2019 Artifact Evaluation Committee