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.

85 entries « 3 of 4 »

2015

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

A Hybrid Approach for Proving Noninterference of Java Programs Proceedings Article

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, vol. 2015, pp. 438, 2015.

Abstract | BibTeX | Links:

Schmitt, Peter H.; Ulbrich, Mattias

Axiomatization of Typed First-Order Logic Proceedings Article

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 Proceedings Article

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 Proceedings Article

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) Proceedings Article

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 Proceedings Article

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 Proceedings Article

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 Proceedings Article

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 Proceedings Article

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 no. 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 no. 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 Proceedings Article

In: 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 no. 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 no. 2013,10, 2013, ISSN: 2190-4782.

BibTeX | Links:

Beckert, Bernhard; Bruns, Daniel

Dynamic Logic with Trace Semantics Proceedings Article

In: Bonacina, Maria Paola (Ed.): 24th International Conference on Automated Deduction (CADE-24), pp. 315–329, Springer-Verlag, 2013, ISBN: 978-3-642-38573-5.

Abstract | BibTeX | Links:

Gladisch, Christoph; Tyszberowicz, Shmuel

Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking Proceedings Article

In: de Moura, Leonardo; Iyoda, Juliano (Ed.): Brazilian Symposium on Formal Methods (SBMF), Springer, 2013.

BibTeX

Kirsten, Michael

Proving Well-Definedness of JML Specifications with KeY Masters Thesis

ITI Schmitt, Karlsruhe Institute of Technology, 2013.

Abstract | BibTeX

2012

Ulbrich, Mattias; Geilmann, Ulrich; Ghazi, Aboubakr Achraf El; Taghdiri, Mana

A Proof Assistant for Alloy Specifications Proceedings Article

In: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 422-436, 2012.

BibTeX

Beckert, Bernhard; Bruns, Daniel

Formal Semantics of Model Fields in Annotation-based Specifications Proceedings Article

In: Glimm, Birte; Krüger, Antonio (Ed.): KI 2012: Advances in Artificial Intelligence, pp. 13–24, Springer-Verlag, 2012, ISBN: 978-3-642-33346-0.

Abstract | BibTeX | Links:

Beckert, Bernhard; Bruns, Daniel

Dynamic Trace Logic: Definition and Proofs Technical Report

Department of Informatics, Karlsruhe Institute of Technology no. 2012,10, 2012, ISSN: 2190-4782, (A revised version replacing an unsound rule is available at http://formal.iti.kit.edu/~bruns/papers/trace-tr.pdf).

Abstract | BibTeX | Links:

Bruns, Daniel

Eine formale Semantik für die Java Modeling Language Journal Article

In: Informatik-Spektrum, vol. 35, no. 1, pp. 45–49, 2012.

BibTeX | Links:

Beckert, Bernhard; Bruns, Daniel; Küsters, Ralf; Scheben, Christoph; Schmitt, Peter H.; Truderung, Tomasz

The KeY Approach for the Cryptographic Verification of Java Programs: A Case Study Technical Report

Department of Informatics, Karlsruhe Institute of Technology no. 2012,8, 2012.

Abstract | BibTeX | Links:

Gladisch, Christoph

Model generation for quantified formulas with application to test data generation Journal Article

In: International Journal on Software Tools for Technology Transfer (STTT), pp. 1-21, 2012, ISSN: 1433-2779, (10.1007/s10009-012-0227-0).

BibTeX | Links:

Thüm, Thomas; Schaefer, Ina; Apel, Sven; Hentschel, Martin

Family-Based Deductive Verification of Software Product Lines Proceedings Article

In: Proceedings of the 11th International Conference on Generative Programming and Component Engineering, pp. 11-20, ACM, Dresden, Germany, 2012, ISBN: 978-1-4503-1129-8.

Abstract | BibTeX

85 entries « 3 of 4 »