Gidon Ernst

According to our database, Gidon Ernst authored at least 54 papers between 2008 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Contract-LIB: A Proposal for a Common Interchange Format for Software System Specification.

Gidon Ernst, Wolfram Pfeifer, Mattias Ulbrich

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification, 2024

SpecifyThis Bridging Gaps Between Program Specification Paradigms: Track Introduction.

Gidon Ernst, Paula Herber, Marieke Huisman, Mattias Ulbrich

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification, 2024

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

Korn - Software Verification with Horn Clauses (Competition Contribution).

Gidon Ernst

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Verify This: Memcached - A Practical Long-Term Challenge for the Integration of Formal Methods.

Gidon Ernst, Alexander Weigl

Proceedings of the iFM 2023 - 18th International Conference, 2023

Compositional Vulnerability Detection with Insecurity Separation Logic.

Toby Murray, Pengbo Yan, Gidon Ernst

Proceedings of the Formal Methods and Software Engineering, 2023

Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications.

Toby Murray, Mukesh Tiwari, Gidon Ernst, David A. Naumann

Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, 2023

ARCH-COMP23 Category Report: Falsification.

Claudio Menghi, Paolo Arcaini, Walstan Baptista, Gidon Ernst, Georgios Fainekos, Federico Formica, Sauvik Gon, Tanmay Khandait, Atanu Kundu, Giulia Pedrielli, Jarkko Peltomäki, Ivan Porres, Rajarshi Ray, Masaki Waga, Zhenya Zhang

Proceedings of 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23), 2023

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

Proceedings of the IEEE International Conference on Software Analysis, 2022

Loop Verification with Invariants and Contracts.

Gidon Ernst

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2022

A Hoare Logic with Regular Behavioral Specifications.

Gidon Ernst, Alexander Knapp, Toby Murray

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 2022

ARCH-COMP 2022 Category Report: Falsification with Ubounded Resources.

Gidon Ernst, Paolo Arcaini, Georgios Fainekos, Federico Formica, Jun Inoue, Tanmay Khandait, Mohammad Mahdi Mahboob, Claudio Menghi, Giulia Pedrielli, Masaki Waga, Yoriyuki Yamagata, Zhenya Zhang

Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22), 2022

2021

Falsification of Hybrid Systems Using Adaptive Probabilistic Search.

Gidon Ernst, Sean Sedwards, Zhenya Zhang, Ichiro Hasuo

ACM Trans. Model. Comput. Simul., 2021

Deductive Verification via the Debug Adapter Protocol.

Gidon Ernst, Johannes Blau, Toby Murray

Proceedings of the 6th Workshop on Formal Integrated Development Environment, 2021

Incremental Vulnerability Detection via Back-Propagating Symbolic Execution of Insecurity Separation Logic.

Toby Murray, Pengbo Yan, Gidon Ernst

CoRR, 2021

Time-Staging Enhancement of Hybrid System Falsification.

Gidon Ernst, Ichiro Hasuo, Zhenya Zhang, Sean Sedwards

Proceedings of the Proceedings The 7th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT, 2021

Bridging Arrays and ADTs in Recursive Proofs.

Grigory Fedyukovich, Gidon Ernst

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

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, Tanmay Khandait, Logan Mathesen, Claudio Menghi, Giulia Pedrielli, Marc Pouzet, Masaki Waga, Shakiba Yaghoubi, Yoriyuki Yamagata, Zhenya Zhang

Proceedings of the 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), 2021

2020

A Complete Approach to Loop Verification with Invariants and Summaries.

Gidon Ernst

CoRR, 2020

Cuvée: Blending SMT-LIB with Programs and Weakest Preconditions.

Gidon Ernst

CoRR, 2020

LEGION: Best-First Concolic Testing.

Dongge Liu, Gidon Ernst, Toby Murray, Benjamin I. P. Rubinstein

Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020

Legion: Best-First Concolic Testing (Competition Contribution).

Dongge Liu, Gidon Ernst, Toby Murray, Benjamin I. P. Rubinstein

Proceedings of the Fundamental Approaches to Software Engineering, 2020

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, Zhenya Zhang

