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, 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.

70 entries « 1 of 7 »
Hentschel, Martin; Bubel, Richard; Hähnle, Reiner: The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more. International Journal on Software Tools for Technology Transfer, 2019, ISSN: 1433-2787. (Type: Journal Article | 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. 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. (Type: Inproceedings | BibTeX | Links: )
Steinhöfel, Dominic; Hähnle, Reiner: Abstract Execution. 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. (Type: Inproceedings | BibTeX | Links: )
Steinhöfel, Dominic; Hähnle, Reiner: The Trace Modality. Baltag, Alexandru; Barbosa, Luis S (Ed.): 2nd Workshop on Dynamic Logic: New Trends and Applications, Springer, Porto, Portugal, Forthcoming, (Accepted, in print.). (Type: Inproceedings | BibTeX)
Bubel, Richard; Hähnle, Reiner; Tabar, Asmae Heydari: A Program Logic For Dependence Analysis. Ahrendt, Wolfgang; Tarifa, Silvia Lizeth Tapia (Ed.): Integrated Formal Methods, 15th International Conference, iFM, Bergen, Norway, Springer, Forthcoming. (Type: Inproceedings | BibTeX)
Grebing, Sarah Caecilia: User Interaction in Deductive Interactive Program Verification. Karlsruhe Institute of Technology, 2019. (Type: PhD Thesis | BibTeX | Links: )
Grebing, Sarah; Klamroth, Jonas; Ulbrich, Mattias: Seamless Interactive Program Verification. 11th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2019), Springer Publishing, New York City, USA, Forthcoming, (To appear). (Type: Inproceedings | BibTeX)
Beckert, Bernhard; Herda, Mihai; Kobischke, Stefan; Ulbrich, Mattias: Towards a Notion of Coverage for Incomplete Program-Correctness Proofs. Margaria, Tiziana; Steffen, Bernhard (Ed.): 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018), pp. 53–63, Springer, 2018. (Type: Inproceedings | BibTeX | Links: )
Steinhöfel, Dominic; Hähnle, Reiner: Modular, Correct Compilation with Automatic Soundness Proofs. 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. (Type: Inproceedings | Abstract | BibTeX | Links: )
Schiffl, Jonas: Specification and Verification of Hyperledger Fabric Chaincode. Karlsruhe Institute of Technology, 2018. (Type: Masters Thesis | BibTeX)
70 entries « 1 of 7 »
70 entries « 1 of 3 »

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

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

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

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 Forthcoming

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

BibTeX

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

A Program Logic For Dependence Analysis Inproceedings Forthcoming

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

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 Forthcoming

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

BibTeX

2018

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

Towards a Notion of Coverage for Incomplete Program-Correctness Proofs Inproceedings

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

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

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

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, (2017,12), 2017, ISSN: 2190-4782.

BibTeX | Links:

Schmitt, Peter H

A Mechanizable First-Order Theory of Ordinals Inproceedings

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

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

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

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

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:

Beckert, Bernhard; Grebing, Sarah; Ulbrich, Mattias

An Interaction Concept for Program Verification Systems with Explicit Proof Object Inproceedings

Hardware and Software: Verification and Testing - 13th Haifa Verification Conference (HVC 2017), pp. 163–178, Springer International Publishing, Cham, 2017, ISBN: 978-3-319-70389-3.

BibTeX | Links:

2016

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 Book

Springer, 2016, ISBN: 978-3-319-49811-9.

BibTeX | Links:

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

An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier Inproceedings

Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, pp. 403-413, ACM, Singapore, Singapore, 2016, ISBN: 978-1-4503-3845-5.

Abstract | BibTeX

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

The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts Inproceedings

Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, pp. 846–851, ACM, Singapore, Singapore, 2016, ISBN: 978-1-4503-3845-5.

Abstract | BibTeX

Hentschel, Martin

Integrating Symbolic Execution, Debugging and Verification PhD Thesis

Technische Universität Darmstadt, 2016.

Abstract | BibTeX

Thüm, Thomas; Winkelmann, Tim; Schröter, Reimar; Hentschel, Martin; Krüger, Stefan

Variability Hiding in Contracts for Dependent Software Product Lines Inproceedings

Proceedings of the Tenth International Workshop on Variability Modelling of Software-intensive Systems, pp. 97–104, ACM, Salvador, Brazil, 2016, ISBN: 978-1-4503-4019-9.

Abstract | BibTeX

70 entries « 1 of 3 »