# Martin Jonáš

I am a Ph.D. student at the Faculty of Informatics, Masaryk University, Brno. My supervisor is Jan Strejček.

## Contact

## Research

My main research interests are SAT/SMT solving 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.

## Publications

- M. Jonáš and J. Strejček:
**Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes** (Experimental Paper), in Proceedings of LPAR 2018, EPiC Series in Computing, 2018. To appear.
- M. Jonáš and J. Strejček:
**Abstraction of Bit-Vector Operations for BDD-based SMT Solvers**, in Proceedings of ICTAC 2018, LNCS. Springer, 2018. To appear.
- 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 my faculty:
## Service

- TACAS 2019 Artifact Evaluation Committee