Proceedings of the ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), 2020

2019

VerifyThis - Verification Competition with a Human Factor.

Gidon Ernst, Marieke Huisman, Wojciech Mostowski, Mattias Ulbrich

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Fast Falsification of Hybrid Systems Using Probabilistically Adaptive Input.

Gidon Ernst, Sean Sedwards, Zhenya Zhang, Ichiro Hasuo

Proceedings of the Quantitative Evaluation of Systems, 16th International Conference, 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

Proceedings of the ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systemsi, 2019

SecCSL: Security Concurrent Separation Logic.

Gidon Ernst, Toby Murray

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

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

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

Unifying separation logic and region logic to allow interoperability.

Yuyan Bao, Gary T. Leavens, Gidon Ernst

Formal Aspects Comput., 2018

Two-Layered Falsification of Hybrid Systems guided by Monte Carlo Tree Search.

Zhenya Zhang, Ichiro Hasuo, Gidon Ernst, Sean Sedwards

CoRR, 2018

In search of perfect users: towards understanding the usability of converged multi-level secure user interfaces.

Abdullah Issa, Toby Murray, Gidon Ernst

Proceedings of the 30th Australian Conference on Computer-Human Interaction, 2018

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

Proceedings of the ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, 2018

2017

A Verified POSIX-Compliant Flash File System - Modular Verification Technology & Crash Tolerance.

Gidon Ernst

PhD thesis, 2017

Modular Verification of Order-Preserving Write-Back Caches.

Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Integrated Formal Methods - 13th International Conference, 2017

2016

Modular, crash-safe refinement for ASMs with submachines.

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif

Sci. Comput. Program., 2016

A Relational Encoding for a Clash-Free Subset of ASMs.

Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

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

Verification of B⁺ trees by integration of shape analysis and interactive theorem proving.

Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif

Softw. Syst. Model., 2015

Inside a Verified Flash File System: Transactions and Garbage Collection.

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Verified Software: Theories, Tools, and Experiments, 2015

Conditional effects in fine-grained region logic.

Yuyan Bao, Gary T. Leavens, Gidon Ernst

Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, 2015

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

Development of a Verified Flash File System.

Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Dominik Haneberg, Wolfgang Reif

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

Modular Refinement for Submachines of ASMs.

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

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

Verification of a Virtual Filesystem Switch.

Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Formal Specification of an Erase Block Management Layer for Flash Memory.

Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif

Proceedings of the Hardware and Software: Verification and Testing, 2013

2012

A Formal Model of a Virtual Filesystem Switch

Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif

Proceedings of the Proceedings Seventh Conference on Systems Software Verification, 2012

2011

Interleaved Programs and Rely-Guarantee Reasoning with ITL.

Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Wolfgang Reif

Proceedings of the Eighteenth International Symposium on Temporal Representation and Reasoning, 2011

Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving.

Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif

Proceedings of the Software Engineering and Formal Methods - 9th International Conference, 2011

Simulating a Flash File System with CoreASM and Eclipse.

Dominik Haneberg, Maximilian Junker, Gerhard Schellhorn, Wolfgang Reif, Gidon Ernst

Proceedings of the 41. Jahrestagung der Gesellschaft für Informatik, 2011

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, Christoph Scheben, Gerhard Schellhorn, Bogdan Tofan, Julian Tschannen, Mattias Ulbrich

Proceedings of the Formal Verification of Object-Oriented Software, 2011

2010

Optimized Java Binary and Virtual Machine for Tiny Motes.

Faisal Aslam, Luminous Fennell, Christian Schindelhauer, Peter Thiemann, Gidon Ernst, Elmar Haussmann, Stefan Rührup, Zartash Afzal Uzmi

Proceedings of the Distributed Computing in Sensor Systems, 2010

2008

Introducing TakaTuka: a java virtualmachine for motes.

Faisal Aslam, Christian Schindelhauer, Gidon Ernst, Damian Spyra, Jan Meyer, Mohannad Zalloom

Proceedings of the 6th International Conference on Embedded Networked Sensor Systems, 2008