About Me
I am an assistant professor at Faculty of Informatics of Masaryk University, Brno, Czech Republic. Before that, I had been a post-doctoral researcher at the Embedded Systems unit of Fondazione Bruno Kessler, Trento, Italy for three years. 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 do not conduct research, include functional programming, and theorem proving.
Contact
Research Interests
- Computational logic
- Satisfiability modulo theories
- Hardware and software verification
Teaching
- Algorithms and Data Structures II
- Computability and Complexity
- Non-Imperative Programming
- Satisfiability and Automated Reasoning
- Seminar on Functional Programming
- Teaching Lab
Selected Publications
In reverse chronological order:
-
Alberto Griggio, Martin Jonáš. Kratos2: An SMT-Based Model Checker for Imperative Programs. In CAV 2023. Paper Slides
-
Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Martin Jonáš, Greg Kimberly. Analysis of Cyclic Fault Propagation via ASP. In LPNMR 2022.
-
Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Martin Jonáš. Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation. In TACAS 2022.
-
Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Martin Jonáš, Marco Roveri, Roberto Sebastiani, Patrick Trentin. Optimization Modulo Non-linear Arithmetic via Incremental Linearization. In FroCoS 2021.
-
Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, Alberto Griggio, Martin Jonáš, Greg Kimberly. Efficient SMT-Based Analysis of Failure Propagation. In CAV 2021.
-
Jan Mrázek, Martin Jonáš, Jiří Barnat. Reconfiguring Metamorphic Robots via SMT: Is It a Viable Way? In IROS 2021.
-
Martin Jonáš, Jan Strejček. Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. In SAT 2020.
-
Martin Jonáš, Jan Strejček. Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors. In CAV 2019.
-
Martin Jonáš, Jan Strejček. Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? In LPAR 2018.
-
Martin Jonáš, Jan Strejček. Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers. In ICTAC 2018.
-
Martin Jonáš, Jan Strejček. On the complexity of the quantified bit-vector arithmetic with binary encoding. In Information Processing Letters 135.
-
Martin Jonáš, Jan Strejček. On Simplification of Formulas with Unconstrained Variables and Quantifiers. In SAT 2017.
-
Martin Jonáš, Jan Strejček. Solving quantified bit-vector formulas using binary decision diagrams. In SAT 2016.
You can find all my publications on Google Scholar or DBLP.
Education
Year | Degree | University |
---|---|---|
2019 | PhD in Theoretical Computer Science | Masaryk University, Brno, Czech Republic |
2014 | Master’s degree in Theoretical Computer Science | Masaryk University, Brno, Czech Republic |
2012 | Bachelor’s degree in Applied Computer Science | Masaryk University, Brno, Czech Republic |
Academic Service
- FMCAD 2023 Student Forum Program Committee
- SMT 2023 Program Committe
- CAV 2023 Artifact Evaluation Committee
- TACAS 2023 Artifact Evaluation Committee
- FMCAD 2022 Sponsorship Chair and Webmaster
- CAV 2022 Artifact Evaluation Committee
- SMT 2021 Program Committe
- TACAS 2020 Artifact Evaluation Committee
- VMCAI 2020 Artifact Evaluation Committee
- TACAS 2019 Artifact Evaluation Committee
- TAP 2019 Artifact Evaluation Committee
I have also been a reviewer for JAIR, CONCUR 2023, TACAS 2023, FMCAD 2022, IJCAR 2022, TACAS 2022, FMCAD 2021, TACAS 2021, CONCUR 2020, LICS 2020, TACAS 2020, TACAS 2019, and STACS 2019.
References
- Alessandro Cimatti, Head of Center for Digital Industry, Fondazione Bruno Kessler
- Alberto Griggio, Senior Researcher, Fondazione Bruno Kessler
- Jan Strejček, Full Professor, Masaryk University