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.

76 entries « 1 of 4 »

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 Inproceedings

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 Inproceedings

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

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 Inproceedings

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 Inproceedings

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 Inproceedings

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 Inproceedings

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 Inproceedings

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 Inproceedings

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 Inproceedings

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 Inproceedings

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 Inproceedings

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

Beckert, Bernhard; Bischof, Simon; Herda, Mihai; Kirsten, Michael; Büning, Marko Kleine

Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow Control Inproceedings

In: Sun, Jing; Sun, Meng (Ed.): 20th International Conference on Formal Engineering Methods - Formal Methods and Software Engineering (ICFEM 2018), pp. 284–300, Springer, Gold Coast, QLD, Australia, 2018.

BibTeX | Links:

Greiner, Simon

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

Karlsruhe Institute of Technology, 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 Inproceedings

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

2017

E., Max; Hecker, Martin; Greiner, Simon; Bao, Kaibin; Yurchenko, Kateryna

Model-Driven Specification and Analysis of Confidentiality in Component-Based Systems Technical Report

Department of Informatics, Karlsruhe Institute of Technology Karlsruhe, no. 2017,12, 2017, ISSN: 2190-4782.

BibTeX | Links:

Schmitt, Peter H.

A Mechanizable First-Order Theory of Ordinals Inproceedings

In: Schmidt, Renate A.; Nalon, Claudia (Ed.): Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, {TABLEAUX} 2017, Brasilia, Brazil, September 25-28, 2017, Proceedings, pp. 331–346, Springer, 2017, ISBN: 978-3-319-66901-4.

Abstract | BibTeX | Links:

Beckert, Bernhard; Schiffl, Jonas; Schmitt, Peter H.; Ulbrich, Mattias

Proving JDK's Dual Pivot Quicksort Correct Inproceedings

In: 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017), 2017, (To appear ).

BibTeX | Links:

de Gouw, Stijn; de Boer, Frank S; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic

Verifying OpenJDK's Sort Method for Generic Collections Journal Article

In: Journal of Automated Reasoning, 2017, ISSN: 1573-0670.

Abstract | BibTeX | Links:

Do, Quoc Huy; Bubel, Richard; Hähnle, Reiner

Inferring Secrets by Guided Experiments Inproceedings

In: Hung, Dang Van; Kapur, Deepak (Ed.): Theoretical Aspects of Computing -- ICTAC 2017: 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings, pp. 269–287, Springer International Publishing, Cham, 2017.

BibTeX | Links:

Steinhöfel, Dominic; Wasser, Nathan

A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows Inproceedings

In: Polikarpova, Nadia; Schneider, Steve (Ed.): Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings, pp. 279–294, Springer, 2017.

BibTeX | Links:

76 entries « 1 of 4 »