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 « 2 of 7 »
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. 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. (Type: Inproceedings | BibTeX | Links: )
Greiner, Simon: A Framework for Non-Interference in Component-Based Systems. Karlsruhe Institute of Technology, 2018. (Type: PhD Thesis | BibTeX | Links: )
Grebing, Sarah; Luong, An Thuy Tien; Weigl, Alexander: Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned. 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). (Type: Inproceedings | BibTeX)
E., Max; Hecker, Martin; Greiner, Simon; Bao, Kaibin; Yurchenko, Kateryna: Model-Driven Specification and Analysis of Confidentiality in Component-Based Systems. Department of Informatics, Karlsruhe Institute of Technology Karlsruhe, (2017,12), 2017, ISSN: 2190-4782. (Type: Technical Report | BibTeX | Links: )
Schmitt, Peter H: A Mechanizable First-Order Theory of Ordinals. 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. (Type: Inproceedings | Abstract | BibTeX | Links: )
Beckert, Bernhard; Schiffl, Jonas; Schmitt, Peter H; Ulbrich, Mattias: Proving JDK's Dual Pivot Quicksort Correct. 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017), 2017, (To appear ). (Type: Inproceedings | 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 of Automated Reasoning, 2017, ISSN: 1573-0670. (Type: Journal Article | Abstract | BibTeX | Links: )
Do, Quoc Huy; Bubel, Richard; Hähnle, Reiner: Inferring Secrets by Guided Experiments. 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. (Type: Inproceedings | BibTeX | Links: )
Steinhöfel, Dominic; Wasser, Nathan: A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows. 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. (Type: Inproceedings | BibTeX | Links: )
Beckert, Bernhard; Grebing, Sarah; Ulbrich, Mattias: An Interaction Concept for Program Verification Systems with Explicit Proof Object. 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. (Type: Inproceedings | BibTeX | Links: )
70 entries « 2 of 7 »
70 entries « 2 of 3 »

2016

Dörre, Felix; Klebanov, Vladimir

Pseudo-Random Number Generator Verification: A Case Study Inproceedings

Revised Selected Papers of the 7th International Conference on Verified Software: Theories, Tools, and Experiments, pp. 61–72, Springer-Verlag New York, Inc., San Francisco, CA, USA, 2016, ISBN: 978-3-319-29612-8.

BibTeX | Links:

Scheurer, Dominic; Hähnle, Reiner; Bubel, Richard

A General Lattice Model for Merging Symbolic Execution Branches Inproceedings

Ogata, Kazuhiro; Lawford, Mark; Liu, Shaoying (Ed.): Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 14-18, 2016, Proceedings, pp. 57–73, Springer International Publishing, 2016.

Abstract | BibTeX | Links:

Do, Quoc Huy; Kamburjan, Eduard; Wasser, Nathan

Towards Fully Automatic Logic-Based Information Flow Analysis: An Electronic-Voting Case Study Inproceedings

Proceedings of the 5th International Conference on Principles of Security and Trust - Volume 9635, pp. 97–115, Springer-Verlag New York, Inc., New York, NY, USA, 2016, ISBN: 978-3-662-49634-3.

BibTeX | Links:

Mostowski, Wojciech; Ulbrich, Mattias

Dynamic Dispatch for Method Contracts Through Abstract Predicates Journal Article

Trans. Modularity and Composition, 1 , pp. 238–267, 2016.

BibTeX | Links:

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

Can Formal Methods Improve the Efficiency of Code Reviews? Inproceedings

Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings, pp. 3–19, 2016.

BibTeX | Links:

Wasser, Nathan

Automatic generation of specifications using verification tools = Automatische Spezifikationserzeugung mit Hilfe von Verifikationswerkzeugen PhD Thesis

Darmstadt University of Technology, Germany, 2016.

BibTeX | Links:

2015

Beckert, Bernhard; Klebanov, Vladimir; Ulbrich, Mattias

Regression Verification for Java Using a Secure Information Flow Calculus Inproceedings

Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, pp. 6:1–6:6, ACM, Prague, Czech Republic, 2015, ISBN: 978-1-4503-3656-7.

BibTeX

Bruns, Daniel; Mostowski, Wojciech; Ulbrich, Mattias

Implementation-level Verification of Algorithms with KeY Journal Article

Software Tools for Technology Transfer, 17 (6), pp. 729–744, 2015, ISSN: 1433-2779.

Abstract | BibTeX | Links:

Mostowski, Wojciech; Ulbrich, Mattias

Dynamic Dispatch for Method Contracts through Abstract Predicates Inproceedings

Proceedings of the 14th International Conference on Modularity, MODULARITY 2015, Fort Collins, CO, USA, March 16 - 19, 2015, pp. 109–116, ACM, 2015.

BibTeX | Links:

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

Exploit Generation for Information Flow Leaks in Object-Oriented Programs Inproceedings

ICT Systems Security and Privacy Protection - 30th IFIP TC 11 International Conference, SEC 2015, Hamburg, Germany, May 26-28, 2015, Proceedings, pp. 401–415, 2015.

BibTeX | Links:

Küsters, Ralf; Truderung, Tomasz; Beckert, Bernhard; Bruns, Daniel; Kirsten, Michael; Mohr, Martin

