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.

56 entries « 1 of 3 »

2018

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, 2018, ISSN: 1433-2787.

Abstract | BibTeX | Links:

2017

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:

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

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

56 entries « 1 of 3 »