header by solar.empire

11th International Conference on Tests & Proofs

19-20 July 2017, Marburg, Germany


Abstraction Refinement for the Analysis of Software Product Lines

Reiner Hähnle, TU Darmstadt

Thursday 20 July 2017, 1st session


We generalize the principle of counter example-guided data abstraction refinement (CEGAR) to guided refinement of Software Product Lines (SPL) and of analysis tools. We also add a problem decomposition step. The result is a framework for formal SPL analysis via guided refinement and divide-and-conquer, through sound orchestration of multiple tools.


Reiner Hähnle received a Diploma and a Ph.D. in Computer Science from University of Karlsruhe and a Habilitation from Technical University of Vienna. From 2000 he was Associate Professor and from 2002 Full Professor of Computer Science at Chalmers University. Since 2011 he holds the Chair of Software Engineering at Technical University Darmstadt. He worked as a guest researcher at ICOT Tokyo, University of Tübingen, University of Turin, and University of Oslo. He authored and edited 180 international, peer-reviewed publications and served on 100 programme committees. Reiner was one of the founders of the Tableaux conference, a founding trustee of FLoC Inc., PC Chair of IJCAR, Tableaux, and TAP, as well as Wine Chair of ECOOP. His research interests include formal analysis and verification of OO languages, executable software models, tool-assisted debugging, test generation. Reiner is founder of the KeY verification system for Java and a co-designer of the executable modeling language ABS.