Temporal plans for software architecture reconfiguration - Ziegert, Steffen; Wehrheim, Heike (Computer Science - R & D)

From Program Verification to Time and Space: The Scientific Life of Ernst-Rüdiger Olderog - Meyer, Roland; Wehrheim, Heike (Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings)

Verifying Opacity of a Transactional Mutex Lock - Derrick, John; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike (FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings)

TSO to SC via Symbolic Execution - Wehrheim, Heike; Travkin, Oleg (Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings)

Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings

Verified Service Compositions by Template-Based Construction - Walther, Sven; Wehrheim, Heike (Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS))
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.

Untersuchung transitiver Eigenschaften der Technik "Programs from Proofs" - Korth, Philipp

Towards Systematic Configuration for Architecture Validation - Becker, Matthias; Becker, Steffen; Besova, Galina; Walther, Sven; Wehrheim, Heike (Proceedings of the 40th Euromicro Conference on Software Engineering and Advanced Applications (Work in Progress Session))

Template-based Generation of Semantic Services - Mohr, Felix; Walther, Sven (Proceedings of the 14th International Conference on Software Reuse (ICSR))
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.

Programs from Proofs -- Approach and Applications - Wonisch, Daniel; Schremmer, Alexander; Wehrheim, Heike (Proceedings of the Software Engineering Conference (SE))
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 eﬃciently veriﬁable program. Code consumers thus still do proving themselves, however, on a computationally inexpensive level only. Experimental results show that the proof eﬀort can be reduced by several orders of magnitude, both with respect to time and space.

The behavioural semantics of Event-B refinement - Schneider, Steve; Treharne, Helen; Wehrheim, Heike (Formal Asp. Comput.)

Two approaches for proving linearizability of multiset - Tofan, Bogdan; Travkin, Oleg; Schellhorn, Gerhard; Wehrheim, Heike (Sci. Comput. Program.)

A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures - Schellhorn, Gerhard; Derrick, John; Wehrheim, Heike (ACM Trans. Comput. Log.)

Quiescent Consistency: Defining and Verifying Relaxed Linearizability - Derrick, John; Dongol, Brijesh; Schellhorn, Gerhard; Tofan, Bogdan; Travkin, Oleg; Wehrheim, Heike (FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings)

Handling TSO in Mechanized Linearizability Proofs - Travkin, Oleg; Wehrheim, Heike (Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014. Proceedings)

Timed Automata Verification via IC3 with Zones - Isenberg, Tobias; Wehrheim, Heike (Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings)

Managing LTL Properties in Event-B Refinement - A. Schneider, Steve; Treharne, Helen; Wehrheim, Heike; M. Williams, David (Integrated Formal Methods - 11th International Conference, IFM 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings)

Managing LTL properties in Event-B refinement - Schneider, Steve; Treharne, Helen; Wehrheim, Heike; M. Williams, David (CoRR)

Proof-Carrying Hardware via IC3 - Isenberg, Tobias; Wehrheim, Heike (CoRR)

Certification for Configurable Program Analysis - Jakobs, Marie-Christine; Wehrheim, Heike (Proceedings of the 21st International Symposium on Model Checking of Software (SPIN))
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.