Christoph Gladisch

Dr. rer. nat. Christoph Gladisch

I am continuing my research at:
Center for Research and Advance Engineering, Robert BOSCH GmbH.

My past position at KIT

Head of the Young Investigator Group (YIG)
Software Verification Techniques for Fault Detection

Postal address:

Institute of Theoretical Informatics
Am Fasanengarten 5
76131 Karlsruhe

More information

Committee Member




A novel model-based testing approach for software product lines
Ferruccio Damiani, David Faitelson, Christoph Gladisch, Shmuel Tyszberowicz
Software and Systems Modeling, http://dx.doi.org/10.1007/s10270-016-0516-2

PDF (preliminary version)



Specifying Linked Data Structures in JML for Combining Formal Verification and Testing
Christoph Gladisch and Shmuel Tyszberowicz
Science of Computer Programming, http://dx.doi.org/10.1016/j.scico.2015.02.005, Elsevier




Generating JML Specifications from Alloy Expressions
Christoph Gladisch, Daniel Grunwald, Tianhai Liu, Mana Taghdiri and Shmuel Tyszberowicz
10th Haifa Verification Conference (HVC) 2014, Haifa, Israel


JKelloy: A Proof Assistant for Relational Specifications of Java Programs
Aboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel Tyszberowicz, Mana Taghdiri
Nasa Formal Methods (NFM) 2014, Houston, USA
PDF - Abstract - BibTeX


The KeY Platform for Verification and Analysis of Java Programs
Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter Schmitt and Mattias Ulbrich
VSTTE – 6th Working Conference on Verified Software: Theories, Tools and Experiments 2014, Vienna, Austria
PDF - Abstract - BibTeX



Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking
Christoph Gladisch and Shmuel Tyszberowicz
Brazilian Symposium on Formal Methods colocated with the The Brazilian Conference on Software: Theory and Practice (CBSoft)
PDF - Abstract - BibTeX


Refinement-based testing of delta-oriented product lines
Ferruccio Damiani, Christoph Gladisch, Shmuel Tyszberowicz
International Conference on Principles and Practices of Programming on the Java platform
PDF - Abstract - BibTeX - Project



Model Generation for Quantified Formulas with Application to Test Data Generation
Christoph Gladisch
International Journal on Software Tools for Technology Transfer (STTT), 2012, Volume 14, Number 4
Springer - PDF - Abstract - BibTeX - Video1 - Video2



KeYGenU: Combining Verification-Based and Capture and Replay Techniques for Regression Unit Testing
Bernhard Beckert, Christoph Gladisch, Shmuel Tyszberowicz, Amiram Yehudai
IJSAEM 2011: Special Issue on Advances in Software Testing
DOI: 10.1007/s13198-011-0068-3
PDF - BibTeX

Doctoral Dissertation

Verification-based Software-fault Detection
Christoph Gladisch
Online-Publication, Fakultät für Informatik (Fak. f. Informatik) Institut für Theoretische Informatik (ITI), Karlsruher Institut für Technologie (KIT)
KIT Library (PDF) - BibTex


ICTSS 2010

Test Data Generation For Programs with Quantified First-order Logic Specifications
Christoph Gladisch
In Proceedings of the 22nd IFIP International Conference on Testing Software and Systems,
November, 2010, Natal, Brazil
PDF - BibTeX - Abstract

FoVeOOS 2010 (Post-Proceedings)

Satisfiability Solving and Model Generation for Quantified First-order Logic Formulas
Christoph Gladisch
Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers

Best Student Paper and Presentation Award

PDF - BibTeX - Abstract

FoVeOOS 2010

Satisfiability Solving and Model Generation for Quantified First-order Logic Formulas
Christoph Gladisch
Formal Verification of Object-Oriented Software, Papers Presented at the International Conference,
June, 2010, Paris, France (peer reviewed)

Best Student Paper and Presentation Award

PDF - BibTeX - Abstract

TAP 2010

Generating Regression Unit Tests using a Combination of Verification and Capture & Replay
Christoph Gladisch, Shmuel Tyszberowicz, Bernhard Beckert, Amiram Yehudai
In proceedings of The 4th International Conference on Tests And Proofs (TAP 2010), Malaga, Spain
PDF - BibTeX - Abstract


TAP 2009

Could we have chosen a better Loop Invariant or Method Contract?
Christoph Gladisch
In proceedings of The Third International Conference on Tests And Proofs (TAP 2009), Zürich, Switzerland
PDF - BibTeX - Abstract


SEFM 2008

Verification-based Testing for Full Feasible Branch Coverage
Christoph Gladisch
In proceedings of 6th IEEE Int. Conf. Software Engineering and Formal Methods (SEFM'08),
November, 2008, Cape Town, Southafrica
PDF - BibTeX - Abstract

Diploma Thesis

Extending KeY for the Verification of C Programs
Christoph Gladisch
Diploma thesis, Gladisch. Originally written in March 2006.
PDF - BibTeX - Abstract - Amazon

TAP 2008

Integrating Verification and Testing of Object-Oriented Software
Christian Engel, Christoph Gladisch, Vladimir Klebanov, Philipp Rümmer
In proceedings of the Second International Conference on Tests and Proofs, TAP 2008, Prato, Italy
PDF - BibTeX - Abstract

TAP 2008

Verification-based Test Case Generation with Loop Invariants and Method Specifications
Christoph Gladisch
In Tests and Proofs: Papers Presented at the Second International Conference, TAP 2008, Prato, Italy (peer reviewed)
BibTeX - Abstract


C/C++ Verification Workshop (Proceedings)

How C differs from Java for Symbolic Program Execution
Christoph Gladisch
C/C++ Verification Workshop colocated with Integrated Formal Methods 2007, Oxford, United Kingdom
Technical Report of the Radboud University Nijmegen, The Netherlands, (peer reviewed)
PDF - BibTeX - Abstract

TAP 2007

White-box Testing by Combining Deduction-based Specification Extraction and Black-box Testing
Bernhard Beckert, Christoph Gladisch
Proceedings, First International Conference on Tests and Proofs, February, 2010, Zürich, Switzerland
PDF - BibTeX - Abstract