A Hybrid Approach for Proving Noninterference of Java Programs Inproceedings

Fournet, Cédric; Hicks, Michael (Ed.): 28th IEEE Computer Security Foundations Symposium (CSF 2015), pp. 305-319, 2015.

Abstract | BibTeX | Links:

Küsters, Ralf; Truderung, Tomasz; Beckert, Bernhard; Bruns, Daniel; Kirsten, Michael; Mohr, Martin

A Hybrid Approach for Proving Noninterference of Java Programs Journal Article

IACR Cryptology ePrint Archive, 2015 , pp. 438, 2015.

Abstract | BibTeX | Links:

Schmitt, Peter H; Ulbrich, Mattias

Axiomatization of Typed First-Order Logic Inproceedings

20th International Symposium on Formal Methods (FM 2015), pp. 470–486, 2015.

BibTeX | Links:

Wasser, Nathan

Generating Specifications for Recursive Methods by Abstracting Program States Inproceedings

SETTA, pp. 243–257, Springer, 2015.

BibTeX

2014

Hentschel, Martin; Käsdorf, Stefan; Hähnle, Reiner; Bubel, Richard

An interactive verification tool meets an IDE Inproceedings

Albert, Elvira; Sekerinski, Emil; Zavattaro, Gianluigi (Ed.): Proceedings of the 11th International Conference on Integrated Formal Methods, pp. 55–70, Springer, 2014.

Abstract | BibTeX

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

Symbolic Execution Debugger (SED) Inproceedings

Bonakdarpour, Borzoo; Smolka, Scott A (Ed.): Proceedings of Runtime Verification 2014, pp. 255–262, Springer, 2014.

Abstract | BibTeX

Thüm, Thomas; Meinicke, Jens; Benduhn, Fabian; Hentschel, Martin; von Rhein, Alexander; Saake, Gunter

Potential Synergies of Theorem Proving and Model Checking for Software Product Lines Inproceedings

Proceedings of the International Software Product Line Conference (SPLC), ACM, New York, NY, USA, 2014.

Abstract | BibTeX

Ahrendt, Wolfgang; Beckert, Bernhard; Bruns, Daniel; Bubel, Richard; Gladisch, Christoph; Grebing, Sarah; Hähnle, Reiner; Hentschel, Martin; Herda, Mihai; Klebanov, Vladimir; Mostowski, Wojciech; Scheben, Christoph; Schmitt, Peter H; Ulbrich, Mattias

The KeY Platform for Verification and Analysis of Java Programs Inproceedings

Giannakopoulou, Dimitra; Kroening, Daniel (Ed.): Verified Software: Theories, Tools, and Experiments (VSTTE 2014), pp. 1–17, Springer-Verlag, 2014, ISBN: 978-3-642-54107-0.

Abstract | BibTeX | Links:

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

Visualizing Unbounded Symbolic Execution Inproceedings

Seidl, Martina; Tillmann, Nikolai (Ed.): Proceedings of Testing and Proofs (TAP) 2014, pp. 82–98, Springer, 2014.

BibTeX

Ghazi, Aboubakr Achraf El; Ulbrich, Mattias; Gladisch, Christoph; Tyszberowicz, Shmuel; Taghdiri, Mana

JKelloy: A Proof Assistant for Relational Specifications of Java Programs Inproceedings

NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings, pp. 173–187, 2014.

BibTeX | Links:

Bruns, Daniel

Formal Verification of an Electronic Voting System Technical Report

Department of Informatics, Karlsruhe Institute of Technology (2014,11), 2014, ISSN: 2190-4782.

Abstract | BibTeX | Links:

Bruns, Daniel

Towards Specification and Verification of Information Flow in Concurrent Java-like Programs Technical Report

Department of Informatics, Karlsruhe Institute of Technology (2014,5), 2014, ISSN: 2190-4782.

Abstract | BibTeX | Links:

2013

Küsters, Ralf; Truderung, Tomasz; Beckert, Bernhard; Bruns, Daniel; Graf, Jürgen; Scheben, Christoph

A Hybrid Approach for Proving Noninterference and Applications to the Cryptographic Verification of Java Programs Inproceedings

Hammer, Christian; Mauw, Sjouke (Ed.): Grande Region Security and Reliability Day 2013, Luxembourg, 2013, (Extended Abstract).

BibTeX | Links:

Beckert, Bernhard; Bruns, Daniel; Klebanov, Vladimir; Scheben, Christoph; Schmitt, Peter H; Ulbrich, Mattias

Information Flow in Object-Oriented Software - Extended Version Technical Report

Department of Informatics, Karlsruhe Institute of Technology (2013,14), 2013, ISSN: 2190-4782.

BibTeX | Links:

Beckert, Bernhard; Bruns, Daniel; Klebanov, Vladimir; Scheben, Christoph; Schmitt, Peter H; Ulbrich, Mattias

Secure Information Flow for Java - A Dynamic Logic Approach Technical Report

Department of Informatics, Karlsruhe Institute of Technology (2013,10), 2013, ISSN: 2190-4782.

BibTeX | Links:

70 entries « 2 of 3 »