[{"date_updated":"2022-01-06T07:01:41Z","author":[{"last_name":"Walther","full_name":"Walther, Sven","first_name":"Sven"},{"first_name":"Heike","id":"573","full_name":"Wehrheim, Heike","last_name":"Wehrheim"}],"date_created":"2017-10-17T12:42:33Z","title":"Knowledge-Based Verification of Service Compositions - An SMT approach","doi":"10.1109/ICECCS.2013.14","has_accepted_license":"1","year":"2013","page":"24 - 32 ","citation":{"ama":"Walther S, Wehrheim H. Knowledge-Based Verification of Service Compositions - An SMT approach. In: <i>Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS)</i>. ; 2013:24-32. doi:<a href=\"https://doi.org/10.1109/ICECCS.2013.14\">10.1109/ICECCS.2013.14</a>","chicago":"Walther, Sven, and Heike Wehrheim. “Knowledge-Based Verification of Service Compositions - An SMT Approach.” In <i>Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS)</i>, 24–32, 2013. <a href=\"https://doi.org/10.1109/ICECCS.2013.14\">https://doi.org/10.1109/ICECCS.2013.14</a>.","ieee":"S. Walther and H. Wehrheim, “Knowledge-Based Verification of Service Compositions - An SMT approach,” in <i>Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS)</i>, 2013, pp. 24–32.","short":"S. Walther, H. Wehrheim, in: Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 2013, pp. 24–32.","bibtex":"@inproceedings{Walther_Wehrheim_2013, title={Knowledge-Based Verification of Service Compositions - An SMT approach}, DOI={<a href=\"https://doi.org/10.1109/ICECCS.2013.14\">10.1109/ICECCS.2013.14</a>}, 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} }","mla":"Walther, Sven, and Heike Wehrheim. “Knowledge-Based Verification of Service Compositions - An SMT Approach.” <i>Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS)</i>, 2013, pp. 24–32, doi:<a href=\"https://doi.org/10.1109/ICECCS.2013.14\">10.1109/ICECCS.2013.14</a>.","apa":"Walther, S., &#38; Wehrheim, H. (2013). Knowledge-Based Verification of Service Compositions - An SMT approach. In <i>Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS)</i> (pp. 24–32). <a href=\"https://doi.org/10.1109/ICECCS.2013.14\">https://doi.org/10.1109/ICECCS.2013.14</a>"},"_id":"517","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Subprojekt B3","_id":"11"},{"_id":"3","name":"SFB 901 - Project Area B"}],"department":[{"_id":"77"}],"user_id":"477","ddc":["000"],"file_date_updated":"2018-11-02T13:26:08Z","language":[{"iso":"eng"}],"publication":"Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS)","type":"conference","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."}],"status":"public","file":[{"relation":"main_file","content_type":"application/pdf","access_level":"closed","file_name":"06601801.pdf","file_id":"5248","file_size":217085,"date_created":"2018-11-02T13:26:08Z","creator":"ups","date_updated":"2018-11-02T13:26:08Z"}]},{"title":"Proving Linearizability of Multiset with Local Proof Obligations","date_created":"2018-06-13T08:16:49Z","author":[{"first_name":"Oleg","last_name":"Travkin","full_name":"Travkin, Oleg"},{"first_name":"Heike","last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike"},{"full_name":"Schellhorn, Gerhard","last_name":"Schellhorn","first_name":"Gerhard"}],"date_updated":"2022-01-06T06:59:03Z","citation":{"apa":"Travkin, O., Wehrheim, H., &#38; Schellhorn, G. (2012). Proving Linearizability of Multiset with Local Proof Obligations. <i>{ECEASST}</i>.","mla":"Travkin, Oleg, et al. “Proving Linearizability of Multiset with Local Proof Obligations.” <i>{ECEASST}</i>, 2012.","short":"O. Travkin, H. Wehrheim, G. Schellhorn, {ECEASST} (2012).","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} }","ieee":"O. Travkin, H. Wehrheim, and G. Schellhorn, “Proving Linearizability of Multiset with Local Proof Obligations,” <i>{ECEASST}</i>, 2012.","chicago":"Travkin, Oleg, Heike Wehrheim, and Gerhard Schellhorn. “Proving Linearizability of Multiset with Local Proof Obligations.” <i>{ECEASST}</i>, 2012.","ama":"Travkin O, Wehrheim H, Schellhorn G. Proving Linearizability of Multiset with Local Proof Obligations. <i>{ECEASST}</i>. 2012."},"year":"2012","department":[{"_id":"77"}],"user_id":"29719","_id":"3180","status":"public","publication":"{ECEASST}","type":"journal_article"},{"issue":"3","year":"2012","citation":{"chicago":"Ruhroth, Thomas, and Heike Wehrheim. “Model Evolution and Refinement.” <i>Sci. Comput. Program.</i>, no. 3 (2012): 270--289. <a href=\"https://doi.org/10.1016/j.scico.2011.04.007\">https://doi.org/10.1016/j.scico.2011.04.007</a>.","ieee":"T. Ruhroth and H. Wehrheim, “Model evolution and refinement,” <i>Sci. Comput. Program.</i>, no. 3, pp. 270--289, 2012.","ama":"Ruhroth T, Wehrheim H. Model evolution and refinement. <i>Sci Comput Program</i>. 2012;(3):270--289. doi:<a href=\"https://doi.org/10.1016/j.scico.2011.04.007\">10.1016/j.scico.2011.04.007</a>","apa":"Ruhroth, T., &#38; Wehrheim, H. (2012). Model evolution and refinement. <i>Sci. Comput. Program.</i>, (3), 270--289. <a href=\"https://doi.org/10.1016/j.scico.2011.04.007\">https://doi.org/10.1016/j.scico.2011.04.007</a>","short":"T. Ruhroth, H. Wehrheim, Sci. Comput. Program. (2012) 270--289.","bibtex":"@article{Ruhroth_Wehrheim_2012, title={Model evolution and refinement}, DOI={<a href=\"https://doi.org/10.1016/j.scico.2011.04.007\">10.1016/j.scico.2011.04.007</a>}, number={3}, journal={Sci. Comput. Program.}, author={Ruhroth, Thomas and Wehrheim, Heike}, year={2012}, pages={270--289} }","mla":"Ruhroth, Thomas, and Heike Wehrheim. “Model Evolution and Refinement.” <i>Sci. Comput. Program.</i>, no. 3, 2012, pp. 270--289, doi:<a href=\"https://doi.org/10.1016/j.scico.2011.04.007\">10.1016/j.scico.2011.04.007</a>."},"page":"270--289","date_updated":"2022-01-06T06:59:03Z","date_created":"2018-06-13T08:17:58Z","author":[{"full_name":"Ruhroth, Thomas","last_name":"Ruhroth","first_name":"Thomas"},{"first_name":"Heike","full_name":"Wehrheim, Heike","id":"573","last_name":"Wehrheim"}],"title":"Model evolution and refinement","doi":"10.1016/j.scico.2011.04.007","type":"journal_article","publication":"Sci. Comput. Program.","status":"public","_id":"3181","user_id":"29719","department":[{"_id":"77"}]},{"status":"public","editor":[{"last_name":"Madhusudan","full_name":"Madhusudan, P.","first_name":"P."},{"last_name":"A. Seshia","full_name":"A. Seshia, Sanjit","first_name":"Sanjit"}],"type":"conference","publication":"Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings","series_title":"Lecture Notes in Computer Science","user_id":"29719","department":[{"_id":"77"}],"_id":"3182","citation":{"ama":"Schellhorn G, Wehrheim H, Derrick J. How to Prove Algorithms Linearisable. In: Madhusudan P, A. Seshia S, eds. <i>Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings</i>. Lecture Notes in Computer Science. ; 2012:243--259. doi:<a href=\"https://doi.org/10.1007/978-3-642-31424-7_21\">10.1007/978-3-642-31424-7_21</a>","chicago":"Schellhorn, Gerhard, Heike Wehrheim, and John Derrick. “How to Prove Algorithms Linearisable.” In <i>Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings</i>, edited by P. Madhusudan and Sanjit A. Seshia, 243--259. Lecture Notes in Computer Science, 2012. <a href=\"https://doi.org/10.1007/978-3-642-31424-7_21\">https://doi.org/10.1007/978-3-642-31424-7_21</a>.","ieee":"G. Schellhorn, H. Wehrheim, and J. Derrick, “How to Prove Algorithms Linearisable,” in <i>Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings</i>, 2012, pp. 243--259.","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.","mla":"Schellhorn, Gerhard, et al. “How to Prove Algorithms Linearisable.” <i>Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings</i>, edited by P. Madhusudan and Sanjit A. Seshia, 2012, pp. 243--259, doi:<a href=\"https://doi.org/10.1007/978-3-642-31424-7_21\">10.1007/978-3-642-31424-7_21</a>.","bibtex":"@inproceedings{Schellhorn_Wehrheim_Derrick_2012, series={Lecture Notes in Computer Science}, title={How to Prove Algorithms Linearisable}, DOI={<a href=\"https://doi.org/10.1007/978-3-642-31424-7_21\">10.1007/978-3-642-31424-7_21</a>}, 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} }","apa":"Schellhorn, G., Wehrheim, H., &#38; Derrick, J. (2012). How to Prove Algorithms Linearisable. In P. Madhusudan &#38; S. A. Seshia (Eds.), <i>Computer Aided Verification - 24th International Conference, {CAV} 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings</i> (pp. 243--259). <a href=\"https://doi.org/10.1007/978-3-642-31424-7_21\">https://doi.org/10.1007/978-3-642-31424-7_21</a>"},"page":"243--259","year":"2012","doi":"10.1007/978-3-642-31424-7_21","title":"How to Prove Algorithms Linearisable","date_created":"2018-06-13T08:19:33Z","author":[{"first_name":"Gerhard","last_name":"Schellhorn","full_name":"Schellhorn, Gerhard"},{"first_name":"Heike","full_name":"Wehrheim, Heike","id":"573","last_name":"Wehrheim"},{"first_name":"John","full_name":"Derrick, John","last_name":"Derrick"}],"date_updated":"2022-01-06T06:59:03Z"},{"date_created":"2017-10-17T12:42:47Z","author":[{"last_name":"Wonisch","full_name":"Wonisch, Daniel","first_name":"Daniel"},{"first_name":"Heike","id":"573","full_name":"Wehrheim, Heike","last_name":"Wehrheim"}],"date_updated":"2022-01-06T07:02:46Z","doi":"10.1007/978-3-642-34281-3_24","title":"Predicate Analysis with Block-Abstraction Memoization","has_accepted_license":"1","page":"332-347","citation":{"chicago":"Wonisch, Daniel, and Heike Wehrheim. “Predicate Analysis with Block-Abstraction Memoization.” In <i>Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)</i>, 332–47. LNCS, 2012. <a href=\"https://doi.org/10.1007/978-3-642-34281-3_24\">https://doi.org/10.1007/978-3-642-34281-3_24</a>.","ieee":"D. Wonisch and H. Wehrheim, “Predicate Analysis with Block-Abstraction Memoization,” in <i>Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)</i>, 2012, pp. 332–347.","ama":"Wonisch D, Wehrheim H. Predicate Analysis with Block-Abstraction Memoization. In: <i>Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)</i>. LNCS. ; 2012:332-347. doi:<a href=\"https://doi.org/10.1007/978-3-642-34281-3_24\">10.1007/978-3-642-34281-3_24</a>","bibtex":"@inproceedings{Wonisch_Wehrheim_2012, series={LNCS}, title={Predicate Analysis with Block-Abstraction Memoization}, DOI={<a href=\"https://doi.org/10.1007/978-3-642-34281-3_24\">10.1007/978-3-642-34281-3_24</a>}, 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} }","mla":"Wonisch, Daniel, and Heike Wehrheim. “Predicate Analysis with Block-Abstraction Memoization.” <i>Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)</i>, 2012, pp. 332–47, doi:<a href=\"https://doi.org/10.1007/978-3-642-34281-3_24\">10.1007/978-3-642-34281-3_24</a>.","short":"D. Wonisch, H. Wehrheim, in: Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 2012, pp. 332–347.","apa":"Wonisch, D., &#38; Wehrheim, H. (2012). Predicate Analysis with Block-Abstraction Memoization. In <i>Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)</i> (pp. 332–347). <a href=\"https://doi.org/10.1007/978-3-642-34281-3_24\">https://doi.org/10.1007/978-3-642-34281-3_24</a>"},"year":"2012","department":[{"_id":"77"}],"user_id":"477","series_title":"LNCS","_id":"590","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"_id":"3","name":"SFB 901 - Project Area B"}],"language":[{"iso":"eng"}],"file_date_updated":"2018-03-15T08:33:56Z","ddc":["040"],"publication":"Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)","type":"conference","status":"public","file":[{"date_created":"2018-03-15T08:33:56Z","creator":"florida","date_updated":"2018-03-15T08:33:56Z","access_level":"closed","file_name":"590-WonischWehrheim2012.pdf","file_id":"1258","file_size":320901,"content_type":"application/pdf","relation":"main_file","success":1}],"abstract":[{"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”.","lang":"eng"}]},{"year":"2012","date_created":"2017-10-17T12:42:50Z","title":"Heuristic-Guided Abstraction Refinement for Concurrent Systems","publication":"Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)","abstract":[{"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.","lang":"eng"}],"file":[{"file_name":"608-Timm2013-0main.pdf","file_id":"1250","access_level":"closed","file_size":396337,"date_created":"2018-03-15T08:15:33Z","creator":"florida","date_updated":"2018-03-15T08:15:33Z","relation":"main_file","success":1,"content_type":"application/pdf"}],"ddc":["040"],"language":[{"iso":"eng"}],"has_accepted_license":"1","page":"348-363","citation":{"chicago":"Timm, Nils, Heike Wehrheim, and Mike Czech. “Heuristic-Guided Abstraction Refinement for Concurrent Systems.” In <i>Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)</i>, 348–63. LNCS, 2012. <a href=\"https://doi.org/10.1007/978-3-642-34281-3_25\">https://doi.org/10.1007/978-3-642-34281-3_25</a>.","ieee":"N. Timm, H. Wehrheim, and M. Czech, “Heuristic-Guided Abstraction Refinement for Concurrent Systems,” in <i>Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)</i>, 2012, pp. 348–363.","ama":"Timm N, Wehrheim H, Czech M. Heuristic-Guided Abstraction Refinement for Concurrent Systems. In: <i>Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)</i>. LNCS. ; 2012:348-363. doi:<a href=\"https://doi.org/10.1007/978-3-642-34281-3_25\">10.1007/978-3-642-34281-3_25</a>","apa":"Timm, N., Wehrheim, H., &#38; Czech, M. (2012). Heuristic-Guided Abstraction Refinement for Concurrent Systems. In <i>Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)</i> (pp. 348–363). <a href=\"https://doi.org/10.1007/978-3-642-34281-3_25\">https://doi.org/10.1007/978-3-642-34281-3_25</a>","short":"N. Timm, H. Wehrheim, M. Czech, in: Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM), 2012, pp. 348–363.","bibtex":"@inproceedings{Timm_Wehrheim_Czech_2012, series={LNCS}, title={Heuristic-Guided Abstraction Refinement for Concurrent Systems}, DOI={<a href=\"https://doi.org/10.1007/978-3-642-34281-3_25\">10.1007/978-3-642-34281-3_25</a>}, 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} }","mla":"Timm, Nils, et al. “Heuristic-Guided Abstraction Refinement for Concurrent Systems.” <i>Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM)</i>, 2012, pp. 348–63, doi:<a href=\"https://doi.org/10.1007/978-3-642-34281-3_25\">10.1007/978-3-642-34281-3_25</a>."},"date_updated":"2022-01-06T07:02:52Z","author":[{"last_name":"Timm","full_name":"Timm, Nils","first_name":"Nils"},{"first_name":"Heike","last_name":"Wehrheim","full_name":"Wehrheim, Heike","id":"573"},{"first_name":"Mike","last_name":"Czech","full_name":"Czech, Mike"}],"doi":"10.1007/978-3-642-34281-3_25","type":"conference","status":"public","_id":"608","project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"name":"SFB 901 - Project Area B","_id":"3"}],"department":[{"_id":"77"}],"series_title":"LNCS","user_id":"477","file_date_updated":"2018-03-15T08:15:33Z"},{"file":[{"content_type":"application/pdf","relation":"main_file","success":1,"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","access_level":"closed","file_size":184000}],"abstract":[{"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.","lang":"eng"}],"publication":"Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","language":[{"iso":"eng"}],"ddc":["040"],"year":"2012","title":"Block Abstraction Memoization for CPAchecker","date_created":"2017-10-17T12:42:54Z","status":"public","type":"conference","file_date_updated":"2018-03-15T06:46:05Z","user_id":"477","series_title":"LNCS","department":[{"_id":"77"}],"project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"name":"SFB 901 - Project Area B","_id":"3"}],"_id":"627","citation":{"ama":"Wonisch D. Block Abstraction Memoization for CPAchecker. In: <i>Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)</i>. LNCS. ; 2012:531-533. doi:<a href=\"https://doi.org/10.1007/978-3-642-28756-5_41\">10.1007/978-3-642-28756-5_41</a>","ieee":"D. Wonisch, “Block Abstraction Memoization for CPAchecker,” in <i>Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)</i>, 2012, pp. 531–533.","chicago":"Wonisch, Daniel. “Block Abstraction Memoization for CPAchecker.” In <i>Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)</i>, 531–33. LNCS, 2012. <a href=\"https://doi.org/10.1007/978-3-642-28756-5_41\">https://doi.org/10.1007/978-3-642-28756-5_41</a>.","bibtex":"@inproceedings{Wonisch_2012, series={LNCS}, title={Block Abstraction Memoization for CPAchecker}, DOI={<a href=\"https://doi.org/10.1007/978-3-642-28756-5_41\">10.1007/978-3-642-28756-5_41</a>}, 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} }","mla":"Wonisch, Daniel. “Block Abstraction Memoization for CPAchecker.” <i>Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)</i>, 2012, pp. 531–33, doi:<a href=\"https://doi.org/10.1007/978-3-642-28756-5_41\">10.1007/978-3-642-28756-5_41</a>.","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.","apa":"Wonisch, D. (2012). Block Abstraction Memoization for CPAchecker. In <i>Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)</i> (pp. 531–533). <a href=\"https://doi.org/10.1007/978-3-642-28756-5_41\">https://doi.org/10.1007/978-3-642-28756-5_41</a>"},"page":"531-533","has_accepted_license":"1","doi":"10.1007/978-3-642-28756-5_41","author":[{"first_name":"Daniel","last_name":"Wonisch","full_name":"Wonisch, Daniel"}],"date_updated":"2022-01-06T07:02:59Z"},{"title":"Weaving-based configuration and modular transformation of multi-layer systems","date_created":"2017-10-17T12:42:42Z","year":"2012","language":[{"iso":"eng"}],"ddc":["040"],"file":[{"file_name":"565-Besova_et_al._-_2012_-_Weaving-Based_Configuration_and_Modular_Transformation_of_Multi-layer_Systems_01.pdf","file_id":"1276","access_level":"closed","file_size":589972,"date_created":"2018-03-15T10:24:06Z","creator":"florida","date_updated":"2018-03-15T10:24:06Z","relation":"main_file","success":1,"content_type":"application/pdf"}],"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."}],"publication":"Proceedings of the 15th International Conference on Model Driven Engineering Languages & Systems (MoDELS)","doi":"10.1007/978-3-642-33666-9_49","author":[{"last_name":"Besova","full_name":"Besova, Galina","first_name":"Galina"},{"full_name":"Walther, Sven","last_name":"Walther","first_name":"Sven"},{"last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike","first_name":"Heike"},{"full_name":"Becker, Steffen","last_name":"Becker","first_name":"Steffen"}],"date_updated":"2022-01-06T07:02:20Z","page":"776-792","citation":{"chicago":"Besova, Galina, Sven Walther, Heike Wehrheim, and Steffen Becker. “Weaving-Based Configuration and Modular Transformation of Multi-Layer Systems.” In <i>Proceedings of the 15th International Conference on Model Driven Engineering Languages &#38; Systems (MoDELS)</i>, 776–92. LNCS, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33666-9_49\">https://doi.org/10.1007/978-3-642-33666-9_49</a>.","ieee":"G. Besova, S. Walther, H. Wehrheim, and S. Becker, “Weaving-based configuration and modular transformation of multi-layer systems,” in <i>Proceedings of the 15th International Conference on Model Driven Engineering Languages &#38; Systems (MoDELS)</i>, 2012, pp. 776–792.","ama":"Besova G, Walther S, Wehrheim H, Becker S. Weaving-based configuration and modular transformation of multi-layer systems. In: <i>Proceedings of the 15th International Conference on Model Driven Engineering Languages &#38; Systems (MoDELS)</i>. LNCS. ; 2012:776-792. doi:<a href=\"https://doi.org/10.1007/978-3-642-33666-9_49\">10.1007/978-3-642-33666-9_49</a>","bibtex":"@inproceedings{Besova_Walther_Wehrheim_Becker_2012, series={LNCS}, title={Weaving-based configuration and modular transformation of multi-layer systems}, DOI={<a href=\"https://doi.org/10.1007/978-3-642-33666-9_49\">10.1007/978-3-642-33666-9_49</a>}, booktitle={Proceedings of the 15th International Conference on Model Driven Engineering Languages &#38; Systems (MoDELS)}, author={Besova, Galina and Walther, Sven and Wehrheim, Heike and Becker, Steffen}, year={2012}, pages={776–792}, collection={LNCS} }","short":"G. Besova, S. Walther, H. Wehrheim, S. Becker, in: Proceedings of the 15th International Conference on Model Driven Engineering Languages &#38; Systems (MoDELS), 2012, pp. 776–792.","mla":"Besova, Galina, et al. “Weaving-Based Configuration and Modular Transformation of Multi-Layer Systems.” <i>Proceedings of the 15th International Conference on Model Driven Engineering Languages &#38; Systems (MoDELS)</i>, 2012, pp. 776–92, doi:<a href=\"https://doi.org/10.1007/978-3-642-33666-9_49\">10.1007/978-3-642-33666-9_49</a>.","apa":"Besova, G., Walther, S., Wehrheim, H., &#38; Becker, S. (2012). Weaving-based configuration and modular transformation of multi-layer systems. In <i>Proceedings of the 15th International Conference on Model Driven Engineering Languages &#38; Systems (MoDELS)</i> (pp. 776–792). <a href=\"https://doi.org/10.1007/978-3-642-33666-9_49\">https://doi.org/10.1007/978-3-642-33666-9_49</a>"},"has_accepted_license":"1","file_date_updated":"2018-03-15T10:24:06Z","department":[{"_id":"77"}],"user_id":"477","series_title":"LNCS","_id":"565","project":[{"_id":"1","name":"SFB 901"},{"_id":"11","name":"SFB 901 - Subprojekt B3"},{"name":"SFB 901 - Project Area B","_id":"3"}],"status":"public","type":"conference"},{"status":"public","type":"journal_article","publication":"Electr. Notes Theor. Comput. Sci.","_id":"3183","user_id":"29719","department":[{"_id":"77"}],"year":"2011","citation":{"ama":"Schneider S, Treharne H, Wehrheim H. Bounded Retransmission in Event-B{\\(\\parallel\\)}CSP: a Case Study. <i>Electr Notes Theor Comput Sci</i>. 2011:69--80. doi:<a href=\"https://doi.org/10.1016/j.entcs.2011.11.019\">10.1016/j.entcs.2011.11.019</a>","ieee":"S. Schneider, H. Treharne, and H. Wehrheim, “Bounded Retransmission in Event-B{\\(\\parallel\\)}CSP: a Case Study,” <i>Electr. Notes Theor. Comput. Sci.</i>, pp. 69--80, 2011.","chicago":"Schneider, Steve, Helen Treharne, and Heike Wehrheim. “Bounded Retransmission in Event-B{\\(\\parallel\\)}CSP: A Case Study.” <i>Electr. Notes Theor. Comput. Sci.</i>, 2011, 69--80. <a href=\"https://doi.org/10.1016/j.entcs.2011.11.019\">https://doi.org/10.1016/j.entcs.2011.11.019</a>.","mla":"Schneider, Steve, et al. “Bounded Retransmission in Event-B{\\(\\parallel\\)}CSP: A Case Study.” <i>Electr. Notes Theor. Comput. Sci.</i>, 2011, pp. 69--80, doi:<a href=\"https://doi.org/10.1016/j.entcs.2011.11.019\">10.1016/j.entcs.2011.11.019</a>.","bibtex":"@article{Schneider_Treharne_Wehrheim_2011, title={Bounded Retransmission in Event-B{\\(\\parallel\\)}CSP: a Case Study}, DOI={<a href=\"https://doi.org/10.1016/j.entcs.2011.11.019\">10.1016/j.entcs.2011.11.019</a>}, journal={Electr. Notes Theor. Comput. Sci.}, author={Schneider, Steve and Treharne, Helen and Wehrheim, Heike}, year={2011}, pages={69--80} }","short":"S. Schneider, H. Treharne, H. Wehrheim, Electr. Notes Theor. Comput. Sci. (2011) 69--80.","apa":"Schneider, S., Treharne, H., &#38; Wehrheim, H. (2011). Bounded Retransmission in Event-B{\\(\\parallel\\)}CSP: a Case Study. <i>Electr. Notes Theor. Comput. Sci.</i>, 69--80. <a href=\"https://doi.org/10.1016/j.entcs.2011.11.019\">https://doi.org/10.1016/j.entcs.2011.11.019</a>"},"page":"69--80","title":"Bounded Retransmission in Event-B{\\(\\parallel\\)}CSP: a Case Study","doi":"10.1016/j.entcs.2011.11.019","date_updated":"2022-01-06T06:59:03Z","date_created":"2018-06-13T08:20:47Z","author":[{"first_name":"Steve","full_name":"Schneider, Steve","last_name":"Schneider"},{"first_name":"Helen","last_name":"Treharne","full_name":"Treharne, Helen"},{"first_name":"Heike","last_name":"Wehrheim","full_name":"Wehrheim, Heike","id":"573"}]},{"_id":"3184","department":[{"_id":"77"}],"user_id":"29719","publication":"{ACM} Trans. Program. Lang. Syst.","type":"journal_article","status":"public","date_updated":"2022-01-06T06:59:03Z","author":[{"first_name":"John","last_name":"Derrick","full_name":"Derrick, John"},{"first_name":"Gerhard","full_name":"Schellhorn, Gerhard","last_name":"Schellhorn"},{"last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike","first_name":"Heike"}],"date_created":"2018-06-13T08:22:02Z","title":"Mechanically verified proof obligations for linearizability","doi":"10.1145/1889997.1890001","issue":"1","year":"2011","page":"4:1--4:43","citation":{"apa":"Derrick, J., Schellhorn, G., &#38; Wehrheim, H. (2011). Mechanically verified proof obligations for linearizability. <i>{ACM} Trans. Program. Lang. Syst.</i>, (1), 4:1--4:43. <a href=\"https://doi.org/10.1145/1889997.1890001\">https://doi.org/10.1145/1889997.1890001</a>","bibtex":"@article{Derrick_Schellhorn_Wehrheim_2011, title={Mechanically verified proof obligations for linearizability}, DOI={<a href=\"https://doi.org/10.1145/1889997.1890001\">10.1145/1889997.1890001</a>}, number={1}, journal={{ACM} Trans. Program. Lang. Syst.}, author={Derrick, John and Schellhorn, Gerhard and Wehrheim, Heike}, year={2011}, pages={4:1--4:43} }","short":"J. Derrick, G. Schellhorn, H. Wehrheim, {ACM} Trans. Program. Lang. Syst. (2011) 4:1--4:43.","mla":"Derrick, John, et al. “Mechanically Verified Proof Obligations for Linearizability.” <i>{ACM} Trans. Program. Lang. Syst.</i>, no. 1, 2011, pp. 4:1--4:43, doi:<a href=\"https://doi.org/10.1145/1889997.1890001\">10.1145/1889997.1890001</a>.","ama":"Derrick J, Schellhorn G, Wehrheim H. Mechanically verified proof obligations for linearizability. <i>{ACM} Trans Program Lang Syst</i>. 2011;(1):4:1--4:43. doi:<a href=\"https://doi.org/10.1145/1889997.1890001\">10.1145/1889997.1890001</a>","ieee":"J. Derrick, G. Schellhorn, and H. Wehrheim, “Mechanically verified proof obligations for linearizability,” <i>{ACM} Trans. Program. Lang. Syst.</i>, no. 1, pp. 4:1--4:43, 2011.","chicago":"Derrick, John, Gerhard Schellhorn, and Heike Wehrheim. “Mechanically Verified Proof Obligations for Linearizability.” <i>{ACM} Trans. Program. Lang. Syst.</i>, no. 1 (2011): 4:1--4:43. <a href=\"https://doi.org/10.1145/1889997.1890001\">https://doi.org/10.1145/1889997.1890001</a>."}},{"_id":"3185","department":[{"_id":"77"}],"user_id":"29719","status":"public","publication":"37th {EUROMICRO} Conference on Software Engineering and Advanced Applications, {SEAA} 2011, Oulu, Finland, August 30 - September 2, 2011","type":"conference","title":"ReL: {A} Generic Refactoring Language for Specification and Execution","doi":"10.1109/SEAA.2011.22","date_updated":"2022-01-06T06:59:03Z","date_created":"2018-06-13T08:23:28Z","author":[{"full_name":"Ruhroth, Thomas","last_name":"Ruhroth","first_name":"Thomas"},{"id":"573","full_name":"Wehrheim, Heike","last_name":"Wehrheim","first_name":"Heike"},{"full_name":"Ziegert, Steffen","last_name":"Ziegert","first_name":"Steffen"}],"year":"2011","page":"83--90","citation":{"short":"T. Ruhroth, H. Wehrheim, S. Ziegert, in: 37th {EUROMICRO} Conference on Software Engineering and Advanced Applications, {SEAA} 2011, Oulu, Finland, August 30 - September 2, 2011, 2011, pp. 83--90.","bibtex":"@inproceedings{Ruhroth_Wehrheim_Ziegert_2011, title={ReL: {A} Generic Refactoring Language for Specification and Execution}, DOI={<a href=\"https://doi.org/10.1109/SEAA.2011.22\">10.1109/SEAA.2011.22</a>}, booktitle={37th {EUROMICRO} Conference on Software Engineering and Advanced Applications, {SEAA} 2011, Oulu, Finland, August 30 - September 2, 2011}, author={Ruhroth, Thomas and Wehrheim, Heike and Ziegert, Steffen}, year={2011}, pages={83--90} }","mla":"Ruhroth, Thomas, et al. “ReL: {A} Generic Refactoring Language for Specification and Execution.” <i>37th {EUROMICRO} Conference on Software Engineering and Advanced Applications, {SEAA} 2011, Oulu, Finland, August 30 - September 2, 2011</i>, 2011, pp. 83--90, doi:<a href=\"https://doi.org/10.1109/SEAA.2011.22\">10.1109/SEAA.2011.22</a>.","apa":"Ruhroth, T., Wehrheim, H., &#38; Ziegert, S. (2011). ReL: {A} Generic Refactoring Language for Specification and Execution. In <i>37th {EUROMICRO} Conference on Software Engineering and Advanced Applications, {SEAA} 2011, Oulu, Finland, August 30 - September 2, 2011</i> (pp. 83--90). <a href=\"https://doi.org/10.1109/SEAA.2011.22\">https://doi.org/10.1109/SEAA.2011.22</a>","ieee":"T. Ruhroth, H. Wehrheim, and S. Ziegert, “ReL: {A} Generic Refactoring Language for Specification and Execution,” in <i>37th {EUROMICRO} Conference on Software Engineering and Advanced Applications, {SEAA} 2011, Oulu, Finland, August 30 - September 2, 2011</i>, 2011, pp. 83--90.","chicago":"Ruhroth, Thomas, Heike Wehrheim, and Steffen Ziegert. “ReL: {A} Generic Refactoring Language for Specification and Execution.” In <i>37th {EUROMICRO} Conference on Software Engineering and Advanced Applications, {SEAA} 2011, Oulu, Finland, August 30 - September 2, 2011</i>, 83--90, 2011. <a href=\"https://doi.org/10.1109/SEAA.2011.22\">https://doi.org/10.1109/SEAA.2011.22</a>.","ama":"Ruhroth T, Wehrheim H, Ziegert S. ReL: {A} Generic Refactoring Language for Specification and Execution. In: <i>37th {EUROMICRO} Conference on Software Engineering and Advanced Applications, {SEAA} 2011, Oulu, Finland, August 30 - September 2, 2011</i>. ; 2011:83--90. doi:<a href=\"https://doi.org/10.1109/SEAA.2011.22\">10.1109/SEAA.2011.22</a>"}},{"type":"conference","publication":"{FM} 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings","editor":[{"full_name":"J. Butler, Michael","last_name":"J. Butler","first_name":"Michael"},{"full_name":"Schulte, Wolfram","last_name":"Schulte","first_name":"Wolfram"}],"status":"public","_id":"3186","series_title":"Lecture Notes in Computer Science","user_id":"29719","department":[{"_id":"77"}],"year":"2011","citation":{"apa":"Derrick, J., Schellhorn, G., &#38; Wehrheim, H. (2011). Verifying Linearisability with Potential Linearisation Points. In M. J. Butler &#38; W. Schulte (Eds.), <i>{FM} 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings</i> (pp. 323--337). <a href=\"https://doi.org/10.1007/978-3-642-21437-0_25\">https://doi.org/10.1007/978-3-642-21437-0_25</a>","mla":"Derrick, John, et al. “Verifying Linearisability with Potential Linearisation Points.” <i>{FM} 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings</i>, edited by Michael J. Butler and Wolfram Schulte, 2011, pp. 323--337, doi:<a href=\"https://doi.org/10.1007/978-3-642-21437-0_25\">10.1007/978-3-642-21437-0_25</a>.","bibtex":"@inproceedings{Derrick_Schellhorn_Wehrheim_2011, series={Lecture Notes in Computer Science}, title={Verifying Linearisability with Potential Linearisation Points}, DOI={<a href=\"https://doi.org/10.1007/978-3-642-21437-0_25\">10.1007/978-3-642-21437-0_25</a>}, booktitle={{FM} 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings}, author={Derrick, John and Schellhorn, Gerhard and Wehrheim, Heike}, editor={J. Butler, Michael and Schulte, WolframEditors}, year={2011}, pages={323--337}, collection={Lecture Notes in Computer Science} }","short":"J. Derrick, G. Schellhorn, H. Wehrheim, in: M. J. Butler, W. Schulte (Eds.), {FM} 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings, 2011, pp. 323--337.","ama":"Derrick J, Schellhorn G, Wehrheim H. Verifying Linearisability with Potential Linearisation Points. In: J. Butler M, Schulte W, eds. <i>{FM} 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings</i>. Lecture Notes in Computer Science. ; 2011:323--337. doi:<a href=\"https://doi.org/10.1007/978-3-642-21437-0_25\">10.1007/978-3-642-21437-0_25</a>","ieee":"J. Derrick, G. Schellhorn, and H. Wehrheim, “Verifying Linearisability with Potential Linearisation Points,” in <i>{FM} 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings</i>, 2011, pp. 323--337.","chicago":"Derrick, John, Gerhard Schellhorn, and Heike Wehrheim. “Verifying Linearisability with Potential Linearisation Points.” In <i>{FM} 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings</i>, edited by Michael J. Butler and Wolfram Schulte, 323--337. Lecture Notes in Computer Science, 2011. <a href=\"https://doi.org/10.1007/978-3-642-21437-0_25\">https://doi.org/10.1007/978-3-642-21437-0_25</a>."},"page":"323--337","date_updated":"2022-01-06T06:59:03Z","date_created":"2018-06-13T08:25:07Z","author":[{"first_name":"John","last_name":"Derrick","full_name":"Derrick, John"},{"first_name":"Gerhard","last_name":"Schellhorn","full_name":"Schellhorn, Gerhard"},{"first_name":"Heike","last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike"}],"title":"Verifying Linearisability with Potential Linearisation Points","doi":"10.1007/978-3-642-21437-0_25"},{"series_title":"Lecture Notes in Computer Science","user_id":"29719","department":[{"_id":"77"}],"_id":"3187","type":"conference","publication":"Formal Methods, Foundations and Applications - 14th Brazilian Symposium, {SBMF} 2011, S{\\~{a}}o Paulo, Brazil, September 26-30, 2011, Revised Selected Papers","status":"public","editor":[{"first_name":"Adenilso","full_name":"da Silva Sim{\\~{a}}o, Adenilso","last_name":"da Silva Sim{\\~{a}}o"},{"first_name":"Carroll","full_name":"Morgan, Carroll","last_name":"Morgan"}],"date_created":"2018-06-13T08:32:12Z","author":[{"first_name":"Dominik","last_name":"Steenken","full_name":"Steenken, Dominik"},{"full_name":"Wehrheim, Heike","id":"573","last_name":"Wehrheim","first_name":"Heike"},{"first_name":"Daniel","full_name":"Wonisch, Daniel","last_name":"Wonisch"}],"date_updated":"2022-01-06T06:59:03Z","doi":"10.1007/978-3-642-25032-3_7","title":"Sound and Complete Abstract Graph Transformation","citation":{"chicago":"Steenken, Dominik, Heike Wehrheim, and Daniel Wonisch. “Sound and Complete Abstract Graph Transformation.” In <i>Formal Methods, Foundations and Applications - 14th Brazilian Symposium, {SBMF} 2011, S{\\~{a}}o Paulo, Brazil, September 26-30, 2011, Revised Selected Papers</i>, edited by Adenilso da Silva Sim{\\~{a}}o and Carroll Morgan, 92--107. Lecture Notes in Computer Science, 2011. <a href=\"https://doi.org/10.1007/978-3-642-25032-3_7\">https://doi.org/10.1007/978-3-642-25032-3_7</a>.","ieee":"D. Steenken, H. Wehrheim, and D. Wonisch, “Sound and Complete Abstract Graph Transformation,” in <i>Formal Methods, Foundations and Applications - 14th Brazilian Symposium, {SBMF} 2011, S{\\~{a}}o Paulo, Brazil, September 26-30, 2011, Revised Selected Papers</i>, 2011, pp. 92--107.","ama":"Steenken D, Wehrheim H, Wonisch D. Sound and Complete Abstract Graph Transformation. In: da Silva Sim{\\~{a}}o A, Morgan C, eds. <i>Formal Methods, Foundations and Applications - 14th Brazilian Symposium, {SBMF} 2011, S{\\~{a}}o Paulo, Brazil, September 26-30, 2011, Revised Selected Papers</i>. Lecture Notes in Computer Science. ; 2011:92--107. doi:<a href=\"https://doi.org/10.1007/978-3-642-25032-3_7\">10.1007/978-3-642-25032-3_7</a>","bibtex":"@inproceedings{Steenken_Wehrheim_Wonisch_2011, series={Lecture Notes in Computer Science}, title={Sound and Complete Abstract Graph Transformation}, DOI={<a href=\"https://doi.org/10.1007/978-3-642-25032-3_7\">10.1007/978-3-642-25032-3_7</a>}, booktitle={Formal Methods, Foundations and Applications - 14th Brazilian Symposium, {SBMF} 2011, S{\\~{a}}o Paulo, Brazil, September 26-30, 2011, Revised Selected Papers}, author={Steenken, Dominik and Wehrheim, Heike and Wonisch, Daniel}, editor={da Silva Sim{\\~{a}}o, Adenilso and Morgan, CarrollEditors}, year={2011}, pages={92--107}, collection={Lecture Notes in Computer Science} }","short":"D. Steenken, H. Wehrheim, D. Wonisch, in: A. da Silva Sim{\\~{a}}o, C. Morgan (Eds.), Formal Methods, Foundations and Applications - 14th Brazilian Symposium, {SBMF} 2011, S{\\~{a}}o Paulo, Brazil, September 26-30, 2011, Revised Selected Papers, 2011, pp. 92--107.","mla":"Steenken, Dominik, et al. “Sound and Complete Abstract Graph Transformation.” <i>Formal Methods, Foundations and Applications - 14th Brazilian Symposium, {SBMF} 2011, S{\\~{a}}o Paulo, Brazil, September 26-30, 2011, Revised Selected Papers</i>, edited by Adenilso da Silva Sim{\\~{a}}o and Carroll Morgan, 2011, pp. 92--107, doi:<a href=\"https://doi.org/10.1007/978-3-642-25032-3_7\">10.1007/978-3-642-25032-3_7</a>.","apa":"Steenken, D., Wehrheim, H., &#38; Wonisch, D. (2011). Sound and Complete Abstract Graph Transformation. In A. da Silva Sim{\\~{a}}o &#38; C. Morgan (Eds.), <i>Formal Methods, Foundations and Applications - 14th Brazilian Symposium, {SBMF} 2011, S{\\~{a}}o Paulo, Brazil, September 26-30, 2011, Revised Selected Papers</i> (pp. 92--107). <a href=\"https://doi.org/10.1007/978-3-642-25032-3_7\">https://doi.org/10.1007/978-3-642-25032-3_7</a>"},"page":"92--107","year":"2011"},{"publication":"Proceedings 15th International Refinement Workshop, Refine@FM 2011, Limerick, Ireland, 20th June 2011.","type":"conference","editor":[{"first_name":"John","full_name":"Derrick, John","last_name":"Derrick"},{"first_name":"Eerke","full_name":"A. Boiten, Eerke","last_name":"A. Boiten"},{"full_name":"Reeves, Steve","last_name":"Reeves","first_name":"Steve"}],"status":"public","_id":"3188","department":[{"_id":"77"}],"user_id":"29719","series_title":"{EPTCS}","year":"2011","page":"139--154","citation":{"chicago":"Schneider, Steve, Helen Treharne, and Heike Wehrheim. “A {CSP} Account of Event-B Refinement.” In <i>Proceedings 15th International Refinement Workshop, Refine@FM 2011, Limerick, Ireland, 20th June 2011.</i>, edited by John Derrick, Eerke A. Boiten, and Steve Reeves, 139--154. {EPTCS}, 2011. <a href=\"https://doi.org/10.4204/EPTCS.55.9\">https://doi.org/10.4204/EPTCS.55.9</a>.","ieee":"S. Schneider, H. Treharne, and H. Wehrheim, “A {CSP} Account of Event-B Refinement,” in <i>Proceedings 15th International Refinement Workshop, Refine@FM 2011, Limerick, Ireland, 20th June 2011.</i>, 2011, pp. 139--154.","ama":"Schneider S, Treharne H, Wehrheim H. A {CSP} Account of Event-B Refinement. In: Derrick J, A. Boiten E, Reeves S, eds. <i>Proceedings 15th International Refinement Workshop, Refine@FM 2011, Limerick, Ireland, 20th June 2011.</i> {EPTCS}. ; 2011:139--154. doi:<a href=\"https://doi.org/10.4204/EPTCS.55.9\">10.4204/EPTCS.55.9</a>","bibtex":"@inproceedings{Schneider_Treharne_Wehrheim_2011, series={{EPTCS}}, title={A {CSP} Account of Event-B Refinement}, DOI={<a href=\"https://doi.org/10.4204/EPTCS.55.9\">10.4204/EPTCS.55.9</a>}, booktitle={Proceedings 15th International Refinement Workshop, Refine@FM 2011, Limerick, Ireland, 20th June 2011.}, author={Schneider, Steve and Treharne, Helen and Wehrheim, Heike}, editor={Derrick, John and A. Boiten, Eerke and Reeves, SteveEditors}, year={2011}, pages={139--154}, collection={{EPTCS}} }","mla":"Schneider, Steve, et al. “A {CSP} Account of Event-B Refinement.” <i>Proceedings 15th International Refinement Workshop, Refine@FM 2011, Limerick, Ireland, 20th June 2011.</i>, edited by John Derrick et al., 2011, pp. 139--154, doi:<a href=\"https://doi.org/10.4204/EPTCS.55.9\">10.4204/EPTCS.55.9</a>.","short":"S. Schneider, H. Treharne, H. Wehrheim, in: J. Derrick, E. A. Boiten, S. Reeves (Eds.), Proceedings 15th International Refinement Workshop, Refine@FM 2011, Limerick, Ireland, 20th June 2011., 2011, pp. 139--154.","apa":"Schneider, S., Treharne, H., &#38; Wehrheim, H. (2011). A {CSP} Account of Event-B Refinement. In J. Derrick, E. A. Boiten, &#38; S. Reeves (Eds.), <i>Proceedings 15th International Refinement Workshop, Refine@FM 2011, Limerick, Ireland, 20th June 2011.</i> (pp. 139--154). <a href=\"https://doi.org/10.4204/EPTCS.55.9\">https://doi.org/10.4204/EPTCS.55.9</a>"},"date_updated":"2022-01-06T06:59:03Z","date_created":"2018-06-13T08:43:19Z","author":[{"last_name":"Schneider","full_name":"Schneider, Steve","first_name":"Steve"},{"full_name":"Treharne, Helen","last_name":"Treharne","first_name":"Helen"},{"first_name":"Heike","id":"573","full_name":"Wehrheim, Heike","last_name":"Wehrheim"}],"title":"A {CSP} Account of Event-B Refinement","doi":"10.4204/EPTCS.55.9"},{"doi":"10.1016/j.scico.2011.01.009","author":[{"full_name":"Leuschel, Michael","last_name":"Leuschel","first_name":"Michael"},{"first_name":"Heike","full_name":"Wehrheim, Heike","id":"573","last_name":"Wehrheim"}],"date_updated":"2022-01-06T07:03:06Z","citation":{"ieee":"M. Leuschel and H. Wehrheim, “Selected papers on Integrated Formal Methods (iFM09),” <i>Science of Computer Programming</i>, no. 10, pp. 835--836, 2011.","chicago":"Leuschel, Michael, and Heike Wehrheim. “Selected Papers on Integrated Formal Methods (IFM09).” <i>Science of Computer Programming</i>, no. 10 (2011): 835--836. <a href=\"https://doi.org/10.1016/j.scico.2011.01.009\">https://doi.org/10.1016/j.scico.2011.01.009</a>.","ama":"Leuschel M, Wehrheim H. Selected papers on Integrated Formal Methods (iFM09). <i>Science of Computer Programming</i>. 2011;(10):835--836. doi:<a href=\"https://doi.org/10.1016/j.scico.2011.01.009\">10.1016/j.scico.2011.01.009</a>","apa":"Leuschel, M., &#38; Wehrheim, H. (2011). Selected papers on Integrated Formal Methods (iFM09). <i>Science of Computer Programming</i>, (10), 835--836. <a href=\"https://doi.org/10.1016/j.scico.2011.01.009\">https://doi.org/10.1016/j.scico.2011.01.009</a>","mla":"Leuschel, Michael, and Heike Wehrheim. “Selected Papers on Integrated Formal Methods (IFM09).” <i>Science of Computer Programming</i>, no. 10, Elsevier, 2011, pp. 835--836, doi:<a href=\"https://doi.org/10.1016/j.scico.2011.01.009\">10.1016/j.scico.2011.01.009</a>.","bibtex":"@article{Leuschel_Wehrheim_2011, title={Selected papers on Integrated Formal Methods (iFM09)}, DOI={<a href=\"https://doi.org/10.1016/j.scico.2011.01.009\">10.1016/j.scico.2011.01.009</a>}, number={10}, journal={Science of Computer Programming}, publisher={Elsevier}, author={Leuschel, Michael and Wehrheim, Heike}, year={2011}, pages={835--836} }","short":"M. Leuschel, H. Wehrheim, Science of Computer Programming (2011) 835--836."},"page":"835--836","has_accepted_license":"1","file_date_updated":"2018-03-14T13:56:48Z","user_id":"477","department":[{"_id":"77"}],"project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Subprojekt B3","_id":"11"},{"_id":"12","name":"SFB 901 - Subproject B4"},{"name":"SFB 901 - Project Area B","_id":"3"}],"_id":"647","status":"public","type":"journal_article","title":"Selected papers on Integrated Formal Methods (iFM09)","date_created":"2017-10-17T12:42:58Z","publisher":"Elsevier","year":"2011","issue":"10","language":[{"iso":"eng"}],"ddc":["040"],"file":[{"file_size":139105,"access_level":"closed","file_id":"1226","file_name":"647-LeuschelWehrheim.pdf","date_updated":"2018-03-14T13:56:48Z","date_created":"2018-03-14T13:56:48Z","creator":"florida","success":1,"relation":"main_file","content_type":"application/pdf"}],"publication":"Science of Computer Programming"},{"publication":"Electronic Notes in Theoretical Computer Science","type":"journal_article","status":"public","file":[{"content_type":"application/pdf","relation":"main_file","success":1,"date_created":"2018-03-14T13:55:38Z","creator":"florida","date_updated":"2018-03-14T13:55:38Z","file_name":"649-ETAPS2011-Besova-Wehrheim-Wagner_01.pdf","access_level":"closed","file_id":"1225","file_size":534727}],"abstract":[{"text":"Today, the concept of service oriented architectures provides a way of building integrated solutions out of existing services. To this end, services from different providers are composed using advanced orchestration and choreography techniques. However, while this principle allows for greater flexibility at a smaller cost, the use of third party services also includes a risk: Deployed services might not work as claimed by their providers. In this paper, we propose a technique for analyzing the expected reliability of service compositions based on ratings given by (previous) service users. Every service thereby comes with a reputation, and the analysis computes an overall reliability of a service composition from the reputations of its constituent services. The proposed model-driven approach proceeds by translating statechart models of service compositions into input for a probabilistic model checker (PRISM) using state-of-the-art model transformations techniques. The approach has been implemented as an Eclipse plug-in and is fully compliant with UML.","lang":"eng"}],"department":[{"_id":"77"}],"user_id":"477","_id":"649","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Subprojekt B3","_id":"11"},{"name":"SFB 901 - Project Area B","_id":"3"}],"file_date_updated":"2018-03-14T13:55:38Z","language":[{"iso":"eng"}],"ddc":["040"],"issue":"2","has_accepted_license":"1","page":"3-16","citation":{"chicago":"Besova, Galina, Heike Wehrheim, and Annika Wagner. “Reputation-Based Reliability Prediction of Service Compositions.” <i>Electronic Notes in Theoretical Computer Science</i>, no. 2 (2011): 3–16. <a href=\"https://doi.org/10.1016/j.entcs.2011.11.008\">https://doi.org/10.1016/j.entcs.2011.11.008</a>.","ieee":"G. Besova, H. Wehrheim, and A. Wagner, “Reputation-based Reliability Prediction of Service Compositions,” <i>Electronic Notes in Theoretical Computer Science</i>, no. 2, pp. 3–16, 2011.","ama":"Besova G, Wehrheim H, Wagner A. Reputation-based Reliability Prediction of Service Compositions. <i>Electronic Notes in Theoretical Computer Science</i>. 2011;(2):3-16. doi:<a href=\"https://doi.org/10.1016/j.entcs.2011.11.008\">10.1016/j.entcs.2011.11.008</a>","apa":"Besova, G., Wehrheim, H., &#38; Wagner, A. (2011). Reputation-based Reliability Prediction of Service Compositions. <i>Electronic Notes in Theoretical Computer Science</i>, (2), 3–16. <a href=\"https://doi.org/10.1016/j.entcs.2011.11.008\">https://doi.org/10.1016/j.entcs.2011.11.008</a>","bibtex":"@article{Besova_Wehrheim_Wagner_2011, title={Reputation-based Reliability Prediction of Service Compositions}, DOI={<a href=\"https://doi.org/10.1016/j.entcs.2011.11.008\">10.1016/j.entcs.2011.11.008</a>}, number={2}, journal={Electronic Notes in Theoretical Computer Science}, publisher={Elsevier}, author={Besova, Galina and Wehrheim, Heike and Wagner, Annika}, year={2011}, pages={3–16} }","mla":"Besova, Galina, et al. “Reputation-Based Reliability Prediction of Service Compositions.” <i>Electronic Notes in Theoretical Computer Science</i>, no. 2, Elsevier, 2011, pp. 3–16, doi:<a href=\"https://doi.org/10.1016/j.entcs.2011.11.008\">10.1016/j.entcs.2011.11.008</a>.","short":"G. Besova, H. Wehrheim, A. Wagner, Electronic Notes in Theoretical Computer Science (2011) 3–16."},"year":"2011","date_created":"2017-10-17T12:42:58Z","author":[{"last_name":"Besova","full_name":"Besova, Galina","first_name":"Galina"},{"id":"573","full_name":"Wehrheim, Heike","last_name":"Wehrheim","first_name":"Heike"},{"last_name":"Wagner","full_name":"Wagner, Annika","first_name":"Annika"}],"publisher":"Elsevier","date_updated":"2022-01-06T07:03:07Z","doi":"10.1016/j.entcs.2011.11.008","title":"Reputation-based Reliability Prediction of Service Compositions"},{"language":[{"iso":"eng"}],"_id":"658","project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"_id":"3","name":"SFB 901 - Project Area B"}],"department":[{"_id":"77"}],"user_id":"477","status":"public","type":"mastersthesis","title":"Function Specification Inference Using Craig Interpolation","date_updated":"2022-01-06T07:03:12Z","publisher":"Universität Paderborn","supervisor":[{"first_name":"Heike","full_name":"Wehrheim, Heike","id":"573","last_name":"Wehrheim"}],"author":[{"first_name":"Alexander","full_name":"Schremmer, Alexander","last_name":"Schremmer"}],"date_created":"2017-10-17T12:43:00Z","year":"2011","citation":{"ama":"Schremmer A. <i>Function Specification Inference Using Craig Interpolation</i>. Universität Paderborn; 2011.","chicago":"Schremmer, Alexander. <i>Function Specification Inference Using Craig Interpolation</i>. Universität Paderborn, 2011.","ieee":"A. Schremmer, <i>Function Specification Inference Using Craig Interpolation</i>. Universität Paderborn, 2011.","short":"A. Schremmer, Function Specification Inference Using Craig Interpolation, Universität Paderborn, 2011.","bibtex":"@book{Schremmer_2011, title={Function Specification Inference Using Craig Interpolation}, publisher={Universität Paderborn}, author={Schremmer, Alexander}, year={2011} }","mla":"Schremmer, Alexander. <i>Function Specification Inference Using Craig Interpolation</i>. Universität Paderborn, 2011.","apa":"Schremmer, A. (2011). <i>Function Specification Inference Using Craig Interpolation</i>. Universität Paderborn."}},{"editor":[{"last_name":"M{\\'{e}}ry","full_name":"M{\\'{e}}ry, Dominique","first_name":"Dominique"},{"first_name":"Stephan","full_name":"Merz, Stephan","last_name":"Merz"}],"status":"public","type":"conference","publication":"Integrated Formal Methods - 8th International Conference, {IFM} 2010, Nancy, France, October 11-14, 2010. Proceedings","_id":"3195","series_title":"Lecture Notes in Computer Science","user_id":"29719","department":[{"_id":"77"}],"year":"2010","citation":{"bibtex":"@inproceedings{Schneider_Treharne_Wehrheim_2010, series={Lecture Notes in Computer Science}, title={A {CSP} Approach to Control in Event-B}, DOI={<a href=\"https://doi.org/10.1007/978-3-642-16265-7_19\">10.1007/978-3-642-16265-7_19</a>}, booktitle={Integrated Formal Methods - 8th International Conference, {IFM} 2010, Nancy, France, October 11-14, 2010. Proceedings}, author={Schneider, Steve and Treharne, Helen and Wehrheim, Heike}, editor={M{\\’{e}}ry, Dominique and Merz, StephanEditors}, year={2010}, pages={260--274}, collection={Lecture Notes in Computer Science} }","mla":"Schneider, Steve, et al. “A {CSP} Approach to Control in Event-B.” <i>Integrated Formal Methods - 8th International Conference, {IFM} 2010, Nancy, France, October 11-14, 2010. Proceedings</i>, edited by Dominique M{\\’{e}}ry and Stephan Merz, 2010, pp. 260--274, doi:<a href=\"https://doi.org/10.1007/978-3-642-16265-7_19\">10.1007/978-3-642-16265-7_19</a>.","short":"S. Schneider, H. Treharne, H. Wehrheim, in: D. M{\\’{e}}ry, S. Merz (Eds.), Integrated Formal Methods - 8th International Conference, {IFM} 2010, Nancy, France, October 11-14, 2010. Proceedings, 2010, pp. 260--274.","apa":"Schneider, S., Treharne, H., &#38; Wehrheim, H. (2010). A {CSP} Approach to Control in Event-B. In D. M{\\’{e}}ry &#38; S. Merz (Eds.), <i>Integrated Formal Methods - 8th International Conference, {IFM} 2010, Nancy, France, October 11-14, 2010. Proceedings</i> (pp. 260--274). <a href=\"https://doi.org/10.1007/978-3-642-16265-7_19\">https://doi.org/10.1007/978-3-642-16265-7_19</a>","chicago":"Schneider, Steve, Helen Treharne, and Heike Wehrheim. “A {CSP} Approach to Control in Event-B.” In <i>Integrated Formal Methods - 8th International Conference, {IFM} 2010, Nancy, France, October 11-14, 2010. Proceedings</i>, edited by Dominique M{\\’{e}}ry and Stephan Merz, 260--274. Lecture Notes in Computer Science, 2010. <a href=\"https://doi.org/10.1007/978-3-642-16265-7_19\">https://doi.org/10.1007/978-3-642-16265-7_19</a>.","ieee":"S. Schneider, H. Treharne, and H. Wehrheim, “A {CSP} Approach to Control in Event-B,” in <i>Integrated Formal Methods - 8th International Conference, {IFM} 2010, Nancy, France, October 11-14, 2010. Proceedings</i>, 2010, pp. 260--274.","ama":"Schneider S, Treharne H, Wehrheim H. A {CSP} Approach to Control in Event-B. In: M{\\’{e}}ry D, Merz S, eds. <i>Integrated Formal Methods - 8th International Conference, {IFM} 2010, Nancy, France, October 11-14, 2010. Proceedings</i>. Lecture Notes in Computer Science. ; 2010:260--274. doi:<a href=\"https://doi.org/10.1007/978-3-642-16265-7_19\">10.1007/978-3-642-16265-7_19</a>"},"page":"260--274","title":"A {CSP} Approach to Control in Event-B","doi":"10.1007/978-3-642-16265-7_19","date_updated":"2022-01-06T06:59:04Z","author":[{"first_name":"Steve","last_name":"Schneider","full_name":"Schneider, Steve"},{"first_name":"Helen","full_name":"Treharne, Helen","last_name":"Treharne"},{"first_name":"Heike","full_name":"Wehrheim, Heike","id":"573","last_name":"Wehrheim"}],"date_created":"2018-06-13T09:20:53Z"},{"_id":"3196","user_id":"29719","series_title":"Lecture Notes in Computer Science","department":[{"_id":"77"}],"type":"conference","publication":"Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, {TACAS} 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings","editor":[{"first_name":"Javier","full_name":"Esparza, Javier","last_name":"Esparza"},{"first_name":"Rupak","full_name":"Majumdar, Rupak","last_name":"Majumdar"}],"status":"public","date_updated":"2022-01-06T06:59:04Z","date_created":"2018-06-13T09:22:07Z","author":[{"first_name":"Klaus","full_name":"Dräger, Klaus","last_name":"Dräger"},{"full_name":"Kupriyanov, Andrey","last_name":"Kupriyanov","first_name":"Andrey"},{"full_name":"Finkbeiner, Bernd","last_name":"Finkbeiner","first_name":"Bernd"},{"full_name":"Wehrheim, Heike","id":"573","last_name":"Wehrheim","first_name":"Heike"}],"title":"{SLAB:} {A} Certifying Model Checker for Infinite-State Concurrent Systems","doi":"10.1007/978-3-642-12002-2_22","year":"2010","citation":{"mla":"Dräger, Klaus, et al. “{SLAB:} {A} Certifying Model Checker for Infinite-State Concurrent Systems.” <i>Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, {TACAS} 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings</i>, edited by Javier Esparza and Rupak Majumdar, 2010, pp. 271--274, doi:<a href=\"https://doi.org/10.1007/978-3-642-12002-2_22\">10.1007/978-3-642-12002-2_22</a>.","bibtex":"@inproceedings{Dräger_Kupriyanov_Finkbeiner_Wehrheim_2010, series={Lecture Notes in Computer Science}, title={{SLAB:} {A} Certifying Model Checker for Infinite-State Concurrent Systems}, DOI={<a href=\"https://doi.org/10.1007/978-3-642-12002-2_22\">10.1007/978-3-642-12002-2_22</a>}, booktitle={Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, {TACAS} 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings}, author={Dräger, Klaus and Kupriyanov, Andrey and Finkbeiner, Bernd and Wehrheim, Heike}, editor={Esparza, Javier and Majumdar, RupakEditors}, year={2010}, pages={271--274}, collection={Lecture Notes in Computer Science} }","short":"K. Dräger, A. Kupriyanov, B. Finkbeiner, H. Wehrheim, in: J. Esparza, R. Majumdar (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, {TACAS} 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, 2010, pp. 271--274.","apa":"Dräger, K., Kupriyanov, A., Finkbeiner, B., &#38; Wehrheim, H. (2010). {SLAB:} {A} Certifying Model Checker for Infinite-State Concurrent Systems. In J. Esparza &#38; R. Majumdar (Eds.), <i>Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, {TACAS} 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings</i> (pp. 271--274). <a href=\"https://doi.org/10.1007/978-3-642-12002-2_22\">https://doi.org/10.1007/978-3-642-12002-2_22</a>","ieee":"K. Dräger, A. Kupriyanov, B. Finkbeiner, and H. Wehrheim, “{SLAB:} {A} Certifying Model Checker for Infinite-State Concurrent Systems,” in <i>Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, {TACAS} 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings</i>, 2010, pp. 271--274.","chicago":"Dräger, Klaus, Andrey Kupriyanov, Bernd Finkbeiner, and Heike Wehrheim. “{SLAB:} {A} Certifying Model Checker for Infinite-State Concurrent Systems.” In <i>Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, {TACAS} 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings</i>, edited by Javier Esparza and Rupak Majumdar, 271--274. Lecture Notes in Computer Science, 2010. <a href=\"https://doi.org/10.1007/978-3-642-12002-2_22\">https://doi.org/10.1007/978-3-642-12002-2_22</a>.","ama":"Dräger K, Kupriyanov A, Finkbeiner B, Wehrheim H. {SLAB:} {A} Certifying Model Checker for Infinite-State Concurrent Systems. In: Esparza J, Majumdar R, eds. <i>Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, {TACAS} 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings</i>. Lecture Notes in Computer Science. ; 2010:271--274. doi:<a href=\"https://doi.org/10.1007/978-3-642-12002-2_22\">10.1007/978-3-642-12002-2_22</a>"},"page":"271--274"},{"date_updated":"2022-01-06T06:59:04Z","_id":"3198","user_id":"29719","date_created":"2018-06-13T09:23:16Z","author":[{"first_name":"Dominik","last_name":"Steenken","full_name":"Steenken, Dominik"},{"last_name":"Wehrheim","full_name":"Wehrheim, Heike","id":"573","first_name":"Heike"},{"last_name":"Wonisch","full_name":"Wonisch, Daniel","first_name":"Daniel"}],"department":[{"_id":"77"}],"title":"Towards {A} Shape Analysis for Graph Transformation Systems","type":"journal_article","publication":"CoRR","year":"2010","citation":{"apa":"Steenken, D., Wehrheim, H., &#38; Wonisch, D. (2010). Towards {A} Shape Analysis for Graph Transformation Systems. <i>CoRR</i>.","short":"D. Steenken, H. Wehrheim, D. Wonisch, CoRR (2010).","mla":"Steenken, Dominik, et al. “Towards {A} Shape Analysis for Graph Transformation Systems.” <i>CoRR</i>, 2010.","bibtex":"@article{Steenken_Wehrheim_Wonisch_2010, title={Towards {A} Shape Analysis for Graph Transformation Systems}, journal={CoRR}, author={Steenken, Dominik and Wehrheim, Heike and Wonisch, Daniel}, year={2010} }","ama":"Steenken D, Wehrheim H, Wonisch D. Towards {A} Shape Analysis for Graph Transformation Systems. <i>CoRR</i>. 2010.","chicago":"Steenken, Dominik, Heike Wehrheim, and Daniel Wonisch. “Towards {A} Shape Analysis for Graph Transformation Systems.” <i>CoRR</i>, 2010.","ieee":"D. Steenken, H. Wehrheim, and D. Wonisch, “Towards {A} Shape Analysis for Graph Transformation Systems,” <i>CoRR</i>, 2010."},"status":"public"}]