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

47 entries « 1 of 2 »

2016

Ahrendt, Wolfgang; Beckert, Bernhard; Bubel, Richard; ä, Reiner H; 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:

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:

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:

47 entries « 1 of 2 »