| 2026 | FM | Quantitative Monitoring of Signal First-Order Logic. | Marek Chalupa, Thomas A. Henzinger, N. Ege Sara, Emily Yu |
| 2025 | ICSE | Cooperative Software Verification via Dynamic Program Splitting. | Cedric Richter, Marek Chalupa, Marie-Christine Jakobs, Heike Wehrheim |
| 2025 | RV | Monitoring Hypernode Logic Over Infinite Domains. | Marek Chalupa, Thomas A. Henzinger, Ana Oliveira da Costa |
| 2025 | TACAS | Automating the Analysis of Quantitative Automata with QuAK. | Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Sara |
| 2025 | TACAS | BUBAAK: Dynamic Cooperative Verification - (Competition Contribution). | Marek Chalupa, Cedric Richter |
| 2024 | IFM | Monitoring Extended Hypernode Logic. | Marek Chalupa, Thomas A. Henzinger, Ana Oliveira da Costa |
| 2024 | ISoLA | QuAK: Quantitative Automata Kit. | Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Sara |
| 2024 | TACAS | Bubaak-SpLit: Split what you cannot verify (Competition contribution). | Marek Chalupa, Cedric Richter |
| 2023 | FASE | Vamos: Middleware for Best-Effort Third-Party Monitoring. | Marek Chalupa, Fabian Muehlboeck, Stefanie Muroya Lei, Thomas A. Henzinger |
| 2023 | RV | Monitoring Hyperproperties with Prefix Transducers. | Marek Chalupa, Thomas A. Henzinger |
| 2023 | TACAS | Bubaak: Runtime Monitoring of Program Verifiers - (Competition Contribution). | Marek Chalupa, Thomas A. Henzinger |
| 2022 | TACAS | Symbiotic-Witch: A Klee-Based Violation Witness Checker - (Competition Contribution). | Paulna Ayaziov, Marek Chalupa, Jan Strejcek |
| 2022 | TACAS | Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding - (Competition Contribution). | Marek Chalupa, Vincent Mihalkovic, Anna Rechtckov, Luks Zaoral, Jan Strejcek |
| 2021 | CAV | Fast Computation of Strong Control Dependencies. | Marek Chalupa, David Klaska, Jan Strejcek, Luks Tomovic |
| 2021 | FASE | Symbiotic 8: Parallel and Targeted Test Generation - (Competition Contribution). | Marek Chalupa, Jakub Novk, Jan Strejcek |
| 2021 | SAS | Backward Symbolic Execution with Loop Folding. | Marek Chalupa, Jan Strejcek |
| 2021 | TACAS | Symbiotic 8: Beyond Symbolic Execution - (Competition Contribution). | Marek Chalupa, Toms Jasek, Jakub Novk, Anna Rechtckov, Veronika Sokov, Jan Strejcek |
| 2020 | ATVA | DG: Analysis and Slicing of LLVM Bitcode. | Marek Chalupa |
| 2020 | TACAS | Symbiotic 7: Integration of Predator and More - (Competition Contribution). | Marek Chalupa, Toms Jasek, Luks Tomovic, Martin Hruska, Veronika Sokov, Paulna Ayaziov, Jan Strejcek, Toms Vojnar |
| 2019 | IFM | Evaluation of Program Slicing in Software Verification. | Marek Chalupa, Jan Strejcek |
| 2018 | TACAS | SYMBIOTIC 5: Boosted Instrumentation - (Competition Contribution). | Marek Chalupa, Martina Vitovsk, Jan Strejcek |
| 2017 | TACAS | Symbiotic 4: Beyond Reachability - (Competition Contribution). | Marek Chalupa, Martina Vitovsk, Martin Jons, Jiri Slaby, Jan Strejcek |
| 2016 | TACAS | Symbiotic 3: New Slicer and Error-Witness Generation - (Competition Contribution). | Marek Chalupa, Martin Jons, Jiri Slaby, Jan Strejcek, Martina Vitovsk |