Publications

This page contains a chronological list of journal and conference papers as well as other documents that are related to the KeY project.

If you want to cite KeY, we recommend to cite the following publication:

Ahrendt, Wolfgang, Beckert, Bernhard, Bubel, Richard, Hähnle, Reiner, Schmitt, Peter H., Ulbrich, Mattias (Ed.): Deductive Software Verification - The KeY Book - From Theory to Practice. Springer, 2016, ISBN: 978-3-319-49811-9.
(BibTeX)

You can also download a BibTeX file with all entries.

85 entries « 1 of 4 »

2022

Klamroth, Jonas; Lanzinger, Florian; Pfeifer, Wolfram; Ulbrich, Mattias

The Karlsruhe Java Verification Suite Book Chapter

In: Ahrendt, Wolfgang; Beckert, Bernhard; Bubel, Richard; Johnsen, Einar Broch (Ed.): The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday, pp. 290–312, Springer International Publishing, 2022, ISBN: 978-3-031-08166-8.

BibTeX | Links:

Boer, Martin; Gouw, Stijn; Klamroth, Jonas; Jung, Christian; Ulbrich, Mattias; Weigl, Alexander

Formal Specification and Verification of JDK’s Identity Hash Map Implementation Proceedings Article

In: Beek, Maurice H.; Monahan, Rosemary (Ed.): 17th International Conference on integrated Formal Methods (iFM 2022), pp. 45–62, Springer, 2022, ISBN: 978-3-031-07727-2.

BibTeX | Links:

Krämer, Jonas; Blatter, Lionel; Darulova, Eva; Ulbrich, Mattias

Inferring Interval-Valued Floating-Point Preconditions Proceedings Article

In: Fisman, Dana; Rosu, Grigore (Ed.): 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), held as part of ETAPS 2022: European Joint Conferences on Theory and Practice of Software, pp. 303–321, Springer, 2022.

BibTeX | Links:

Hähnle, Reiner

Dijkstra's Legacy on Program Verification Book Section

In: Apt, Krzysztof R.; Hoare, Tony (Ed.): Edsger Wybe Dijkstra: His Life, Work, and Legacy, pp. 105–140, ACM / Morgan & Claypool, 2022.

BibTeX | Links:

Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner; Ulbrich, Mattias

Towards a Usable and Sustainable Deductive Verification Tool Proceedings Article

In: Margaria, Tiziana; Steffen, Bernhard (Ed.): Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part II, pp. 281–300, Springer, 2022.

BibTeX | Links:

Tabar, Asmae Heydari; Bubel, Richard; Hähnle, Reiner

Automatic Loop Invariant Generation for Data Dependence Analysis Proceedings Article

In: 10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE@ICSE 2022, Pittsburgh, PA, USA, May 22-23, 2022, pp. 34–45, ACM, 2022.

BibTeX | Links:

Grätz, Lukas; Hähnle, Reiner; Bubel, Richard

Finding Semantic Bugs Fast Proceedings Article

In: Johnsen, Einar Broch; Wimmer, Manuel (Ed.): Fundamental Approaches to Software Engineering - 25th International Conference, FASE 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, pp. 145–154, Springer, 2022.

BibTeX | Links:

2021

Lanzinger, Florian; Weigl, Alexander; Ulbrich, Mattias; Dietl, Werner

Scalability and Precision by Combining Expressive Type Systems and Deductive Verification Journal Article

In: Proceedings of the ACM on programming languages, vol. 5, no. OOPSLA, pp. Article no: 143, 2021, ISSN: 2475-1421, (46.23.01; LK 01).

BibTeX | Links:

Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang

Deductive Verification of Floating-Point Java Programs in KeY Proceedings Article

In: Groote, Jan Friso; Larsen, Kim Guldstrand (Ed.): 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021) held as part of ETAPS 2021: European Joint Conferences on Theory and Practice of Software, pp. 242–261, Springer, 2021.

Abstract | BibTeX | Links:

Albert, Elvira; Hähnle, Reiner; Merayo, Alicia; Steinhöfel, Dominic

Certified Abstract Cost Analysis Proceedings Article

In: Guerra, Esther; Stoelinga, Mariëlle (Ed.): Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, pp. 24–45, Springer, 2021.

BibTeX | Links:

Scaletta, Marco; Hähnle, Reiner; Steinhöfel, Dominic; Bubel, Richard

Delta-based verification of software product families Proceedings Article

In: Tilevich, Eli; Roover, Coen De (Ed.): GPCE '21: Concepts and Experiences, Chicago, IL, USA, October 17 - 18, 2021, pp. 69–82, ACM, 2021.

