@article{3162, author = {{Ziegert, Steffen and Wehrheim, Heike}}, journal = {{Computer Science - R & D}}, number = {{3-4}}, pages = {{303----320}}, title = {{{Temporal plans for software architecture reconfiguration}}}, doi = {{10.1007/s00450-014-0259-7}}, year = {{2015}}, } @inproceedings{3163, author = {{Meyer, Roland and Wehrheim, Heike}}, booktitle = {{Correct System Design - Symposium in Honor of Ernst-R{\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings}}, editor = {{Meyer, Roland and Platzer, Andr{\'{e}} and Wehrheim, Heike}}, pages = {{3----4}}, title = {{{From Program Verification to Time and Space: The Scientific Life of Ernst-R{\"{u}}diger Olderog}}}, doi = {{10.1007/978-3-319-23506-6_1}}, year = {{2015}}, } @inproceedings{3164, author = {{Derrick, John and Dongol, Brijesh and Schellhorn, Gerhard and Travkin, Oleg and Wehrheim, Heike}}, booktitle = {{{FM} 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings}}, editor = {{Bj{\o}rner, Nikolaj and S. de Boer, Frank}}, pages = {{161----177}}, title = {{{Verifying Opacity of a Transactional Mutex Lock}}}, doi = {{10.1007/978-3-319-19249-9_11}}, year = {{2015}}, } @inproceedings{3165, author = {{Wehrheim, Heike and Travkin, Oleg}}, booktitle = {{Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, {HVC} 2015, Haifa, Israel, November 17-19, 2015, Proceedings}}, editor = {{Piterman, Nir}}, pages = {{104----119}}, title = {{{{TSO} to {SC} via Symbolic Execution}}}, doi = {{10.1007/978-3-319-26287-1_7}}, year = {{2015}}, } @proceedings{3166, editor = {{Meyer, Roland and Platzer, Andr{\'{e}} and Wehrheim, Heike}}, isbn = {{978-3-319-23505-9}}, title = {{{Correct System Design - Symposium in Honor of Ernst-R{\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings}}}, doi = {{10.1007/978-3-319-23506-6}}, year = {{2015}}, } @inproceedings{336, abstract = {{Today, service compositions often need to be assembled or changed on-the-fly, which leaves only little time for quality assurance. Moreover, quality assurance is complicated by service providers only giving information on their services in terms of domain specific concepts with only limited semantic meaning. In this paper, we propose a method to construct service compositions based on pre-verifiedtemplates. Templates, given as workflow descriptions, are typed over a (domain-independent) template ontology defining concepts and predicates. Templates are proven correct using an abstract semantics, leaving the specific meaning of ontology concepts open, however, only up to given ontology rules. Construction of service compositions amounts to instantiation of templates with domain-specific services.Correctness of an instantiation can then simply be checked by verifying that the domain ontology(a) adheres to the rules of the template ontology, and (b) fulfills the constraints of the employed template.}}, author = {{Walther, Sven and Wehrheim, Heike}}, booktitle = {{Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS)}}, editor = {{Lanese, Ivan and Madelaine, Eric}}, pages = {{31--48}}, title = {{{Verified Service Compositions by Template-Based Construction}}}, doi = {{10.1007/978-3-319-15317-9_3}}, year = {{2014}}, } @misc{340, author = {{Korth, Philipp}}, publisher = {{Universität Paderborn}}, title = {{{Untersuchung transitiver Eigenschaften der Technik "Programs from Proofs"}}}, year = {{2014}}, } @inproceedings{344, author = {{Becker, Matthias and Becker, Steffen and Besova, Galina and Walther, Sven and Wehrheim, Heike}}, booktitle = {{Proceedings of the 40th Euromicro Conference on Software Engineering and Advanced Applications (Work in Progress Session)}}, title = {{{Towards Systematic Configuration for Architecture Validation}}}, year = {{2014}}, } @inproceedings{353, abstract = {{There are many technologies for the automation of processesthat deal with services; examples are service discovery and composition.Automation of these processes requires that the services are described semantically. However, semantically described services are currently not oronly rarely available, which limits the applicability of discovery and composition approaches. The systematic support for creating new semanticservices usable by automated technologies is an open problem.We tackle this problem with a template based approach: Domain independent templates are instantiated with domain specific services andboolean expressions. The obtained services have semantic descriptionswhose correctness directly follows from the correctness of the template.Besides the theory, we present experimental results for a service repository in which 85% of the services were generated automatically.}}, author = {{Mohr, Felix and Walther, Sven}}, booktitle = {{Proceedings of the 14th International Conference on Software Reuse (ICSR)}}, pages = {{188--203}}, title = {{{Template-based Generation of Semantic Services}}}, doi = {{10.1007/978-3-319-14130-5_14}}, year = {{2014}}, } @inproceedings{383, abstract = {{Proof-carrying code approaches aim at safe execution of untrusted code by having the code producer attach a safety proof to the code which the code consumer only has to validate. Depending on the type of safety property, proofs can however become quite large and their validation - though faster than their construction - still time consuming. In this paper we introduce a new concept for safe execution of untrusted code. It keeps the idea of putting the time consuming part of proving on the side of the code producer, however, attaches no proofs to code anymore but instead uses the proof to transform the program into an equivalent but more efficiently verifiable program. Code consumers thus still do proving themselves, however, on a computationally inexpensive level only. Experimental results show that the proof effort can be reduced by several orders of magnitude, both with respect to time and space.}}, author = {{Wonisch, Daniel and Schremmer, Alexander and Wehrheim, Heike}}, booktitle = {{Proceedings of the Software Engineering Conference (SE)}}, pages = {{67--68}}, title = {{{Programs from Proofs -- Approach and Applications}}}, year = {{2014}}, } @article{3167, author = {{Schneider, Steve and Treharne, Helen and Wehrheim, Heike}}, journal = {{Formal Asp. Comput.}}, number = {{2}}, pages = {{251----280}}, title = {{{The behavioural semantics of Event-B refinement}}}, doi = {{10.1007/s00165-012-0265-0}}, year = {{2014}}, } @article{3168, author = {{Tofan, Bogdan and Travkin, Oleg and Schellhorn, Gerhard and Wehrheim, Heike}}, journal = {{Sci. Comput. Program.}}, pages = {{297----314}}, title = {{{Two approaches for proving linearizability of multiset}}}, doi = {{10.1016/j.scico.2014.04.001}}, year = {{2014}}, } @article{3169, author = {{Schellhorn, Gerhard and Derrick, John and Wehrheim, Heike}}, journal = {{{ACM} Trans. Comput. Log.}}, number = {{4}}, pages = {{31:1----31:37}}, title = {{{A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures}}}, doi = {{10.1145/2629496}}, year = {{2014}}, } @inproceedings{3170, author = {{Derrick, John and Dongol, Brijesh and Schellhorn, Gerhard and Tofan, Bogdan and Travkin, Oleg and Wehrheim, Heike}}, booktitle = {{{FM} 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings}}, editor = {{B. Jones, Cliff and Pihlajasaari, Pekka and Sun, Jun}}, pages = {{200----214}}, title = {{{Quiescent Consistency: Defining and Verifying Relaxed Linearizability}}}, doi = {{10.1007/978-3-319-06410-9_15}}, year = {{2014}}, } @inproceedings{3171, author = {{Travkin, Oleg and Wehrheim, Heike}}, booktitle = {{Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, {HVC} 2014, Haifa, Israel, November 18-20, 2014. Proceedings}}, editor = {{Yahav, Eran}}, pages = {{132----147}}, title = {{{Handling {TSO} in Mechanized Linearizability Proofs}}}, doi = {{10.1007/978-3-319-13338-6_11}}, year = {{2014}}, } @inproceedings{3172, author = {{Isenberg, Tobias and Wehrheim, Heike}}, booktitle = {{Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, {ICFEM} 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings}}, editor = {{Merz, Stephan and Pang, Jun}}, pages = {{203----218}}, title = {{{Timed Automata Verification via {IC3} with Zones}}}, doi = {{10.1007/978-3-319-11737-9_14}}, year = {{2014}}, } @inproceedings{3173, author = {{A. Schneider, Steve and Treharne, Helen and Wehrheim, Heike and M. Williams, David}}, booktitle = {{Integrated Formal Methods - 11th International Conference, {IFM} 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings}}, editor = {{Albert, Elvira and Sekerinski, Emil}}, pages = {{221----237}}, title = {{{Managing {LTL} Properties in Event-B Refinement}}}, doi = {{10.1007/978-3-319-10181-1_14}}, year = {{2014}}, } @article{3174, author = {{Schneider, Steve and Treharne, Helen and Wehrheim, Heike and M. Williams, David}}, journal = {{CoRR}}, title = {{{Managing {LTL} properties in Event-B refinement}}}, year = {{2014}}, } @article{3175, author = {{Isenberg, Tobias and Wehrheim, Heike}}, journal = {{CoRR}}, title = {{{Proof-Carrying Hardware via {IC3}}}}, year = {{2014}}, } @inproceedings{450, abstract = {{Configurable program analysis (CPA) is a generic concept for the formalization of different software analysis techniques in a single framework. With the tool CPAchecker, this framework allows for an easy configuration and subsequent automatic execution of analysis procedures ranging from data-flow analysis to model checking. The focus of the tool CPAchecker is thus on analysis. In this paper, we study configurability from the point of view of software certification. Certification aims at providing (via a prior analysis) a certificate of correctness for a program which is (a) tamper-proof and (b) more efficient to check for validity than a full analysis. Here, we will show how, given an analysis instance of a CPA, to construct a corresponding sound certification instance, thereby arriving at configurable program certification. We report on experiments with certification based on different analysis techniques, and in particular explain which characteristics of an underlying analysis allow us to design an efficient (in the above (b) sense) certification procedure. }}, author = {{Jakobs, Marie-Christine and Wehrheim, Heike}}, booktitle = {{Proceedings of the 21st International Symposium on Model Checking of Software (SPIN)}}, pages = {{30--39}}, title = {{{Certification for Configurable Program Analysis}}}, doi = {{10.1145/2632362.2632372}}, year = {{2014}}, }