Publications

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

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