--- _id: '517' abstract: - lang: eng text: In the Semantic (Web) Services area, services are considered black boxes with a semantic description of their interfaces as to allow for precise service selection and configuration. The semantic description is usually grounded on domain-specific concepts as modeled in ontologies. This accounts for types used in service signatures, but also predicates occurring in preconditions and effects of services. Ontologies, in particular those enhanced with rules, capture the knowledge of domain experts on properties of and relations between domain concepts. In this paper, we present a verification technique for service compositions which makes use of this domain knowledge. We consider a service composition to be an assembly of services of which we just know signatures, preconditions, and effects. We aim at proving that a composition satisfies a (user-defined) requirement, specified in terms of guaranteed preconditions and required postconditions. As an underlying verification engine we use an SMT solver. To take advantage of the domain knowledge (and often, to enable verification at all), the knowledge is fed into the solver in the form of sorts, uninterpreted functions and in particular assertions as to enhance the solver’s reasoning capabilities. Thereby, we allow for deductions within a domain previously unknown to the solver. We exemplify our technique on a case study from the area of water network optimization software. author: - first_name: Sven full_name: Walther, Sven last_name: Walther - first_name: Heike full_name: Wehrheim, Heike id: '573' last_name: Wehrheim citation: ama: 'Walther S, Wehrheim H. Knowledge-Based Verification of Service Compositions - An SMT approach. In: Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS). ; 2013:24-32. doi:10.1109/ICECCS.2013.14' apa: Walther, S., & Wehrheim, H. (2013). Knowledge-Based Verification of Service Compositions - An SMT approach. In Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS) (pp. 24–32). https://doi.org/10.1109/ICECCS.2013.14 bibtex: '@inproceedings{Walther_Wehrheim_2013, title={Knowledge-Based Verification of Service Compositions - An SMT approach}, DOI={10.1109/ICECCS.2013.14}, booktitle={Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS)}, author={Walther, Sven and Wehrheim, Heike}, year={2013}, pages={24–32} }' chicago: Walther, Sven, and Heike Wehrheim. “Knowledge-Based Verification of Service Compositions - An SMT Approach.” In Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 24–32, 2013. https://doi.org/10.1109/ICECCS.2013.14. ieee: S. Walther and H. Wehrheim, “Knowledge-Based Verification of Service Compositions - An SMT approach,” in Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 2013, pp. 24–32. mla: Walther, Sven, and Heike Wehrheim. “Knowledge-Based Verification of Service Compositions - An SMT Approach.” Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 2013, pp. 24–32, doi:10.1109/ICECCS.2013.14. short: 'S. Walther, H. Wehrheim, in: Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 2013, pp. 24–32.' date_created: 2017-10-17T12:42:33Z date_updated: 2022-01-06T07:01:41Z ddc: - '000' department: - _id: '77' doi: 10.1109/ICECCS.2013.14 file: - access_level: closed content_type: application/pdf creator: ups date_created: 2018-11-02T13:26:08Z date_updated: 2018-11-02T13:26:08Z file_id: '5248' file_name: 06601801.pdf file_size: 217085 relation: main_file file_date_updated: 2018-11-02T13:26:08Z has_accepted_license: '1' language: - iso: eng page: '24 - 32 ' project: - _id: '1' name: SFB 901 - _id: '11' name: SFB 901 - Subprojekt B3 - _id: '3' name: SFB 901 - Project Area B publication: Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS) status: public title: Knowledge-Based Verification of Service Compositions - An SMT approach type: conference user_id: '477' year: '2013' ... --- _id: '3180' author: - first_name: Oleg full_name: Travkin, Oleg last_name: Travkin - first_name: Heike full_name: Wehrheim, Heike id: '573' last_name: Wehrheim - first_name: Gerhard full_name: Schellhorn, Gerhard last_name: Schellhorn citation: ama: Travkin O, Wehrheim H, Schellhorn G. Proving Linearizability of Multiset with Local Proof Obligations. {ECEASST}. 2012. apa: Travkin, O., Wehrheim, H., & Schellhorn, G. (2012). Proving Linearizability of Multiset with Local Proof Obligations. {ECEASST}. bibtex: '@article{Travkin_Wehrheim_Schellhorn_2012, title={Proving Linearizability of Multiset with Local Proof Obligations}, journal={{ECEASST}}, author={Travkin, Oleg and Wehrheim, Heike and Schellhorn, Gerhard}, year={2012} }' chicago: Travkin, Oleg, Heike Wehrheim, and Gerhard Schellhorn. “Proving Linearizability of Multiset with Local Proof Obligations.” {ECEASST}, 2012. ieee: O. Travkin, H. Wehrheim, and G. Schellhorn, “Proving Linearizability of Multiset with Local Proof Obligations,” {ECEASST}, 2012. mla: Travkin, Oleg, et al. “Proving Linearizability of Multiset with Local Proof Obligations.” {ECEASST}, 2012. short: O. Travkin, H. Wehrheim, G. Schellhorn, {ECEASST} (2012). date_created: 2018-06-13T08:16:49Z date_updated: 2022-01-06T06:59:03Z department: - _id: '77' publication: '{ECEASST}' status: public title: Proving Linearizability of Multiset with Local Proof Obligations type: journal_article user_id: '29719' year: '2012' ... --- _id: '3181' author: - first_name: Thomas full_name: Ruhroth, Thomas last_name: Ruhroth - first_name: Heike full_name: Wehrheim, Heike id: '573' last_name: Wehrheim citation: ama: Ruhroth T, Wehrheim H. Model evolution and refinement. Sci Comput Program. 2012;(3):270--289. doi:10.1016/j.scico.2011.04.007 apa: Ruhroth, T., & Wehrheim, H. (2012). Model evolution and refinement. Sci. Comput. Program., (3), 270--289. https://doi.org/10.1016/j.scico.2011.04.007 bibtex: '@article{Ruhroth_Wehrheim_2012, title={Model evolution and refinement}, DOI={10.1016/j.scico.2011.04.007}, number={3}, journal={Sci. Comput. Program.}, author={Ruhroth, Thomas and Wehrheim, Heike}, year={2012}, pages={270--289} }' chicago: 'Ruhroth, Thomas, and Heike Wehrheim. “Model Evolution and Refinement.” Sci. Comput. Program., no. 3 (2012): 270--289. https://doi.org/10.1016/j.scico.2011.04.007.' ieee: T. Ruhroth and H. Wehrheim, “Model evolution and refinement,” Sci. Comput. Program., no. 3, pp. 270--289, 2012. mla: Ruhroth, Thomas, and Heike Wehrheim. “Model Evolution and Refinement.” Sci. Comput. Program., no. 3, 2012, pp. 270--289, doi:10.1016/j.scico.2011.04.007. short: T. Ruhroth, H. Wehrheim, Sci. Comput. Program. (2012) 270--289. date_created: 2018-06-13T08:17:58Z date_updated: 2022-01-06T06:59:03Z department: - _id: '77' doi: 10.1016/j.scico.2011.04.007 issue: '3' page: 270--289 publication: Sci. Comput. Program. status: public title: Model evolution and refinement type: journal_article user_id: '29719' year: '2012' ... --- _id: '3182' author: - first_name: Gerhard full_name: Schellhorn, Gerhard last_name: Schellhorn - first_name: Heike full_name: Wehrheim, Heike id: '573' last_name: Wehrheim - first_name: John full_name: Derrick, John last_name: Derrick citation: ama: 'Schellhorn G, Wehrheim H, Derrick J. How to Prove Algorithms Linearisable. In: Madhusudan P, A. Seshia S, eds. Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. Lecture Notes in Computer Science. ; 2012:243--259. doi:10.1007/978-3-642-31424-7_21' apa: Schellhorn, G., Wehrheim, H., & Derrick, J. (2012). How to Prove Algorithms Linearisable. In P. Madhusudan & S. A. Seshia (Eds.), Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings (pp. 243--259). https://doi.org/10.1007/978-3-642-31424-7_21 bibtex: '@inproceedings{Schellhorn_Wehrheim_Derrick_2012, series={Lecture Notes in Computer Science}, title={How to Prove Algorithms Linearisable}, DOI={10.1007/978-3-642-31424-7_21}, booktitle={Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings}, author={Schellhorn, Gerhard and Wehrheim, Heike and Derrick, John}, editor={Madhusudan, P. and A. Seshia, SanjitEditors}, year={2012}, pages={243--259}, collection={Lecture Notes in Computer Science} }' chicago: Schellhorn, Gerhard, Heike Wehrheim, and John Derrick. “How to Prove Algorithms Linearisable.” In Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, edited by P. Madhusudan and Sanjit A. Seshia, 243--259. Lecture Notes in Computer Science, 2012. https://doi.org/10.1007/978-3-642-31424-7_21. ieee: G. Schellhorn, H. Wehrheim, and J. Derrick, “How to Prove Algorithms Linearisable,” in Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, 2012, pp. 243--259. mla: Schellhorn, Gerhard, et al. “How to Prove Algorithms Linearisable.” Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, edited by P. Madhusudan and Sanjit A. Seshia, 2012, pp. 243--259, doi:10.1007/978-3-642-31424-7_21. short: 'G. Schellhorn, H. Wehrheim, J. Derrick, in: P. Madhusudan, S. A. Seshia (Eds.), Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, 2012, pp. 243--259.' date_created: 2018-06-13T08:19:33Z date_updated: 2022-01-06T06:59:03Z department: - _id: '77' doi: 10.1007/978-3-642-31424-7_21 editor: - first_name: P. full_name: Madhusudan, P. last_name: Madhusudan - first_name: Sanjit full_name: A. Seshia, Sanjit last_name: A. Seshia page: 243--259 publication: Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings series_title: Lecture Notes in Computer Science status: public title: How to Prove Algorithms Linearisable type: conference user_id: '29719' year: '2012' ... --- _id: '590' abstract: - lang: eng text: 'Predicate abstraction is an established technique for reducing the size of the state space during verification. In this paper, we extend predication abstraction with block-abstraction memoization (BAM), which exploits the fact that blocks are often executed several times in a program. The verification can thus benefit from caching the values of previous block analyses and reusing them upon next entry into a block. In addition to function bodies, BAM also performs well for nested loops. To further increase effectiveness, block memoization has been integrated with lazy abstraction adopting a lazy strategy for cache refinement. Together, this achieves significant performance increases: our tool (an implementation within the configurable program analysis framework CPAchecker) has won the Competition on Software Verification 2012 in the category “Overall”.' author: - first_name: Daniel full_name: Wonisch, Daniel last_name: Wonisch - first_name: Heike full_name: Wehrheim, Heike id: '573' last_name: Wehrheim citation: ama: 'Wonisch D, Wehrheim H. Predicate Analysis with Block-Abstraction Memoization. In: Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM). LNCS. ; 2012:332-347. doi:10.1007/978-3-642-34281-3_24' apa: Wonisch, D., & Wehrheim, H. (2012). Predicate Analysis with Block-Abstraction Memoization. In Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM) (pp. 332–347). https://doi.org/10.1007/978-3-642-34281-3_24 bibtex: '@inproceedings{Wonisch_Wehrheim_2012, series={LNCS}, title={Predicate Analysis with Block-Abstraction Memoization}, DOI={10.1007/978-3-642-34281-3_24}, booktitle={Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)}, author={Wonisch, Daniel and Wehrheim, Heike}, year={2012}, pages={332–347}, collection={LNCS} }' chicago: Wonisch, Daniel, and Heike Wehrheim. “Predicate Analysis with Block-Abstraction Memoization.” In Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 332–47. LNCS, 2012. https://doi.org/10.1007/978-3-642-34281-3_24. ieee: D. Wonisch and H. Wehrheim, “Predicate Analysis with Block-Abstraction Memoization,” in Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 2012, pp. 332–347. mla: Wonisch, Daniel, and Heike Wehrheim. “Predicate Analysis with Block-Abstraction Memoization.” Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 2012, pp. 332–47, doi:10.1007/978-3-642-34281-3_24. short: 'D. Wonisch, H. Wehrheim, in: Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 2012, pp. 332–347.' date_created: 2017-10-17T12:42:47Z date_updated: 2022-01-06T07:02:46Z ddc: - '040' department: - _id: '77' doi: 10.1007/978-3-642-34281-3_24 file: - access_level: closed content_type: application/pdf creator: florida date_created: 2018-03-15T08:33:56Z date_updated: 2018-03-15T08:33:56Z file_id: '1258' file_name: 590-WonischWehrheim2012.pdf file_size: 320901 relation: main_file success: 1 file_date_updated: 2018-03-15T08:33:56Z has_accepted_license: '1' language: - iso: eng page: 332-347 project: - _id: '1' name: SFB 901 - _id: '12' name: SFB 901 - Subprojekt B4 - _id: '3' name: SFB 901 - Project Area B publication: Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM) series_title: LNCS status: public title: Predicate Analysis with Block-Abstraction Memoization type: conference user_id: '477' year: '2012' ... --- _id: '608' abstract: - lang: eng text: 'Predicate abstraction is an established technique in software verification. It inherently includes an abstraction refinement loop successively adding predicates until the right level of abstraction is found. For concurrent systems, predicate abstraction can be combined with spotlight abstraction, further reducing the state space by abstracting away certain processes. Refinement then has to decide whether to add a new predicate or a new process. Selecting the right predicates and processes is a crucial task: The positive effect of abstraction may be compromised by unfavourable refinement decisions. Here we present a heuristic approach to abstraction refinement. The basis for a decision is a set of refinement candidates, derived by multiple counterexample-generation. Candidates are evaluated with respect to their influence on other components in the system. Experimental results show that our technique can significantly speed up verification as compared to a naive abstraction refinement.' author: - first_name: Nils full_name: Timm, Nils last_name: Timm - first_name: Heike full_name: Wehrheim, Heike id: '573' last_name: Wehrheim - first_name: Mike full_name: Czech, Mike last_name: Czech citation: ama: 'Timm N, Wehrheim H, Czech M. Heuristic-Guided Abstraction Refinement for Concurrent Systems. In: Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM). LNCS. ; 2012:348-363. doi:10.1007/978-3-642-34281-3_25' apa: Timm, N., Wehrheim, H., & Czech, M. (2012). Heuristic-Guided Abstraction Refinement for Concurrent Systems. In Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM) (pp. 348–363). https://doi.org/10.1007/978-3-642-34281-3_25 bibtex: '@inproceedings{Timm_Wehrheim_Czech_2012, series={LNCS}, title={Heuristic-Guided Abstraction Refinement for Concurrent Systems}, DOI={10.1007/978-3-642-34281-3_25}, booktitle={Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)}, author={Timm, Nils and Wehrheim, Heike and Czech, Mike}, year={2012}, pages={348–363}, collection={LNCS} }' chicago: Timm, Nils, Heike Wehrheim, and Mike Czech. “Heuristic-Guided Abstraction Refinement for Concurrent Systems.” In Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 348–63. LNCS, 2012. https://doi.org/10.1007/978-3-642-34281-3_25. ieee: N. Timm, H. Wehrheim, and M. Czech, “Heuristic-Guided Abstraction Refinement for Concurrent Systems,” in Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 2012, pp. 348–363. mla: Timm, Nils, et al. “Heuristic-Guided Abstraction Refinement for Concurrent Systems.” Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 2012, pp. 348–63, doi:10.1007/978-3-642-34281-3_25. short: 'N. Timm, H. Wehrheim, M. Czech, in: Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 2012, pp. 348–363.' date_created: 2017-10-17T12:42:50Z date_updated: 2022-01-06T07:02:52Z ddc: - '040' department: - _id: '77' doi: 10.1007/978-3-642-34281-3_25 file: - access_level: closed content_type: application/pdf creator: florida date_created: 2018-03-15T08:15:33Z date_updated: 2018-03-15T08:15:33Z file_id: '1250' file_name: 608-Timm2013-0main.pdf file_size: 396337 relation: main_file success: 1 file_date_updated: 2018-03-15T08:15:33Z has_accepted_license: '1' language: - iso: eng page: 348-363 project: - _id: '1' name: SFB 901 - _id: '12' name: SFB 901 - Subprojekt B4 - _id: '3' name: SFB 901 - Project Area B publication: Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM) series_title: LNCS status: public title: Heuristic-Guided Abstraction Refinement for Concurrent Systems type: conference user_id: '477' year: '2012' ... --- _id: '627' abstract: - lang: eng text: Block Abstraction Memoization (ABM) is a technique in software model checking that exploits the modularity of programs during verification by caching. To this end, ABM records the results of block analyses and reuses them if possible when revisiting the same block again. In this paper we present an implementation of ABM into the predicate-analysis component of the software-verification framework CPAchecker. With our participation at the Competition on Software Verification we aim at providing evidence that ABM can not only substantially increase the efficiency of predicate analysis but also enables verification of a wider range of programs. author: - first_name: Daniel full_name: Wonisch, Daniel last_name: Wonisch citation: ama: 'Wonisch D. Block Abstraction Memoization for CPAchecker. In: Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS. ; 2012:531-533. doi:10.1007/978-3-642-28756-5_41' apa: Wonisch, D. (2012). Block Abstraction Memoization for CPAchecker. In Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (pp. 531–533). https://doi.org/10.1007/978-3-642-28756-5_41 bibtex: '@inproceedings{Wonisch_2012, series={LNCS}, title={Block Abstraction Memoization for CPAchecker}, DOI={10.1007/978-3-642-28756-5_41}, booktitle={Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, author={Wonisch, Daniel}, year={2012}, pages={531–533}, collection={LNCS} }' chicago: Wonisch, Daniel. “Block Abstraction Memoization for CPAchecker.” In Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 531–33. LNCS, 2012. https://doi.org/10.1007/978-3-642-28756-5_41. ieee: D. Wonisch, “Block Abstraction Memoization for CPAchecker,” in Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2012, pp. 531–533. mla: Wonisch, Daniel. “Block Abstraction Memoization for CPAchecker.” Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2012, pp. 531–33, doi:10.1007/978-3-642-28756-5_41. short: 'D. Wonisch, in: Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2012, pp. 531–533.' date_created: 2017-10-17T12:42:54Z date_updated: 2022-01-06T07:02:59Z ddc: - '040' department: - _id: '77' doi: 10.1007/978-3-642-28756-5_41 file: - access_level: closed content_type: application/pdf creator: florida date_created: 2018-03-15T06:46:05Z date_updated: 2018-03-15T06:46:05Z file_id: '1242' file_name: 627-WonischSV-Comp2012_01.pdf file_size: 184000 relation: main_file success: 1 file_date_updated: 2018-03-15T06:46:05Z has_accepted_license: '1' language: - iso: eng page: 531-533 project: - _id: '1' name: SFB 901 - _id: '12' name: SFB 901 - Subprojekt B4 - _id: '3' name: SFB 901 - Project Area B publication: Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) series_title: LNCS status: public title: Block Abstraction Memoization for CPAchecker type: conference user_id: '477' year: '2012' ... --- _id: '565' abstract: - lang: eng text: 'In model-driven development of multi-layer systems (e.g. application, platform and infrastructure), each layer is usually described by separate models. When generating analysis models or code, these separate models rst of all need to be linked. Hence, existing model transformations for single layers cannot be simply re-used. In this paper, we present a modular approach to the transformation of multi-layer systems. It employs model weaving to dene the interconnections between models of dierent layers. The weaving models themselves are subject to model transformations: The result of transforming a weaving model constitutes a conguration for the models obtained by transforming single layers, thereby allowing for a re-use of existing model transformations. We exemplify our approach by the generation of analysis models for component-based software.' author: - first_name: Galina full_name: Besova, Galina last_name: Besova - first_name: Sven full_name: Walther, Sven last_name: Walther - first_name: Heike full_name: Wehrheim, Heike id: '573' last_name: Wehrheim - first_name: Steffen full_name: Becker, Steffen last_name: Becker citation: ama: 'Besova G, Walther S, Wehrheim H, Becker S. Weaving-based configuration and modular transformation of multi-layer systems. In: Proceedings of the 15th International Conference on Model Driven Engineering Languages & Systems (MoDELS). LNCS. ; 2012:776-792. doi:10.1007/978-3-642-33666-9_49' apa: Besova, G., Walther, S., Wehrheim, H., & Becker, S. (2012). Weaving-based configuration and modular transformation of multi-layer systems. In Proceedings of the 15th International Conference on Model Driven Engineering Languages & Systems (MoDELS) (pp. 776–792). https://doi.org/10.1007/978-3-642-33666-9_49 bibtex: '@inproceedings{Besova_Walther_Wehrheim_Becker_2012, series={LNCS}, title={Weaving-based configuration and modular transformation of multi-layer systems}, DOI={10.1007/978-3-642-33666-9_49}, booktitle={Proceedings of the 15th International Conference on Model Driven Engineering Languages & Systems (MoDELS)}, author={Besova, Galina and Walther, Sven and Wehrheim, Heike and Becker, Steffen}, year={2012}, pages={776–792}, collection={LNCS} }' chicago: Besova, Galina, Sven Walther, Heike Wehrheim, and Steffen Becker. “Weaving-Based Configuration and Modular Transformation of Multi-Layer Systems.” In Proceedings of the 15th International Conference on Model Driven Engineering Languages & Systems (MoDELS), 776–92. LNCS, 2012. https://doi.org/10.1007/978-3-642-33666-9_49. ieee: G. Besova, S. Walther, H. Wehrheim, and S. Becker, “Weaving-based configuration and modular transformation of multi-layer systems,” in Proceedings of the 15th International Conference on Model Driven Engineering Languages & Systems (MoDELS), 2012, pp. 776–792. mla: Besova, Galina, et al. “Weaving-Based Configuration and Modular Transformation of Multi-Layer Systems.” Proceedings of the 15th International Conference on Model Driven Engineering Languages & Systems (MoDELS), 2012, pp. 776–92, doi:10.1007/978-3-642-33666-9_49. short: 'G. Besova, S. Walther, H. Wehrheim, S. Becker, in: Proceedings of the 15th International Conference on Model Driven Engineering Languages & Systems (MoDELS), 2012, pp. 776–792.' date_created: 2017-10-17T12:42:42Z date_updated: 2022-01-06T07:02:20Z ddc: - '040' department: - _id: '77' doi: 10.1007/978-3-642-33666-9_49 file: - access_level: closed content_type: application/pdf creator: florida date_created: 2018-03-15T10:24:06Z date_updated: 2018-03-15T10:24:06Z file_id: '1276' file_name: 565-Besova_et_al._-_2012_-_Weaving-Based_Configuration_and_Modular_Transformation_of_Multi-layer_Systems_01.pdf file_size: 589972 relation: main_file success: 1 file_date_updated: 2018-03-15T10:24:06Z has_accepted_license: '1' language: - iso: eng page: 776-792 project: - _id: '1' name: SFB 901 - _id: '11' name: SFB 901 - Subprojekt B3 - _id: '3' name: SFB 901 - Project Area B publication: Proceedings of the 15th International Conference on Model Driven Engineering Languages & Systems (MoDELS) series_title: LNCS status: public title: Weaving-based configuration and modular transformation of multi-layer systems type: conference user_id: '477' year: '2012' ... --- _id: '3183' author: - first_name: Steve full_name: Schneider, Steve last_name: Schneider - first_name: Helen full_name: Treharne, Helen last_name: Treharne - first_name: Heike full_name: Wehrheim, Heike id: '573' last_name: Wehrheim citation: ama: 'Schneider S, Treharne H, Wehrheim H. Bounded Retransmission in Event-B{\(\parallel\)}CSP: a Case Study. Electr Notes Theor Comput Sci. 2011:69--80. doi:10.1016/j.entcs.2011.11.019' apa: 'Schneider, S., Treharne, H., & Wehrheim, H. (2011). Bounded Retransmission in Event-B{\(\parallel\)}CSP: a Case Study. Electr. Notes Theor. Comput. Sci., 69--80. https://doi.org/10.1016/j.entcs.2011.11.019' bibtex: '@article{Schneider_Treharne_Wehrheim_2011, title={Bounded Retransmission in Event-B{\(\parallel\)}CSP: a Case Study}, DOI={10.1016/j.entcs.2011.11.019}, journal={Electr. Notes Theor. Comput. Sci.}, author={Schneider, Steve and Treharne, Helen and Wehrheim, Heike}, year={2011}, pages={69--80} }' chicago: 'Schneider, Steve, Helen Treharne, and Heike Wehrheim. “Bounded Retransmission in Event-B{\(\parallel\)}CSP: A Case Study.” Electr. Notes Theor. Comput. Sci., 2011, 69--80. https://doi.org/10.1016/j.entcs.2011.11.019.' ieee: 'S. Schneider, H. Treharne, and H. Wehrheim, “Bounded Retransmission in Event-B{\(\parallel\)}CSP: a Case Study,” Electr. Notes Theor. Comput. Sci., pp. 69--80, 2011.' mla: 'Schneider, Steve, et al. “Bounded Retransmission in Event-B{\(\parallel\)}CSP: A Case Study.” Electr. Notes Theor. Comput. Sci., 2011, pp. 69--80, doi:10.1016/j.entcs.2011.11.019.' short: S. Schneider, H. Treharne, H. Wehrheim, Electr. Notes Theor. Comput. Sci. (2011) 69--80. date_created: 2018-06-13T08:20:47Z date_updated: 2022-01-06T06:59:03Z department: - _id: '77' doi: 10.1016/j.entcs.2011.11.019 page: 69--80 publication: Electr. Notes Theor. Comput. Sci. status: public title: 'Bounded Retransmission in Event-B{\(\parallel\)}CSP: a Case Study' type: journal_article user_id: '29719' year: '2011' ... --- _id: '3184' author: - first_name: John full_name: Derrick, John last_name: Derrick - first_name: Gerhard full_name: Schellhorn, Gerhard last_name: Schellhorn - first_name: Heike full_name: Wehrheim, Heike id: '573' last_name: Wehrheim citation: ama: Derrick J, Schellhorn G, Wehrheim H. Mechanically verified proof obligations for linearizability. {ACM} Trans Program Lang Syst. 2011;(1):4:1--4:43. doi:10.1145/1889997.1890001 apa: Derrick, J., Schellhorn, G., & Wehrheim, H. (2011). Mechanically verified proof obligations for linearizability. {ACM} Trans. Program. Lang. Syst., (1), 4:1--4:43. https://doi.org/10.1145/1889997.1890001 bibtex: '@article{Derrick_Schellhorn_Wehrheim_2011, title={Mechanically verified proof obligations for linearizability}, DOI={10.1145/1889997.1890001}, number={1}, journal={{ACM} Trans. Program. Lang. Syst.}, author={Derrick, John and Schellhorn, Gerhard and Wehrheim, Heike}, year={2011}, pages={4:1--4:43} }' chicago: 'Derrick, John, Gerhard Schellhorn, and Heike Wehrheim. “Mechanically Verified Proof Obligations for Linearizability.” {ACM} Trans. Program. Lang. Syst., no. 1 (2011): 4:1--4:43. https://doi.org/10.1145/1889997.1890001.' ieee: J. Derrick, G. Schellhorn, and H. Wehrheim, “Mechanically verified proof obligations for linearizability,” {ACM} Trans. Program. Lang. Syst., no. 1, pp. 4:1--4:43, 2011. mla: Derrick, John, et al. “Mechanically Verified Proof Obligations for Linearizability.” {ACM} Trans. Program. Lang. Syst., no. 1, 2011, pp. 4:1--4:43, doi:10.1145/1889997.1890001. short: J. Derrick, G. Schellhorn, H. Wehrheim, {ACM} Trans. Program. Lang. Syst. (2011) 4:1--4:43. date_created: 2018-06-13T08:22:02Z date_updated: 2022-01-06T06:59:03Z department: - _id: '77' doi: 10.1145/1889997.1890001 issue: '1' page: 4:1--4:43 publication: '{ACM} Trans. Program. Lang. Syst.' status: public title: Mechanically verified proof obligations for linearizability type: journal_article user_id: '29719' year: '2011' ...