Introducing TakaTuka: a java virtualmachine for motes. - Faisal Aslam; Christian Schindelhauer; Gidon Ernst; Damian Spyra; Jan Meyer; Mohannad Zalloom (SenSys, 2008)

Optimized Java Binary and Virtual Machine for Tiny Motes. - Faisal Aslam; Luminous Fennell; Christian Schindelhauer; Peter Thiemann 001; Gidon Ernst; Elmar Haussmann; Stefan Rührup; Zartash Afzal Uzmi (DCOSS, 2010)

The COST IC0701 Verification Competition 2011. - Thorsten Bormer; Marc Brockschmidt; Dino Distefano; Gidon Ernst; Jean-Christophe Filliâtre; Radu Grigore; Marieke Huisman; Vladimir Klebanov; Claude Marché; Rosemary Monahan; Wojciech Mostowski; Nadia Polikarpova; et al. (FoVeOOS, 2011)

Simulating a Flash File System with CoreASM and Eclipse. - Dominik Haneberg; Maximilian Junker; Gerhard Schellhorn; Wolfgang Reif; Gidon Ernst (GI-Jahrestagung, 2011)

Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving. - Gidon Ernst; Gerhard Schellhorn; Wolfgang Reif (SEFM, 2011)

Interleaved Programs and Rely-Guarantee Reasoning with ITL. - Gerhard Schellhorn; Bogdan Tofan; Gidon Ernst; Wolfgang Reif (TIME, 2011)

A Formal Model of a Virtual Filesystem Switch - Gidon Ernst; Gerhard Schellhorn; Dominik Haneberg; Jörg Pfähler; Wolfgang Reif (SSV, 2012)

Formal Specification of an Erase Block Management Layer for Flash Memory. - Jörg Pfähler; Gidon Ernst; Gerhard Schellhorn; Dominik Haneberg; Wolfgang Reif (Haifa Verification Conference, 2013)

Verification of a Virtual Filesystem Switch. - Gidon Ernst; Gerhard Schellhorn; Dominik Haneberg; Jörg Pfähler; Wolfgang Reif (VSTTE, 2013)

