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:

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:

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:

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:

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:

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:

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:

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:

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:

2020

Steinhöfel, Dominic

Abstract Execution: Automatically Proving Infinitely Many Programs PhD Thesis

Darmstadt University of Technology, Germany, 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:

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:

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:

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:

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:

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

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

Grebing, Sarah Caecilia

User Interaction in Deductive Interactive Program Verification PhD Thesis

Karlsruhe Institute of Technology, 2019.

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

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:

Steinhöfel, Dominic; Hähnle, Reiner

Modular, Correct Compilation with Automatic Soundness Proofs Proceedings Article

In: Margaria, Tiziana; Steffen, Bernhard (Ed.): Leveraging Applications of Formal Methods, Verification and Validation. Modeling, pp. 424–447, Springer International Publishing, Cham, 2018, ISSN: 0302-9743.

Abstract | BibTeX | Links:

Schiffl, Jonas

Specification and Verification of Hyperledger Fabric Chaincode Masters Thesis

Karlsruhe Institute of Technology, Karlsruhe, Germany, 2018.

BibTeX

85 entries « 1 of 4 »