Publications

2015

SCICO

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

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