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.

73 entries « 2 of 3 »

2016

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

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

In: 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

In: 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

In: 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

In: 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

In: 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

In: 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

In: 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

In: 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

In: 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

In: 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

In: 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

In: 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

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

Abstract | BibTeX | Links:

Schmitt, Peter H.; Ulbrich, Mattias

Axiomatization of Typed First-Order Logic Inproceedings

In: 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

In: 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

In: 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

In: 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

In: 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

In: 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

In: 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

In: 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:

73 entries « 2 of 3 »