Gidon Ernst - RankMe

71 papers A* 2A 1B 7C 5Misc 2Journal 21Unranked 29

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	A Weakest Precondition Calculus for Programs and Linear Temporal Specifications. CoRR Gidon Ernst
2026	—	`ed.`	Model Checking Software - 31st International Symposium, SPIN 2025, Hamilton, ON, Canada, May 7-8, 2025, Proceedings SPIN Gidon Ernst, Kristin Yvonne Rozier
2025	—	`conf`	Eine REIFe Leistung - Anecdotes from Behind the Scenes. Go Where the Bugs Are Gidon Ernst, Dominik Haneberg, Matthias Güdemann, Oliver Kosak, Florian Nafz, Hella Ponsar, Gerhard Schellhorn
2025	—	`conf`	Exploring Behaviors of Hybrid Systems via the Voronoi Bias over Output Signals. HSCC Jirí Fejlek, Gidon Ernst
2025	—	`ed.`	Go Where the Bugs Are - Essays Dedicated to Wolfgang Reif on the Occasion of His 65th Birthday Go Where the Bugs Are Gidon Ernst, Matthias Güdemann, Alexander Knapp, Florian Nafz, Frank Ortmeier, Hella Ponsar, Gerhard Schellhorn, Alexander Schiendorfer
2025	B	`conf`	Quick Theory Exploration for Algebraic Data Types via Program Transformations. iFM Gidon Ernst, Grigory Fedyukovich
2025	J	`jnl`	SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks. CoRR Dirk Beyer, Gidon Ernst, Martin Jonás, Marian Lingsch Rosenfeld
2025	—	`conf`	Towards Automatic Structured Inference of Module Abstractions. Go Where the Bugs Are Gidon Ernst, Marian Lingsch Rosenfeld
2024	—	`conf`	Contract-LIB: A Proposal for a Common Interchange Format for Software System Specification. ISoLA (3) Gidon Ernst, Wolfram Pfeifer, Mattias Ulbrich
2024	J	`jnl`	Exploring Behaviors of Hybrid Systems via the Voronoi Bias over Output Signals. CoRR Gidon Ernst, Jirí Fejlek
2024	—	`conf`	SpecifyThis Bridging Gaps Between Program Specification Paradigms: Track Introduction. ISoLA (3) Gidon Ernst, Paula Herber, Marieke Huisman, Mattias Ulbrich
2023	—	`conf`	ARCH-COMP23 Category Report: Falsification. ARCH 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
2023	J	`jnl`	Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version). CoRR Toby Murray, Mukesh Tiwari, Gidon Ernst, David A. Naumann
2023	A*	`conf`	Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. CCS Toby Murray, Mukesh Tiwari, Gidon Ernst, David A. Naumann
2023	C	`conf`	Compositional Vulnerability Detection with Insecurity Separation Logic. ICFEM Toby Murray, Pengbo Yan, Gidon Ernst
2023	—	`conf`	Korn - Software Verification with Horn Clauses (Competition Contribution). TACAS (2) Gidon Ernst
2023	—	`conf`	The ARCH-COMP Friendly Verification Competition for Continuous and Hybrid Systems. TOOLympics@ETAPS Alessandro Abate, Matthias Althoff, Lei Bu, Gidon Ernst, Goran Frehse, Luca Geretti, Taylor T. Johnson, Claudio Menghi, Stefan Mitsch, Stefan Schupp, Sadegh Soudjani
2023	—	`conf`	The VerifyThis Collaborative Long-Term Challenge Series. TOOLympics@ETAPS Wolfgang Ahrendt, Gidon Ernst, Paula Herber, Marieke Huisman, Raúl E. Monti, Mattias Ulbrich, Alexander Weigl
2023	B	`conf`	Verify This: Memcached - A Practical Long-Term Challenge for the Integration of Formal Methods. iFM Gidon Ernst, Alexander Weigl
2022	—	`conf`	A Hoare Logic with Regular Behavioral Specifications. ISoLA (1) Gidon Ernst, Alexander Knapp, Toby Murray
2022	J	`jnl`	A Hoare Logic with Regular Behavioral Specifications. CoRR Gidon Ernst, Alexander Knapp, Toby Murray
2022	—	`conf`	ARCH-COMP 2022 Category Report: Falsification with Ubounded Resources. ARCH@SAFECOMP 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
2022	B	`conf`	Loop Verification with Invariants and Contracts. VMCAI Gidon Ernst
2022	A	`conf`	State Selection Algorithms and Their Impact on The Performance of Stateful Network Protocol Fuzzing. SANER Dongge Liu, Van-Thuan Pham, Gidon Ernst, Toby Murray, Benjamin I. P. Rubinstein
2021	—	`conf`	ARCH-COMP 2021 Category Report: Falsification with Validation of Results. ARCH@ADHS 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
2021	—	`conf`	Bridging Arrays and ADTs in Recursive Proofs. TACAS (2) Grigory Fedyukovich, Gidon Ernst
2021	—	`conf`	Deductive Verification via the Debug Adapter Protocol. F-IDE@NFM Gidon Ernst, Johannes Blau, Toby Murray
2021	J	`jnl`	Falsification of Hybrid Systems Using Adaptive Probabilistic Search. ACM Trans. Model. Comput. Simul. Gidon Ernst, Sean Sedwards, Zhenya Zhang, Ichiro Hasuo
2021	J	`jnl`	Incremental Vulnerability Detection via Back-Propagating Symbolic Execution of Insecurity Separation Logic. CoRR Toby Murray, Pengbo Yan, Gidon Ernst
2021	J	`jnl`	State Selection Algorithms and Their Impact on The Performance of Stateful Network Protocol Fuzzing. CoRR Dongge Liu, Van-Thuan Pham, Gidon Ernst, Toby Murray, Benjamin I. P. Rubinstein
2021	—	`conf`	Time-Staging Enhancement of Hybrid System Falsification. SNR Gidon Ernst, Ichiro Hasuo, Zhenya Zhang, Sean Sedwards
2020	J	`jnl`	A Complete Approach to Loop Verification with Invariants and Summaries. CoRR Gidon Ernst
2020	—	`conf`	ARCH-COMP 2020 Category Report: Falsification. ARCH 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
2020	J	`jnl`	Cuvée: Blending SMT-LIB with Programs and Weakest Preconditions. CoRR Gidon Ernst
2020	A*	`conf`	LEGION: Best-First Concolic Testing. ASE Dongge Liu, Gidon Ernst, Toby Murray, Benjamin I. P. Rubinstein
2020	B	`conf`	Legion: Best-First Concolic Testing (Competition Contribution). FASE Dongge Liu, Gidon Ernst, Toby Murray, Benjamin I. P. Rubinstein
2020	J	`jnl`	Legion: Best-First Concolic Testing. CoRR Dongge Liu, Gidon Ernst, Toby Murray, Benjamin I. P. Rubinstein
2019	—	`conf`	ARCH-COMP 2019 Category Report: Falsification. ARCH@CPSIoTWeek Gidon Ernst, Paolo Arcaini, Alexandre Donzé, Georgios Fainekos, Logan Mathesen, Giulia Pedrielli, Shakiba Yaghoubi, Yoriyuki Yamagata, Zhenya Zhang
2019	—	`conf`	Fast Falsification of Hybrid Systems Using Probabilistically Adaptive Input. QEST Gidon Ernst, Sean Sedwards, Zhenya Zhang, Ichiro Hasuo
2019	—	`ed.`	Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, FTfJP@ECOOP 2019, London, United Kingdom, July 15, 2019 FTfJP@ECOOP Toby Murray, Gidon Ernst
2019	—	`conf`	SecCSL: Security Concurrent Separation Logic. CAV (2) Gidon Ernst, Toby Murray
2019	—	`conf`	VerifyThis - Verification Competition with a Human Factor. TACAS (3) Gidon Ernst, Marieke Huisman, Wojciech Mostowski, Mattias Ulbrich
2018	—	`conf`	ARCH-COMP18 Category Report: Results on the Falsification Benchmarks. ARCH@ADHS Adel Dokhanchi, Shakiba Yaghoubi, Bardh Hoxha, Georgios Fainekos, Gidon Ernst, Zhenya Zhang, Paolo Arcaini, Ichiro Hasuo, Sean Sedwards
2018	J	`jnl`	Fast Falsification of Hybrid Systems using Probabilistically Adaptive Input. CoRR Gidon Ernst, Sean Sedwards, Zhenya Zhang, Ichiro Hasuo
2018	Misc	`conf`	In search of perfect users: towards understanding the usability of converged multi-level secure user interfaces. OZCHI Abdullah Issa, Toby Murray, Gidon Ernst
2018	J	`jnl`	Symbolic execution for a clash-free subset of ASMs. Sci. Comput. Program. Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Stefan Bodenmüller, Wolfgang Reif
2018	—	`conf`	Time-Staging Enhancement of Hybrid System Falsification. MT@CPSWeek Zhenya Zhang, Gidon Ernst, Ichiro Hasuo, Sean Sedwards
2018	J	`jnl`	Two-Layered Falsification of Hybrid Systems Guided by Monte Carlo Tree Search. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Zhenya Zhang, Gidon Ernst, Sean Sedwards, Paolo Arcaini, Ichiro Hasuo
2018	J	`jnl`	Two-Layered Falsification of Hybrid Systems guided by Monte Carlo Tree Search. CoRR Zhenya Zhang, Ichiro Hasuo, Gidon Ernst, Sean Sedwards
2018	J	`jnl`	Unifying separation logic and region logic to allow interoperability. Formal Aspects Comput. Yuyan Bao, Gary T. Leavens, Gidon Ernst
2017	—	`—`	A Verified POSIX-Compliant Flash File System - Modular Verification Technology & Crash Tolerance. Gidon Ernst
2017	B	`conf`	Modular Verification of Order-Preserving Write-Back Caches. IFM Jörg Pfähler, Gidon Ernst, Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif
2016	C	`conf`	A Relational Encoding for a Clash-Free Subset of ASMs. ABZ Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif
2016	J	`jnl`	Modular, crash-safe refinement for ASMs with submachines. Sci. Comput. Program. Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif
2015	—	`conf`	Conditional effects in fine-grained region logic. FTfJP@ECOOP Yuyan Bao, Gary T. Leavens, Gidon Ernst
2015	—	`conf`	Inside a Verified Flash File System: Transactions and Garbage Collection. VSTTE Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif
2015	J	`jnl`	KIV: overview and VerifyThis competition. Int. J. Softw. Tools Technol. Transf. Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif
2015	J	`jnl`	Verification of B Softw. Syst. Model. Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif
2014	C	`conf`	Development of a Verified Flash File System. ABZ Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Dominik Haneberg, Wolfgang Reif
2014	C	`conf`	Modular Refinement for Submachines of ASMs. ABZ Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Wolfgang Reif
2014	J	`jnl`	RGITL: A temporal logic framework for compositional reasoning about interleaved programs. Ann. Math. Artif. Intell. Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Jörg Pfähler, Wolfgang Reif
2013	J	`jnl`	Compositional Verification of a Lock-Free Stack with RGITL. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Bogdan Tofan, Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif
2013	—	`conf`	Formal Specification of an Erase Block Management Layer for Flash Memory. Haifa Verification Conference Jörg Pfähler, Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif
2013	—	`conf`	Verification of a Virtual Filesystem Switch. VSTTE Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif
2012	—	`conf`	A Formal Model of a Virtual Filesystem Switch SSV Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, Wolfgang Reif
2011	C	`conf`	Interleaved Programs and Rely-Guarantee Reasoning with ITL. TIME Gerhard Schellhorn, Bogdan Tofan, Gidon Ernst, Wolfgang Reif
2011	—	`conf`	Simulating a Flash File System with CoreASM and Eclipse. GI-Jahrestagung Dominik Haneberg, Maximilian Junker, Gerhard Schellhorn, Wolfgang Reif, Gidon Ernst
2011	—	`conf`	The COST IC0701 Verification Competition 2011. FoVeOOS 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
2011	B	`conf`	Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving. SEFM Gidon Ernst, Gerhard Schellhorn, Wolfgang Reif
2010	B	`conf`	Optimized Java Binary and Virtual Machine for Tiny Motes. DCOSS Faisal Aslam, Luminous Fennell, Christian Schindelhauer, Peter Thiemann, Gidon Ernst, Elmar Haussmann, Stefan Rührup, Zartash Afzal Uzmi
2008	Misc	`conf`	Introducing TakaTuka: a java virtualmachine for motes. SenSys Faisal Aslam, Christian Schindelhauer, Gidon Ernst, Damian Spyra, Jan Meyer, Mohannad Zalloom