Publications and Tools

@inproceedings{DBLP:conf/birthday/DamianiHKL18,

title = {Same Same But Different: Interoperability of Software Product Line  Variants},

author = {Ferruccio Damiani and Reiner H\"{a}hnle and Eduard Kamburjan and Michael Lienhardt},

editor = {Peter M\"{u}ller and Ina Schaefer},

url = {https://doi.org/10.1007/978-3-319-98047-8_7},

doi = {10.1007/978-3-319-98047-8_7},

year  = {2018},

date = {2018-01-01},

booktitle = {Principled Software Development - Essays Dedicated to Arnd Poetzsch-Heffter 

 on the Occasion of his 60th Birthday},

pages = {99--117},

publisher = {Springer},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{DBLP:conf/ifm/KamburjanC18,

title = {Stateful Behavioral Types for Active Objects},

author = {Eduard Kamburjan and Tzu-Chun Chen},

editor = {Carlo A Furia and Kirsten Winter},

url = {https://doi.org/10.1007/978-3-319-98938-9_13},

doi = {10.1007/978-3-319-98938-9_13},

year  = {2018},

date = {2018-01-01},

booktitle = {Integrated Formal Methods - 14th International Conference, IFM 2018, 

 Maynooth, Ireland, September 5-7, 2018, Proceedings},

volume = {11023},

pages = {214--235},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{DBLP:conf/splc/DamianiHKL18,

title = {Interoperability of software product line variants},

author = {Ferruccio Damiani and Reiner H\"{a}hnle and Eduard Kamburjan and Michael Lienhardt},

editor = {Thorsten Berger and Paulo Borba and Goetz Botterweck and Tomi M\"{a}nnist \"{o} and David Benavides and Sarah Nadi and Timo Kehrer and Rick Rabiser and Christoph Elsner and Mukelabai Mukelabai},

url = {https://doi.org/10.1145/3233027.3236401},

doi = {10.1145/3233027.3236401},

year  = {2018},

date = {2018-01-01},

booktitle = {Proceeedings of the 22nd International Systems and Software Product 

 Line Conference - Volume 1, SPLC 2018, Gothenburg, Sweden, September 

 10-14, 2018},

pages = {264--268},

publisher = {ACM},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{DBLP:journals/corr/abs-1810-02470,

title = {Prototyping Formal System Models with Active Objects},

author = {Eduard Kamburjan and Reiner H\"{a}hnle},

editor = {Massimo Bartoletti and Sophia Knight},

url = {https://doi.org/10.4204/EPTCS.279.7},

doi = {10.4204/EPTCS.279.7},

year  = {2018},

date = {2018-01-01},

booktitle = {Proceedings 11th Interaction and Concurrency Experience, ICE 2018, 

 Madrid, Spain, June 20-21, 2018.},

volume = {279},

pages = {52--67},

series = {EPTCS},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Kamburjan2017,

title = {Deductive Verification of Railway Operations},

author = {Eduard Kamburjan and Reiner H\"{a}hnle},

editor = {Alessandro Fantechi and Thierry Lecomte and Alexander Romanovsky},

url = {https://doi.org/10.1007/978-3-319-68499-4_9},

doi = {10.1007/978-3-319-68499-4_9},

isbn = {978-3-319-68499-4},

year  = {2017},

date = {2017-11-11},

booktitle = {Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification: 2nd International Conference, RSSRail 2017},

pages = {131--147},

publisher = {Springer International Publishing},

address = {Cham},

abstract = {We use deductive verification to show safety properties for the railway operations of Deutsche Bahn. We formalize and verify safety properties for a precise, comprehensive model of operational procedures as specified in the rule books, independently of the shape and size of the actual network layout and the number or schedule of trains. We decompose a global safety property into local properties as well as compositionality and well-formedness assumptions. Then we map local state-based safety properties into history-based properties that can be proven with a high degree of automation using deductive verification. We illustrate our methodology with the proof that for any well-formed infrastructure operating according to the regulations of Deutsche Bahn the following safety property holds: whenever a train leaves a station, the next section is free and no other train on the same line runs in the opposite direction.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Damiani2017,

title = {A Unified and Formal Programming Model for Deltas and Traits},

author = {Ferruccio Damiani and 

 Reiner H\"{a}hnle and 

 Eduard Kamburjan and 

 Michael Lienhardt},

editor = {Marieke Huisman and 

 Julia Rubin},

url = {http://link.springer.com/chapter/10.1007/978-3-662-54494-5_25},

year  = {2017},

date = {2017-01-01},

booktitle = {Fundamental Approaches to Software Engineering - 20th International 

 Conference, FASE 2017, Proceedings},

pages = {424--441},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{Damiani2017b,

title = {Abstraction Refinement for the Analysis of Software Product Lines},

author = {Ferruccio Damiani and Reiner H\"{a}hnle and Michael Lienhardt},

editor = {Sebastian Gabmeyer and Einar Broch Johnsen},

url = {https://doi.org/10.1007/978-3-319-61467-0_1},

doi = {10.1007/978-3-319-61467-0_1},

isbn = {978-3-319-61467-0},

year  = {2017},

date = {2017-01-01},

booktitle = {Tests and Proofs: 11th International Conference, TAP 2017, Held as Part of STAF 2017, Marburg, Germany, July 19--20, 2017, Proceedings},

pages = {3--20},

publisher = {Springer International Publishing},

abstract = {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.},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{kamburjan2016uniform,

title = {Uniform Modeling of Railway Operations},

author = {Eduard Kamburjan and Reiner H\"{a}hnle},

editor = {Cyrille Artho and Peter Csaba \"{O}lveczky},

url = {http://folk.uio.no/peterol/ftscs16-preproceedings.pdf#page=56},

year  = {2016},

date = {2016-11-14},

booktitle = {Fifth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2016), Preproceedings},

pages = {51},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{HaehnleMuschevici16,

title = {Towards Incremental Validation of Railway Systems},

author = {Reiner H\"{a}hnle and Radu Muschevici},

editor = {Tiziana Margaria and Bernhard Steffen},

url = {http://link.springer.com/chapter/10.1007/978-3-319-47169-3_36},

doi = {10.1007/978-3-319-47169-3_36},

isbn = {978-3-319-47169-3},

year  = {2016},

date = {2016-01-01},

booktitle = {Leveraging Applications of Formal Methods, 

 Verification and Validation, 7th International 

 Symposium (ISoLA), Corfu, Greece},

volume = {9953},

publisher = {Springer},

series = {LNCS},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{DBLP:conf/icfem/KamburjanDC16,

title = {Session-Based Compositional Analysis for Actor-Based Languages Using  Futures},

author = {Eduard Kamburjan and Crystal Chang Din and Tzu -Chun Chen},

editor = {Kazuhiro Ogata and 

 Mark Lawford and 

 Shaoying Liu},

url = {http://dx.doi.org/10.1007/978-3-319-47846-3_19},

doi = {10.1007/978-3-319-47846-3_19},

year  = {2016},

date = {2016-01-01},

booktitle = {Formal Methods and Software Engineering - 18th International Conference 

 on Formal Engineering Methods, ICFEM 2016, Tokyo, Japan, November 

 14-18, 2016, Proceedings},

pages = {296--312},

crossref = {DBLP:conf/icfem/2016},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}