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 « 2 of 4 »

2018

Beckert, Bernhard; Bischof, Simon; Herda, Mihai; Kirsten, Michael; Büning, Marko Kleine

Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow Control Proceedings Article

In: Sun, Jing; Sun, Meng (Ed.): 20th International Conference on Formal Engineering Methods - Formal Methods and Software Engineering (ICFEM 2018), pp. 284–300, Springer, Gold Coast, QLD, Australia, 2018.

BibTeX | Links:

Greiner, Simon

A Framework for Non-Interference in Component-Based Systems PhD Thesis

Karlsruhe Institute of Technology, 2018.

BibTeX | Links:

Grebing, Sarah; Luong, An Thuy Tien; Weigl, Alexander

Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification -- Lessons Learned Proceedings Article

In: Jamnik, Mateja; Lüth, Christoph (Ed.): 13th International Workshop on User Interfaces for Theorem Provers (UITP 2018), 2018, (To appear, %snip pdf=https://formal.iti.kit.edu/~grebing/pub/uitp2018.pdf).

BibTeX

2017

E., Max; Hecker, Martin; Greiner, Simon; Bao, Kaibin; Yurchenko, Kateryna

Model-Driven Specification and Analysis of Confidentiality in Component-Based Systems Technical Report

Department of Informatics, Karlsruhe Institute of Technology Karlsruhe, no. 2017,12, 2017, ISSN: 2190-4782.

BibTeX | Links:

Schmitt, Peter H.

A Mechanizable First-Order Theory of Ordinals Proceedings Article

In: Schmidt, Renate A.; Nalon, Claudia (Ed.): Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, {TABLEAUX} 2017, Brasilia, Brazil, September 25-28, 2017, Proceedings, pp. 331–346, Springer, 2017, ISBN: 978-3-319-66901-4.

Abstract | BibTeX | Links:

Beckert, Bernhard; Schiffl, Jonas; Schmitt, Peter H.; Ulbrich, Mattias

Proving JDK's Dual Pivot Quicksort Correct Proceedings Article

In: 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017), 2017, (To appear ).

BibTeX | Links:

de Gouw, Stijn; de Boer, Frank S; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic

Verifying OpenJDK's Sort Method for Generic Collections Journal Article

In: Journal of Automated Reasoning, 2017, ISSN: 1573-0670.

Abstract | BibTeX | Links:

Do, Quoc Huy; Bubel, Richard; Hähnle, Reiner

Inferring Secrets by Guided Experiments Proceedings Article

In: Hung, Dang Van; Kapur, Deepak (Ed.): Theoretical Aspects of Computing -- ICTAC 2017: 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings, pp. 269–287, Springer International Publishing, Cham, 2017.

BibTeX | Links:

Steinhöfel, Dominic; Wasser, Nathan

A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows Proceedings Article

In: Polikarpova, Nadia; Schneider, Steve (Ed.): Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings, pp. 279–294, Springer, 2017.

BibTeX | Links:

Beckert, Bernhard; Grebing, Sarah; Ulbrich, Mattias

An Interaction Concept for Program Verification Systems with Explicit Proof Object Proceedings Article

In: Hardware and Software: Verification and Testing - 13th Haifa Verification Conference (HVC 2017), pp. 163–178, Springer International Publishing, Cham, 2017, ISBN: 978-3-319-70389-3.

BibTeX | Links:

2016

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

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

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

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

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

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

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, vol. 1, pp. 238–267, 2016.

BibTeX | Links:

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

Can Formal Methods Improve the Efficiency of Code Reviews? Proceedings Article

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

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, vol. 17, no. 6, pp. 729–744, 2015, ISSN: 1433-2779.

Abstract | BibTeX | Links:

Mostowski, Wojciech; Ulbrich, Mattias

Dynamic Dispatch for Method Contracts through Abstract Predicates Proceedings Article

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

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:

85 entries « 2 of 4 »