BibTeX | Links:

Pfeifer, Wolfram; Schiffl, Jonas; Ulbrich, Mattias

Reconstructing Z3 proofs in KeY: There and back again Proceedings Article

In: Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs : 23rd ACM International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2021, co-located with ECOOP/ISSTA 2021, Online, 13 July 2021 - null, pp. 24–31, Association for Computing Machinery (ACM), 2021, ISBN: 978-1-4503-8543-5.

BibTeX | Links:

2020

Ahrendt, Wolfgang; Bubel, Richard

Functional Verification of Smart Contracts via Strong Data Integrity Proceedings Article

In: Margaria, Tiziana; Steffen, Bernhard (Ed.): Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III, pp. 9–24, Springer, 2020.

BibTeX | Links:

Hähnle, Reiner; Tabar, Asmae Heydari; Mazaheri, Arya; Norouzi, Mohammad; Steinhöfel, Dominic; Wolf, Felix

Safer Parallelization Proceedings Article

In: Margaria, Tiziana; Steffen, Bernhard (Ed.): Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part II, pp. 117–137, Springer, 2020.

BibTeX | Links:

Steinhöfel, Dominic

Abstract Execution: Automatically Proving Infinitely Many Programs PhD Thesis

Darmstadt University of Technology, Germany, 2020.

BibTeX | Links:

2019

Hentschel, Martin; Bubel, Richard; Hähnle, Reiner

The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more Journal Article

In: International Journal on Software Tools for Technology Transfer, 2019, ISSN: 1433-2787.

Abstract | BibTeX | Links:

Grebing, Sarah; Klamroth, Jonas; Ulbrich, Mattias

Seamless Interactive Program Verification Proceedings Article

In: 11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019), Springer Publishing, New York City, USA, 2019, (To appear).

BibTeX

Grebing, Sarah Caecilia

User Interaction in Deductive Interactive Program Verification PhD Thesis

Karlsruhe Institute of Technology, 2019.

BibTeX | Links:

Bubel, Richard; Hähnle, Reiner; Tabar, Asmae Heydari

A Program Logic For Dependence Analysis Proceedings Article

In: Ahrendt, Wolfgang; Tarifa, Silvia Lizeth Tapia (Ed.): Integrated Formal Methods, 15th International Conference, iFM, Bergen, Norway, Springer, 2019.

BibTeX

Steinhöfel, Dominic; Hähnle, Reiner

The Trace Modality Proceedings Article

In: Baltag, Alexandru; Barbosa, Luis S (Ed.): 2nd Workshop on Dynamic Logic: New Trends and Applications, Springer, Porto, Portugal, 2019, (Accepted, in print.).

BibTeX

Steinhöfel, Dominic; Hähnle, Reiner

Abstract Execution Proceedings Article

In: ter Beek, Maurice H; McIver, Annabelle; é, Jos (Ed.): Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings, pp. 319–336, Springer, 2019.

BibTeX | Links:

Ahrendt, Wolfgang; Bubel, Richard; Ellul, Joshua; Pace, Gordon J; Pardo, Raul; Rebiscoul, Vincent; Schneider, Gerardo

Verification of Smart Contract Business Logic - Exploiting a Java Source Code Verifier Proceedings Article

In: Hojjat, Hossein; Massink, Mieke (Ed.): Fundamentals of Software Engineering - 8th International Conference, FSEN 2019, Tehran, Iran, May 1-3, 2019, Revised Selected Papers, pp. 228–243, Springer, 2019.

BibTeX | Links:

2018

Beckert, Bernhard; Herda, Mihai; Kobischke, Stefan; Ulbrich, Mattias

Towards a Notion of Coverage for Incomplete Program-Correctness Proofs Proceedings Article

In: Margaria, Tiziana; Steffen, Bernhard (Ed.): 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018), pp. 53–63, Springer, 2018.

BibTeX | Links:

Grebing, Sarah; Luong, An Thuy Tien; Weigl, Alexander

Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned Proceedings Article

In: Jamnik, Mateja; Lüth, Christoph (Ed.): 13th International Workshop on User Interfaces for Theorem Provers (UITP 2018), 2018, (To appear, %snip pdf=https://formal.iti.kit.edu/~grebing/pub/uitp2018.pdf).

BibTeX

Greiner, Simon

A Framework for Non-Interference in Component-Based Systems PhD Thesis

Karlsruhe Institute of Technology, 2018.

BibTeX | Links:

85 entries « 1 of 4 »