I am a Ph.D. student at the Faculty of Informatics, Masaryk University, Brno. My supervisor is Jan Strejček.
My main research interests are SAT/SMT solving and program analysis and verification. 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]
I have been seminar tutor for the following courses at my faculty: