| 2025 | IFM | Quick Theory Exploration for Algebraic Data Types via Program Transformations. | Gidon Ernst, Grigory Fedyukovich |
| 2024 | ISoLA | SpecifyThis Bridging Gaps Between Program Specification Paradigms: Track Introduction. | Gidon Ernst, Paula Herber, Marieke Huisman, Mattias Ulbrich |
| 2024 | ISoLA | Contract-LIB: A Proposal for a Common Interchange Format for Software System Specification. | Gidon Ernst, Wolfram Pfeifer, Mattias Ulbrich |
| 2023 | CCS | Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. | Toby Murray, Mukesh Tiwari, Gidon Ernst, David A. Naumann |
| 2023 | ICFEM | Compositional Vulnerability Detection with Insecurity Separation Logic. | Toby Murray, Pengbo Yan, Gidon Ernst |
| 2023 | IFM | Verify This: Memcached - A Practical Long-Term Challenge for the Integration of Formal Methods. | Gidon Ernst, Alexander Weigl |
| 2023 | TACAS | Korn - Software Verification with Horn Clauses (Competition Contribution). | Gidon Ernst |
| 2022 | ISoLA | A Hoare Logic with Regular Behavioral Specifications. | Gidon Ernst, Alexander Knapp, Toby Murray |
| 2022 | VMCAI | Loop Verification with Invariants and Contracts. | Gidon Ernst |
| 2021 | TACAS | Bridging Arrays and ADTs in Recursive Proofs. | Grigory Fedyukovich, Gidon Ernst |
| 2020 | FASE | Legion: Best-First Concolic Testing (Competition Contribution). | Dongge Liu, Gidon Ernst, Toby Murray, Benjamin I. P. Rubinstein |
| 2019 | CAV | SecCSL: Security Concurrent Separation Logic. | Gidon Ernst, Toby Murray |
| 2019 | TACAS | VerifyThis - Verification Competition with a Human Factor. | Gidon Ernst, Marieke Huisman, Wojciech Mostowski, Mattias Ulbrich |
| 2018 | OZCHI | In search of perfect users: towards understanding the usability of converged multi-level secure user interfaces. | Abdullah Issa, Toby Murray, Gidon Ernst |
| 2017 | IFM | Modular Verification of Order-Preserving Write-Back Caches. | Jrg Pfhler, Gidon Ernst, Stefan Bodenmller, Gerhard Schellhorn, Wolfgang Reif |
| 2015 | ECOOP | Conditional effects in fine-grained region logic. | Yuyan Bao, Gary T. Leavens, Gidon Ernst |
| 2011 | GI | Simulating a Flash File System with CoreASM and Eclipse. | Dominik Haneberg, Maximilian Junker, Gerhard Schellhorn, Wolfgang Reif, Gidon Ernst |
| 2011 | SEFM | Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving. | Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif |
| 2011 | TIME | Interleaved Programs and Rely-Guarantee Reasoning with ITL. | Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Wolfgang Reif |
| 2010 | DCOSS | Optimized Java Binary and Virtual Machine for Tiny Motes. | Faisal Aslam, Luminous Fennell, Christian Schindelhauer, Peter Thiemann, Gidon Ernst, Elmar Haussmann, Stefan Rhrup, Zartash Afzal Uzmi |
| 2008 | SENSYS | Introducing TakaTuka: a java virtualmachine for motes. | Faisal Aslam, Christian Schindelhauer, Gidon Ernst, Damian Spyra, Jan Meyer, Mohannad Zalloom |