Compositional Verification of a Lock-Free Stack with RGITL. - Bogdan Tofan; Gerhard Schellhorn; Gidon Ernst; Jörg Pfähler; Wolfgang Reif (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Modular Refinement for Submachines of ASMs. - Gidon Ernst; Jörg Pfähler; Gerhard Schellhorn; Wolfgang Reif (ABZ, 2014)

Development of a Verified Flash File System. - Gerhard Schellhorn; Gidon Ernst; Jörg Pfähler; Dominik Haneberg; Wolfgang Reif (ABZ, 2014)

RGITL: A temporal logic framework for compositional reasoning about interleaved programs. - Gerhard Schellhorn; Bogdan Tofan; Gidon Ernst; Jörg Pfähler; Wolfgang Reif (Ann. Math. Artif. Intell., 2014)

Conditional effects in fine-grained region logic. - Yuyan Bao; Gary T. Leavens; Gidon Ernst (FTfJP@ECOOP, 2015)

Inside a Verified Flash File System: Transactions and Garbage Collection. - Gidon Ernst; Jörg Pfähler; Gerhard Schellhorn; Wolfgang Reif (VSTTE, 2015)

Verification of B+ trees by integration of shape analysis and interactive theorem proving. - Gidon Ernst; Gerhard Schellhorn; Wolfgang Reif (Softw. Syst. Model., 2015)

KIV: overview and VerifyThis competition. - Gidon Ernst; Jörg Pfähler; Gerhard Schellhorn; Dominik Haneberg; Wolfgang Reif (Int. J. Softw. Tools Technol. Transf., 2015)

A Relational Encoding for a Clash-Free Subset of ASMs. - Gerhard Schellhorn; Gidon Ernst; Jörg Pfähler; Wolfgang Reif (ABZ, 2016)

Modular, crash-safe refinement for ASMs with submachines. - Gidon Ernst; Jörg Pfähler; Gerhard Schellhorn; Wolfgang Reif (Sci. Comput. Program., 2016)

Modular Verification of Order-Preserving Write-Back Caches. - Jörg Pfähler; Gidon Ernst; Stefan Bodenmüller; Gerhard Schellhorn; Wolfgang Reif (IFM, 2017)

A Verified POSIX-Compliant Flash File System - Modular Verification Technology & Crash Tolerance. - Gidon Ernst (2017)

ARCH-COMP18 Category Report: Results on the Falsification Benchmarks. - Adel Dokhanchi; Shakiba Yaghoubi; Bardh Hoxha; Georgios Fainekos; Gidon Ernst; Zhenya Zhang; Paolo Arcaini; Ichiro Hasuo; Sean Sedwards (ARCH@ADHS, 2018)

In search of perfect users: towards understanding the usability of converged multi-level secure user interfaces. - Abdullah Issa; Toby Murray; Gidon Ernst (OZCHI, 2018)

Two-Layered Falsification of Hybrid Systems guided by Monte Carlo Tree Search. - Zhenya Zhang; Ichiro Hasuo; Gidon Ernst; Sean Sedwards (CoRR, 2018)

Unifying separation logic and region logic to allow interoperability. - Yuyan Bao; Gary T. Leavens; Gidon Ernst (Formal Aspects Comput., 2018)

Symbolic execution for a clash-free subset of ASMs. - Gerhard Schellhorn; Gidon Ernst; Jörg Pfähler; Stefan Bodenmüller; Wolfgang Reif (Sci. Comput. Program., 2018)

Two-Layered Falsification of Hybrid Systems Guided by Monte Carlo Tree Search. - Zhenya Zhang; Gidon Ernst; Sean Sedwards; Paolo Arcaini; Ichiro Hasuo (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2018)

SecCSL: Security Concurrent Separation Logic. - Gidon Ernst; Toby Murray (CAV (2), 2019)

ARCH-COMP 2019 Category Report: Falsification. - Gidon Ernst; Paolo Arcaini; Alexandre Donzé; Georgios Fainekos; Logan Mathesen; Giulia Pedrielli; Shakiba Yaghoubi; Yoriyuki Yamagata; Zhenya Zhang (ARCH@CPSIoTWeek, 2019)

Fast Falsification of Hybrid Systems Using Probabilistically Adaptive Input. - Gidon Ernst; Sean Sedwards; Zhenya Zhang; Ichiro Hasuo (QEST, 2019)

VerifyThis - Verification Competition with a Human Factor. - Gidon Ernst; Marieke Huisman; Wojciech Mostowski; Mattias Ulbrich (TACAS (3), 2019)

ARCH-COMP 2020 Category Report: Falsification. - Gidon Ernst; Paolo Arcaini; Ismail Bennani; Alexandre Donzé; Georgios Fainekos; Goran Frehse; Logan Mathesen; Claudio Menghi; Giulia Pedrielli; Marc Pouzet; Shakiba Yaghoubi; Yoriyuki Yamagata; et al. (ARCH, 2020)

Legion: Best-First Concolic Testing (Competition Contribution). - Dongge Liu; Gidon Ernst; Toby Murray; Benjamin I. P. Rubinstein (FASE, 2020)

LEGION: Best-First Concolic Testing. - Dongge Liu; Gidon Ernst; Toby Murray; Benjamin I. P. Rubinstein (ASE, 2020)

Cuvée: Blending SMT-LIB with Programs and Weakest Preconditions. - Gidon Ernst (CoRR, 2020)

A Complete Approach to Loop Verification with Invariants and Summaries. - Gidon Ernst (CoRR, 2020)

ARCH-COMP 2021 Category Report: Falsification with Validation of Results. - Gidon Ernst; Paolo Arcaini; Ismail Bennani; Aniruddh Chandratre; Alexandre Donzé; Georgios Fainekos; Goran Frehse; Khouloud Gaaloul; Jun Inoue 001; Tanmay Khandait; Logan Mathesen; Claudio Menghi; et al. (ARCH@ADHS, 2021)

Bridging Arrays and ADTs in Recursive Proofs. - Grigory Fedyukovich; Gidon Ernst (TACAS (2), 2021)

Time-Staging Enhancement of Hybrid System Falsification. - Gidon Ernst; Ichiro Hasuo; Zhenya Zhang; Sean Sedwards (SNR, 2021)

Incremental Vulnerability Detection via Back-Propagating Symbolic Execution of Insecurity Separation Logic. - Toby Murray; Pengbo Yan; Gidon Ernst (CoRR, 2021)

Deductive Verification via the Debug Adapter Protocol. - Gidon Ernst; Johannes Blau; Toby Murray (F-IDE@NFM, 2021)

Falsification of Hybrid Systems Using Adaptive Probabilistic Search. - Gidon Ernst; Sean Sedwards; Zhenya Zhang; Ichiro Hasuo (ACM Trans. Model. Comput. Simul., 2021)

ARCH-COMP 2022 Category Report: Falsification with Ubounded Resources. - Gidon Ernst; Paolo Arcaini; Georgios Fainekos; Federico Formica; Jun Inoue 001; Tanmay Khandait; Mohammad Mahdi Mahboob; Claudio Menghi; Giulia Pedrielli; Masaki Waga; Yoriyuki Yamagata; Zhenya Zhang (ARCH@SAFECOMP, 2022)

A Hoare Logic with Regular Behavioral Specifications. - Gidon Ernst; Alexander Knapp; Toby Murray (ISoLA (1), 2022)

Loop Verification with Invariants and Contracts. - Gidon Ernst (VMCAI, 2022)

State Selection Algorithms and Their Impact on The Performance of Stateful Network Protocol Fuzzing. - Dongge Liu; Van-Thuan Pham; Gidon Ernst; Toby Murray; Benjamin I. P. Rubinstein (SANER, 2022)

ARCH-COMP23 Category Report: Falsification. - Claudio Menghi; Paolo Arcaini; Walstan Baptista; Gidon Ernst; Georgios Fainekos; Federico Formica; Sauvik Gon; Tanmay Khandait; Atanu Kundu 002; Giulia Pedrielli; Jarkko Peltomäki; Ivan Porres; et al. (ARCH, 2023)

Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. - Toby Murray; Mukesh Tiwari; Gidon Ernst; David A. Naumann (CCS, 2023)

Compositional Vulnerability Detection with Insecurity Separation Logic. - Toby Murray; Pengbo Yan; Gidon Ernst (ICFEM, 2023)

Verify This: Memcached - A Practical Long-Term Challenge for the Integration of Formal Methods. - Gidon Ernst; Alexander Weigl (iFM, 2023)

Korn - Software Verification with Horn Clauses (Competition Contribution). - Gidon Ernst (TACAS (2), 2023)

The ARCH-COMP Friendly Verification Competition for Continuous and Hybrid Systems. - Alessandro Abate; Matthias Althoff; Lei Bu; Gidon Ernst; Goran Frehse; Luca Geretti; Taylor T. Johnson; Claudio Menghi; Stefan Mitsch; Stefan Schupp; Sadegh Soudjani (TOOLympics@ETAPS, 2023)

The VerifyThis Collaborative Long-Term Challenge Series. - Wolfgang Ahrendt; Gidon Ernst; Paula Herber; Marieke Huisman; Raúl E. Monti; Mattias Ulbrich; Alexander Weigl (TOOLympics@ETAPS, 2023)

Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version). - Toby Murray; Mukesh Tiwari; Gidon Ernst; David A. Naumann (CoRR, 2023)

SpecifyThis Bridging Gaps Between Program Specification Paradigms: Track Introduction. - Gidon Ernst; Paula Herber; Marieke Huisman; Mattias Ulbrich (ISoLA (3), 2024)

Contract-LIB: A Proposal for a Common Interchange Format for Software System Specification. - Gidon Ernst; Wolfram Pfeifer; Mattias Ulbrich (ISoLA (3), 2024)

Eine REIFe Leistung - Anecdotes from Behind the Scenes. - Gidon Ernst; Dominik Haneberg; Matthias Güdemann; Oliver Kosak; Florian Nafz; Hella Ponsar; Gerhard Schellhorn (Go Where the Bugs Are, 2025)

Towards Automatic Structured Inference of Module Abstractions. - Gidon Ernst; Marian Lingsch Rosenfeld (Go Where the Bugs Are, 2025)

Exploring Behaviors of Hybrid Systems via the Voronoi Bias over Output Signals. - Jirí Fejlek; Gidon Ernst (HSCC, 2025)