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

- M. Jonas and J. Strejcek:
**Abstraction of Bit-Vector Operations for BDD-based SMT Solvers**, in Proceedings of ICTAC 2018, LNCS. Springer, 2018. To appear. - M. Jonas and J. Strejcek:
**On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoding**, Information Processing Letters 135:57-61, 2018. [DOI link, PDF] - M. Jonas and J. Strejcek:
**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. Vitovska, M. Jonas, J. Slaby, and J. Strejcek:
**Symbiotic 4: Beyond Reachability (Competition Contribution)**, in Proceedings of TACAS 2017, volume 10206 of LNCS, pages 385-389. Springer, 2017. [DOI link, preprint PDF] - M. Jonas and J. Strejcek:
**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. Jonas, J. Slaby, J. Strejcek, and M. Vitovska:
**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)