Application-oriented Formal Verification

Dr. rer. nat. Christoph Gladisch

I am continuing 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

gladisch571625900Xfd4∂mail.informatik.kit.edu

Postal address:

Institute of Theoretical Informatics
Am Fasanengarten 5
76131 Karlsruhe
Germany

More Information

Current research in: AI Safeguarding - Methods and measures for safeguarding AI-based perception functions for automated driving. funded by the Federal Ministry for Economic Affairs and Energy

More information on Young Investigator Groups (YIG)

Committee Member

Center for Embedded Systems, Arizona State University (Member of the Industrial Advisory Board)
11th International Conference on Tests and Proofs, 19 - 20 July 2017, Marburg, Germany (Program Committee)
Formal Verification of Autonomous Vehicles Workshop, Turin, Italy, September 19th, 2017 (Program Committee)
SoSyM 2016, Software and Systems Modeling (Reviewer)
10th International Conference on Tests and Proofs, 5-7 July 2016, Vienna, Austria (Program Committee)
19th ACM International Conference on Hybrid Systems: Computation and Control (Subreviewer)
9th International Conference on Tests and Proofs, L’Aquila, Italy, July 20 - 24, 2015 (Program Committee)
Next Generation Static Software Analysis Tools, Schloss Dagstuhl, Germany, August 24 - August 29, 2014 (Editorial Coordinator)
8th International Conference on Tests & Proofs, York, UK, July 24 - July 25, 2014 (Program Committee)
The 28th IEEE/ACM International Conference on Automated Software Engineering, Palo Alto, California on November 11th - 15th 2013 (Publicity Chair)
7th International Conference on Tests & Proofs Budapest, Hungary, June 18-19, 2013 (Program Committee)
The 27th IEEE/ACM International Conference on Automated Software Engineering (ASE), September 3-7, 2012, Essen, Germany. (Tool Demonstrations Program Committee)
COMPUTING 2011, Symposium on 75 Years of Turing Machine and Lambda-Calculus, Karlsruhe, Germany, October 20-21, 2011. (Program Committee and Organizing Committee)
The Second International Conference on Tests and Proofs April 9-11, 2008 - Prato (near Florence), Italy. (Organizing Committee)
Subreviewer in:GPCE 2016 SWAT 2016 SBMF 2011, TABLEAUX 2011, TAP 2010, FoVeOOS 2010, SoSyM, ECOOP 2009, TAP 2009, JAR, SEFM 2008, ...

Publications

2019

ASE 2019

Experience Paper: Search-based Testing in Automated Driving Control Applications.
Christoph Gladisch, Thomas Heinz, Christian Heinzemann, Jens Oehlerking, Anne von Vietinghoff, Tim Pfitzer.
34th IEEE/ACM International Conference on Automated Software Engineering (ASE 2019), San Diego, USA, November 11 -15, 2019.

Link

SafeComp 2019, WAISE 2019

Open Questions in Testing of Learned Computer Vision Functions for Automated Driving.
Matthias Woehrle, Christoph Gladisch, Christian Heinzemann.
WAISE 2019: Second International Workshop on Artificial Intelligence Safety Engineering. Colocated with International Conference on Computer Safety, Reliability, and Security, Turku, Finland, September 11 -15, 2019.

PDF - Presentation

2017

SoSyM

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

Print ISSN 1619-1366, Online ISSN 1619-1374 PDF PDF (old version)

2016

Book Chapter

Proof-based Test Case Generation
Wolfgang Ahrendt, Christoph Gladisch, Mihai Herda
Deductive Software Verification - The KeY Book: From Theory to Practice

PDF (Springer Link)

2015

SCICO

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

PDF

2014

HVC

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

NFM

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

VSTTE

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

2013

SBMF

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

PPPJ

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

2012

STTT

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

2011

IJSAEM

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

2010

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

2009

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

2008

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

2007

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

Other

Source code based formal techniques for fault-detection, testing, and specification of Java programs