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.

70 entries « 3 of 7 »
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. (Type: Book | BibTeX | Links: )
Hentschel, Martin; Hähnle, Reiner; Bubel, Richard: An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier. 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. (Type: Inproceedings | Abstract | BibTeX)
Hentschel, Martin; Hähnle, Reiner; Bubel, Richard: The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts. 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. (Type: Inproceedings | Abstract | BibTeX)
Hentschel, Martin: Integrating Symbolic Execution, Debugging and Verification. Technische Universität Darmstadt, 2016. (Type: PhD Thesis | Abstract | BibTeX)
Thüm, Thomas; Winkelmann, Tim; Schröter, Reimar; Hentschel, Martin; Krüger, Stefan: Variability Hiding in Contracts for Dependent Software Product Lines. 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. (Type: Inproceedings | Abstract | BibTeX)
Dörre, Felix; Klebanov, Vladimir: Pseudo-Random Number Generator Verification: A Case Study. 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. (Type: Inproceedings | BibTeX | Links: )
Scheurer, Dominic; Hähnle, Reiner; Bubel, Richard: A General Lattice Model for Merging Symbolic Execution Branches. 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. (Type: Inproceedings | Abstract | BibTeX | Links: )
Do, Quoc Huy; Kamburjan, Eduard; Wasser, Nathan: Towards Fully Automatic Logic-Based Information Flow Analysis: An Electronic-Voting Case Study. 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. (Type: Inproceedings | BibTeX | Links: )
Mostowski, Wojciech; Ulbrich, Mattias: Dynamic Dispatch for Method Contracts Through Abstract Predicates. Trans. Modularity and Composition, 1 , pp. 238–267, 2016. (Type: Journal Article | BibTeX | Links: )
Hentschel, Martin; Hähnle, Reiner; Bubel, Richard: Can Formal Methods Improve the Efficiency of Code Reviews?. Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings, pp. 3–19, 2016. (Type: Inproceedings | BibTeX | Links: )
70 entries « 3 of 7 »
70 entries « 3 of 3 »

2013

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

2010

Gladisch, Christoph

Test Data Generation for Programs with Quantified First-Order Logic Specifications Inproceedings

ICTSS, pp. 158-173, 2010.

BibTeX

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

Generating Regression Unit Tests Using a Combination of Verification and Capture & Replay Book Chapter

Fraser, Gordon ; Gargantini, Angelo (Ed.): Tests and Proofs: 4th International Conference, TAP 2010, M'alaga, Spain, July 1-2, 2010. Proceedings, pp. 61–76, Springer Berlin Heidelberg, Berlin, Heidelberg, 2010, ISBN: 978-3-642-13977-2.

BibTeX | Links:

2008

Gladisch, Christoph

Verification-based Testing for Full Feasible Branch Coverage Inproceedings

Cerone, Antonio (Ed.): Proc. 6th IEEE Int. Conf. Software Engineering and Formal Methods (SEFM'08), IEEE Computer Society Press, 2008, ISBN: 978-0-7695-3437-4.

BibTeX

2007

Beckert, Bernhard; Gladisch, Christoph

White-box Testing by Combining Deduction-based Specification Extraction and Black-box Testing Inproceedings

Proceedings of the 1st International Conference on Tests and Proofs, pp. 207–216, Springer-Verlag, Zurich, Switzerland, 2007, ISBN: 3-540-73769-3, 978-3-540-73769-8.

BibTeX | Links:

Engel, Christian; Hähnle, Reiner

Generating Unit Tests from Formal Proofs Inproceedings

Gurevich, Yuri; Meyer, Bertrand (Ed.): Proceedings, 1st International Conference on Tests And Proofs (TAP), Zurich, Switzerland, Springer, 2007.

BibTeX

2005

Darvas, Ádám; Hähnle, Reiner; Sands, Dave

A Theorem Proving Approach to Analysis of Secure Information Flow Inproceedings

Hutter, Dieter; Ullmann, Markus (Ed.): Proc. 2nd International Conference on Security in Pervasive Computing, pp. 193–209, Springer-Verlag, 2005.

BibTeX | Links:

2003

Darvas, Ádám; Hähnle, Reiner; Sands, Dave

A Theorem Proving Approach to Analysis of Secure Information Flow Inproceedings

Gorrieri, Roberto (Ed.): Workshop on Issues in the Theory of Security, WITS, IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS 2003.

BibTeX

70 entries « 3 of 3 »