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.
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.
- 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: 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]
I have been seminar tutor for the following courses at FI MUNI:
- TACAS 2019, 2020 Artifact Evaluation Committee
- VMCAI 2020 Artifact Evaluation Committee
- TAP 2019 Artifact Evaluation Committee