**Office:**C415 (ideally after prior email notification)**Phone to office:**(+420) 54949 1879**Email:**martin.jonas@mail.muni.cz

Other fields of computer science I am interested in but I don't conduct research at, include functional programming, (dependent) type theory and theorem proving.

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

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

- Automata, Grammars, and Complexity (2014–2016)
- Automata and Grammars (2016–now)
- Non-Imperative Programming (2015–now)
- Formal Languages and Automata (2016–now)
- Computational Logic (2017–now)