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.

57 entries « 2 of 3 »

2015

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:

Beckert, Bernhard; Bruns, Daniel

Dynamic Logic with Trace Semantics Inproceedings

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 Inproceedings

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 Inproceedings

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 Inproceedings

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 (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

Informatik-Spektrum, 35 (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 (2012,8), 2012.

Abstract | BibTeX | Links:

Gladisch, Christoph

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

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 Inproceedings

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

2011

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

On Proving Alloy Specifications using KeY Technical Report

Karlsruhe Institute of Technology (2011-37), 2011.

BibTeX

Beckert, Bernhard; Gladisch, Christoph; Tyszberowicz, Shmuel; Yehudai, Amiram

KeYGenU: Combining Verification-Based and Capture and Replay Techniques for Regression Unit Testing Journal Article

International Journal of System Assurance Engineering and Management, 2 (2), pp. 97–113, 2011, ISSN: 0976-4348.

Abstract | BibTeX | Links:

Schmitt, Peter H; Ulbrich, Mattias; Weiß, Benjamin

Dynamic Frames in Java Dynamic Logic Inproceedings

Beckert, Bernhard; Marché, Claude (Ed.): Revised Selected Papers, International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), pp. 138–152, Springer, 2011.

BibTeX

57 entries « 2 of 3 »