[{"user_id":"477","ddc":["000"],"status":"public","has_accepted_license":"1","date_created":"2018-06-13T07:47:56Z","file":[{"file_size":2136451,"file_id":"5315","creator":"ups","date_updated":"2018-11-02T15:52:13Z","content_type":"application/pdf","relation":"main_file","success":1,"file_name":"TemporalPlansForSoftwareArchit.pdf","date_created":"2018-11-02T15:52:13Z","access_level":"closed"}],"author":[{"last_name":"Ziegert","first_name":"Steffen","full_name":"Ziegert, Steffen"},{"full_name":"Wehrheim, Heike","first_name":"Heike","id":"573","last_name":"Wehrheim"}],"file_date_updated":"2018-11-02T15:52:13Z","publication":"Computer Science - R & D","issue":"3-4","_id":"3162","citation":{"ieee":"S. Ziegert and H. Wehrheim, “Temporal plans for software architecture reconfiguration,” Computer Science - R & D, no. 3–4, pp. 303--320, 2015.","short":"S. Ziegert, H. Wehrheim, Computer Science - R & D (2015) 303--320.","mla":"Ziegert, Steffen, and Heike Wehrheim. “Temporal Plans for Software Architecture Reconfiguration.” Computer Science - R & D, no. 3–4, 2015, pp. 303--320, doi:10.1007/s00450-014-0259-7.","bibtex":"@article{Ziegert_Wehrheim_2015, title={Temporal plans for software architecture reconfiguration}, DOI={10.1007/s00450-014-0259-7}, number={3–4}, journal={Computer Science - R & D}, author={Ziegert, Steffen and Wehrheim, Heike}, year={2015}, pages={303--320} }","chicago":"Ziegert, Steffen, and Heike Wehrheim. “Temporal Plans for Software Architecture Reconfiguration.” Computer Science - R & D, no. 3–4 (2015): 303--320. https://doi.org/10.1007/s00450-014-0259-7.","apa":"Ziegert, S., & Wehrheim, H. (2015). Temporal plans for software architecture reconfiguration. Computer Science - R & D, (3–4), 303--320. https://doi.org/10.1007/s00450-014-0259-7","ama":"Ziegert S, Wehrheim H. Temporal plans for software architecture reconfiguration. Computer Science - R & D. 2015;(3-4):303--320. doi:10.1007/s00450-014-0259-7"},"year":"2015","type":"journal_article","page":"303--320","title":"Temporal plans for software architecture reconfiguration","project":[{"name":"SFB 901 - Project Area B","_id":"3"},{"name":"SFB 901","_id":"1"},{"_id":"11","name":"SFB 901 - Subproject B3"}],"department":[{"_id":"77"}],"doi":"10.1007/s00450-014-0259-7","date_updated":"2022-01-06T06:59:01Z","language":[{"iso":"eng"}]},{"doi":"10.1007/978-3-319-23506-6_1","_id":"3163","date_updated":"2022-01-06T06:59:01Z","page":"3--4","type":"conference","citation":{"bibtex":"@inproceedings{Meyer_Wehrheim_2015, series={Lecture Notes in Computer Science}, title={From Program Verification to Time and Space: The Scientific Life of Ernst-R{\\\"{u}}diger Olderog}, DOI={10.1007/978-3-319-23506-6_1}, booktitle={Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings}, author={Meyer, Roland and Wehrheim, Heike}, editor={Meyer, Roland and Platzer, Andr{\\’{e}} and Wehrheim, HeikeEditors}, year={2015}, pages={3--4}, collection={Lecture Notes in Computer Science} }","mla":"Meyer, Roland, and Heike Wehrheim. “From Program Verification to Time and Space: The Scientific Life of Ernst-R{\\\"{u}}diger Olderog.” Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings, edited by Roland Meyer et al., 2015, pp. 3--4, doi:10.1007/978-3-319-23506-6_1.","ama":"Meyer R, Wehrheim H. From Program Verification to Time and Space: The Scientific Life of Ernst-R{\\\"{u}}diger Olderog. In: Meyer R, Platzer A, Wehrheim H, eds. Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings. Lecture Notes in Computer Science. ; 2015:3--4. doi:10.1007/978-3-319-23506-6_1","apa":"Meyer, R., & Wehrheim, H. (2015). From Program Verification to Time and Space: The Scientific Life of Ernst-R{\\\"{u}}diger Olderog. In R. Meyer, A. Platzer, & H. Wehrheim (Eds.), Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings (pp. 3--4). https://doi.org/10.1007/978-3-319-23506-6_1","chicago":"Meyer, Roland, and Heike Wehrheim. “From Program Verification to Time and Space: The Scientific Life of Ernst-R{\\\"{u}}diger Olderog.” In Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings, edited by Roland Meyer, Andr{\\’{e}} Platzer, and Heike Wehrheim, 3--4. Lecture Notes in Computer Science, 2015. https://doi.org/10.1007/978-3-319-23506-6_1.","ieee":"R. Meyer and H. Wehrheim, “From Program Verification to Time and Space: The Scientific Life of Ernst-R{\\\"{u}}diger Olderog,” in Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings, 2015, pp. 3--4.","short":"R. Meyer, H. Wehrheim, in: R. Meyer, A. Platzer, H. Wehrheim (Eds.), Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings, 2015, pp. 3--4."},"year":"2015","series_title":"Lecture Notes in Computer Science","title":"From Program Verification to Time and Space: The Scientific Life of Ernst-R{\\\"{u}}diger Olderog","user_id":"29719","editor":[{"last_name":"Meyer","first_name":"Roland","full_name":"Meyer, Roland"},{"last_name":"Platzer","full_name":"Platzer, Andr{\\'{e}}","first_name":"Andr{\\'{e}}"},{"full_name":"Wehrheim, Heike","first_name":"Heike","last_name":"Wehrheim"}],"date_created":"2018-06-13T07:49:28Z","status":"public","publication":"Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings","department":[{"_id":"77"}],"author":[{"first_name":"Roland","full_name":"Meyer, Roland","last_name":"Meyer"},{"full_name":"Wehrheim, Heike","first_name":"Heike","id":"573","last_name":"Wehrheim"}]},{"title":"Verifying Opacity of a Transactional Mutex Lock","user_id":"29719","publication":"{FM} 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings","department":[{"_id":"77"}],"author":[{"full_name":"Derrick, John","first_name":"John","last_name":"Derrick"},{"last_name":"Dongol","first_name":"Brijesh","full_name":"Dongol, Brijesh"},{"first_name":"Gerhard","full_name":"Schellhorn, Gerhard","last_name":"Schellhorn"},{"last_name":"Travkin","full_name":"Travkin, Oleg","first_name":"Oleg"},{"last_name":"Wehrheim","id":"573","first_name":"Heike","full_name":"Wehrheim, Heike"}],"editor":[{"full_name":"Bj{\\o}rner, Nikolaj","first_name":"Nikolaj","last_name":"Bj{\\o}rner"},{"first_name":"Frank","full_name":"S. de Boer, Frank","last_name":"S. de Boer"}],"project":[{"name":"Validation of Software Transactional Memory","_id":"78"}],"date_created":"2018-06-13T07:50:43Z","status":"public","_id":"3164","date_updated":"2022-01-06T06:59:01Z","doi":"10.1007/978-3-319-19249-9_11","series_title":"Lecture Notes in Computer Science","page":"161--177","year":"2015","citation":{"ieee":"J. Derrick, B. Dongol, G. Schellhorn, O. Travkin, and H. Wehrheim, “Verifying Opacity of a Transactional Mutex Lock,” in {FM} 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, 2015, pp. 161--177.","short":"J. Derrick, B. Dongol, G. Schellhorn, O. Travkin, H. Wehrheim, in: N. Bj{\\o}rner, F. S. de Boer (Eds.), {FM} 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, 2015, pp. 161--177.","bibtex":"@inproceedings{Derrick_Dongol_Schellhorn_Travkin_Wehrheim_2015, series={Lecture Notes in Computer Science}, title={Verifying Opacity of a Transactional Mutex Lock}, DOI={10.1007/978-3-319-19249-9_11}, booktitle={{FM} 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings}, author={Derrick, John and Dongol, Brijesh and Schellhorn, Gerhard and Travkin, Oleg and Wehrheim, Heike}, editor={Bj{\\o}rner, Nikolaj and S. de Boer, FrankEditors}, year={2015}, pages={161--177}, collection={Lecture Notes in Computer Science} }","mla":"Derrick, John, et al. “Verifying Opacity of a Transactional Mutex Lock.” {FM} 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, edited by Nikolaj Bj{\\o}rner and Frank S. de Boer, 2015, pp. 161--177, doi:10.1007/978-3-319-19249-9_11.","chicago":"Derrick, John, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, and Heike Wehrheim. “Verifying Opacity of a Transactional Mutex Lock.” In {FM} 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, edited by Nikolaj Bj{\\o}rner and Frank S. de Boer, 161--177. Lecture Notes in Computer Science, 2015. https://doi.org/10.1007/978-3-319-19249-9_11.","apa":"Derrick, J., Dongol, B., Schellhorn, G., Travkin, O., & Wehrheim, H. (2015). Verifying Opacity of a Transactional Mutex Lock. In N. Bj{\\o}rner & F. S. de Boer (Eds.), {FM} 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings (pp. 161--177). https://doi.org/10.1007/978-3-319-19249-9_11","ama":"Derrick J, Dongol B, Schellhorn G, Travkin O, Wehrheim H. Verifying Opacity of a Transactional Mutex Lock. In: Bj{\\o}rner N, S. de Boer F, eds. {FM} 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings. Lecture Notes in Computer Science. ; 2015:161--177. doi:10.1007/978-3-319-19249-9_11"},"type":"conference"},{"date_updated":"2022-01-06T06:59:01Z","_id":"3165","doi":"10.1007/978-3-319-26287-1_7","series_title":"Lecture Notes in Computer Science","citation":{"bibtex":"@inproceedings{Wehrheim_Travkin_2015, series={Lecture Notes in Computer Science}, title={{TSO} to {SC} via Symbolic Execution}, DOI={10.1007/978-3-319-26287-1_7}, booktitle={Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, {HVC} 2015, Haifa, Israel, November 17-19, 2015, Proceedings}, author={Wehrheim, Heike and Travkin, Oleg}, editor={Piterman, NirEditor}, year={2015}, pages={104--119}, collection={Lecture Notes in Computer Science} }","mla":"Wehrheim, Heike, and Oleg Travkin. “{TSO} to {SC} via Symbolic Execution.” Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, {HVC} 2015, Haifa, Israel, November 17-19, 2015, Proceedings, edited by Nir Piterman, 2015, pp. 104--119, doi:10.1007/978-3-319-26287-1_7.","chicago":"Wehrheim, Heike, and Oleg Travkin. “{TSO} to {SC} via Symbolic Execution.” In Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, {HVC} 2015, Haifa, Israel, November 17-19, 2015, Proceedings, edited by Nir Piterman, 104--119. Lecture Notes in Computer Science, 2015. https://doi.org/10.1007/978-3-319-26287-1_7.","apa":"Wehrheim, H., & Travkin, O. (2015). {TSO} to {SC} via Symbolic Execution. In N. Piterman (Ed.), Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, {HVC} 2015, Haifa, Israel, November 17-19, 2015, Proceedings (pp. 104--119). https://doi.org/10.1007/978-3-319-26287-1_7","ama":"Wehrheim H, Travkin O. {TSO} to {SC} via Symbolic Execution. In: Piterman N, ed. Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, {HVC} 2015, Haifa, Israel, November 17-19, 2015, Proceedings. Lecture Notes in Computer Science. ; 2015:104--119. doi:10.1007/978-3-319-26287-1_7","ieee":"H. Wehrheim and O. Travkin, “{TSO} to {SC} via Symbolic Execution,” in Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, {HVC} 2015, Haifa, Israel, November 17-19, 2015, Proceedings, 2015, pp. 104--119.","short":"H. Wehrheim, O. Travkin, in: N. Piterman (Ed.), Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, {HVC} 2015, Haifa, Israel, November 17-19, 2015, Proceedings, 2015, pp. 104--119."},"type":"conference","year":"2015","page":"104--119","user_id":"29719","title":"{TSO} to {SC} via Symbolic Execution","author":[{"last_name":"Wehrheim","id":"573","first_name":"Heike","full_name":"Wehrheim, Heike"},{"full_name":"Travkin, Oleg","first_name":"Oleg","last_name":"Travkin"}],"publication":"Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, {HVC} 2015, Haifa, Israel, November 17-19, 2015, Proceedings","department":[{"_id":"77"}],"status":"public","date_created":"2018-06-13T07:52:44Z","editor":[{"full_name":"Piterman, Nir","first_name":"Nir","last_name":"Piterman"}]},{"_id":"3166","date_updated":"2022-01-06T06:59:01Z","doi":"10.1007/978-3-319-23506-6","series_title":"Lecture Notes in Computer Science","citation":{"ieee":"R. Meyer, A. Platzer, and H. Wehrheim, Eds., Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings. 2015.","short":"R. Meyer, A. Platzer, H. Wehrheim, eds., Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings, 2015.","mla":"Meyer, Roland, et al., editors. Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings. 2015, doi:10.1007/978-3-319-23506-6.","bibtex":"@book{Meyer_Platzer_Wehrheim_2015, series={Lecture Notes in Computer Science}, title={Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings}, DOI={10.1007/978-3-319-23506-6}, year={2015}, collection={Lecture Notes in Computer Science} }","chicago":"Meyer, Roland, Andr{\\’{e}} Platzer, and Heike Wehrheim, eds. Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings. Lecture Notes in Computer Science, 2015. https://doi.org/10.1007/978-3-319-23506-6.","apa":"Meyer, R., Platzer, A., & Wehrheim, H. (Eds.). (2015). Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings. https://doi.org/10.1007/978-3-319-23506-6","ama":"Meyer R, Platzer A, Wehrheim H, eds. Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings.; 2015. doi:10.1007/978-3-319-23506-6"},"year":"2015","type":"conference_editor","user_id":"29719","title":"Correct System Design - Symposium in Honor of Ernst-R{\\\"{u}}diger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings","department":[{"_id":"77"}],"date_created":"2018-06-13T07:54:06Z","status":"public","publication_identifier":{"isbn":["978-3-319-23505-9"]},"editor":[{"first_name":"Roland","full_name":"Meyer, Roland","last_name":"Meyer"},{"first_name":"Andr{\\'{e}}","full_name":"Platzer, Andr{\\'{e}}","last_name":"Platzer"},{"full_name":"Wehrheim, Heike","first_name":"Heike","id":"573","last_name":"Wehrheim"}]},{"department":[{"_id":"77"}],"project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Subprojekt B3","_id":"11"},{"_id":"3","name":"SFB 901 - Project Area B"}],"editor":[{"last_name":"Lanese","full_name":"Lanese, Ivan","first_name":"Ivan"},{"full_name":"Madelaine, Eric","first_name":"Eric","last_name":"Madelaine"}],"title":"Verified Service Compositions by Template-Based Construction","series_title":"LNCS","language":[{"iso":"eng"}],"date_updated":"2022-01-06T06:59:13Z","doi":"10.1007/978-3-319-15317-9_3","file":[{"date_created":"2018-03-20T07:29:29Z","file_name":"336-facs2014_walther.pdf","access_level":"closed","file_size":484422,"file_id":"1423","creator":"florida","content_type":"application/pdf","date_updated":"2018-03-20T07:29:29Z","success":1,"relation":"main_file"}],"author":[{"last_name":"Walther","full_name":"Walther, Sven","first_name":"Sven"},{"first_name":"Heike","full_name":"Wehrheim, Heike","last_name":"Wehrheim","id":"573"}],"publication":"Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS)","file_date_updated":"2018-03-20T07:29:29Z","status":"public","has_accepted_license":"1","date_created":"2017-10-17T12:41:57Z","abstract":[{"lang":"eng","text":"Today, service compositions often need to be assembled or changed on-the-fly, which leaves only little time for quality assurance. Moreover, quality assurance is complicated by service providers only giving information on their services in terms of domain specific concepts with only limited semantic meaning. In this paper, we propose a method to construct service compositions based on pre-verifiedtemplates. Templates, given as workflow descriptions, are typed over a (domain-independent) template ontology defining concepts and predicates. Templates are proven correct using an abstract semantics, leaving the specific meaning of ontology concepts open, however, only up to given ontology rules. Construction of service compositions amounts to instantiation of templates with domain-specific services.Correctness of an instantiation can then simply be checked by verifying that the domain ontology(a) adheres to the rules of the template ontology, and (b) fulfills the constraints of the employed template."}],"user_id":"477","ddc":["040"],"year":"2014","type":"conference","citation":{"ieee":"S. Walther and H. Wehrheim, “Verified Service Compositions by Template-Based Construction,” in Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS), 2014, pp. 31–48.","short":"S. Walther, H. Wehrheim, in: I. Lanese, E. Madelaine (Eds.), Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS), 2014, pp. 31–48.","bibtex":"@inproceedings{Walther_Wehrheim_2014, series={LNCS}, title={Verified Service Compositions by Template-Based Construction}, DOI={10.1007/978-3-319-15317-9_3}, booktitle={Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS)}, author={Walther, Sven and Wehrheim, Heike}, editor={Lanese, Ivan and Madelaine, EricEditors}, year={2014}, pages={31–48}, collection={LNCS} }","mla":"Walther, Sven, and Heike Wehrheim. “Verified Service Compositions by Template-Based Construction.” Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS), edited by Ivan Lanese and Eric Madelaine, 2014, pp. 31–48, doi:10.1007/978-3-319-15317-9_3.","chicago":"Walther, Sven, and Heike Wehrheim. “Verified Service Compositions by Template-Based Construction.” In Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS), edited by Ivan Lanese and Eric Madelaine, 31–48. LNCS, 2014. https://doi.org/10.1007/978-3-319-15317-9_3.","apa":"Walther, S., & Wehrheim, H. (2014). Verified Service Compositions by Template-Based Construction. In I. Lanese & E. Madelaine (Eds.), Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS) (pp. 31–48). https://doi.org/10.1007/978-3-319-15317-9_3","ama":"Walther S, Wehrheim H. Verified Service Compositions by Template-Based Construction. In: Lanese I, Madelaine E, eds. Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS). LNCS. ; 2014:31-48. doi:10.1007/978-3-319-15317-9_3"},"page":"31-48","_id":"336"},{"type":"bachelorsthesis","citation":{"ieee":"P. Korth, Untersuchung transitiver Eigenschaften der Technik “Programs from Proofs.” Universität Paderborn, 2014.","short":"P. Korth, Untersuchung transitiver Eigenschaften der Technik “Programs from Proofs,” Universität Paderborn, 2014.","bibtex":"@book{Korth_2014, title={Untersuchung transitiver Eigenschaften der Technik “Programs from Proofs”}, publisher={Universität Paderborn}, author={Korth, Philipp}, year={2014} }","mla":"Korth, Philipp. Untersuchung transitiver Eigenschaften der Technik “Programs from Proofs.” Universität Paderborn, 2014.","ama":"Korth P. Untersuchung transitiver Eigenschaften der Technik “Programs from Proofs.” Universität Paderborn; 2014.","apa":"Korth, P. (2014). Untersuchung transitiver Eigenschaften der Technik “Programs from Proofs.” Universität Paderborn.","chicago":"Korth, Philipp. Untersuchung transitiver Eigenschaften der Technik “Programs from Proofs.” Universität Paderborn, 2014."},"year":"2014","language":[{"iso":"ger"}],"supervisor":[{"last_name":"Wehrheim","first_name":"Heike","full_name":"Wehrheim, Heike"}],"date_updated":"2022-01-06T06:59:14Z","_id":"340","department":[{"_id":"77"}],"author":[{"full_name":"Korth, Philipp","first_name":"Philipp","last_name":"Korth"}],"publisher":"Universität Paderborn","date_created":"2017-10-17T12:41:58Z","project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"name":"SFB 901 - Project Area B","_id":"3"}],"status":"public","title":"Untersuchung transitiver Eigenschaften der Technik \"Programs from Proofs\"","user_id":"15504"},{"department":[{"_id":"77"}],"publication":"Proceedings of the 40th Euromicro Conference on Software Engineering and Advanced Applications (Work in Progress Session)","file_date_updated":"2018-03-20T07:27:54Z","author":[{"first_name":"Matthias","full_name":"Becker, Matthias","last_name":"Becker"},{"last_name":"Becker","first_name":"Steffen","full_name":"Becker, Steffen"},{"first_name":"Galina","full_name":"Besova, Galina","last_name":"Besova"},{"last_name":"Walther","full_name":"Walther, Sven","first_name":"Sven"},{"id":"573","last_name":"Wehrheim","full_name":"Wehrheim, Heike","first_name":"Heike"}],"file":[{"content_type":"application/pdf","date_updated":"2018-03-20T07:27:54Z","relation":"main_file","success":1,"file_size":80674,"creator":"florida","file_id":"1420","access_level":"closed","date_created":"2018-03-20T07:27:54Z","file_name":"344-paper_CAMERA_READY.pdf"}],"project":[{"name":"SFB 901","_id":"1"},{"_id":"11","name":"SFB 901 - Subprojekt B3"},{"_id":"3","name":"SFB 901 - Project Area B"}],"date_created":"2017-10-17T12:41:59Z","has_accepted_license":"1","status":"public","title":"Towards Systematic Configuration for Architecture Validation","ddc":["040"],"user_id":"477","year":"2014","type":"conference","citation":{"ieee":"M. Becker, S. Becker, G. Besova, S. Walther, and H. Wehrheim, “Towards Systematic Configuration for Architecture Validation,” in Proceedings of the 40th Euromicro Conference on Software Engineering and Advanced Applications (Work in Progress Session), 2014.","short":"M. Becker, S. Becker, G. Besova, S. Walther, H. Wehrheim, in: Proceedings of the 40th Euromicro Conference on Software Engineering and Advanced Applications (Work in Progress Session), 2014.","mla":"Becker, Matthias, et al. “Towards Systematic Configuration for Architecture Validation.” Proceedings of the 40th Euromicro Conference on Software Engineering and Advanced Applications (Work in Progress Session), 2014.","bibtex":"@inproceedings{Becker_Becker_Besova_Walther_Wehrheim_2014, title={Towards Systematic Configuration for Architecture Validation}, booktitle={Proceedings of the 40th Euromicro Conference on Software Engineering and Advanced Applications (Work in Progress Session)}, author={Becker, Matthias and Becker, Steffen and Besova, Galina and Walther, Sven and Wehrheim, Heike}, year={2014} }","chicago":"Becker, Matthias, Steffen Becker, Galina Besova, Sven Walther, and Heike Wehrheim. “Towards Systematic Configuration for Architecture Validation.” In Proceedings of the 40th Euromicro Conference on Software Engineering and Advanced Applications (Work in Progress Session), 2014.","ama":"Becker M, Becker S, Besova G, Walther S, Wehrheim H. Towards Systematic Configuration for Architecture Validation. In: Proceedings of the 40th Euromicro Conference on Software Engineering and Advanced Applications (Work in Progress Session). ; 2014.","apa":"Becker, M., Becker, S., Besova, G., Walther, S., & Wehrheim, H. (2014). Towards Systematic Configuration for Architecture Validation. In Proceedings of the 40th Euromicro Conference on Software Engineering and Advanced Applications (Work in Progress Session)."},"language":[{"iso":"eng"}],"_id":"344","date_updated":"2022-01-06T06:59:17Z"},{"year":"2014","citation":{"short":"F. Mohr, S. Walther, in: Proceedings of the 14th International Conference on Software Reuse (ICSR), 2014, pp. 188–203.","ieee":"F. Mohr and S. Walther, “Template-based Generation of Semantic Services,” in Proceedings of the 14th International Conference on Software Reuse (ICSR), 2014, pp. 188–203.","apa":"Mohr, F., & Walther, S. (2014). Template-based Generation of Semantic Services. In Proceedings of the 14th International Conference on Software Reuse (ICSR) (pp. 188–203). https://doi.org/10.1007/978-3-319-14130-5_14","ama":"Mohr F, Walther S. Template-based Generation of Semantic Services. In: Proceedings of the 14th International Conference on Software Reuse (ICSR). LNCS. ; 2014:188-203. doi:10.1007/978-3-319-14130-5_14","chicago":"Mohr, Felix, and Sven Walther. “Template-Based Generation of Semantic Services.” In Proceedings of the 14th International Conference on Software Reuse (ICSR), 188–203. LNCS, 2014. https://doi.org/10.1007/978-3-319-14130-5_14.","bibtex":"@inproceedings{Mohr_Walther_2014, series={LNCS}, title={Template-based Generation of Semantic Services}, DOI={10.1007/978-3-319-14130-5_14}, booktitle={Proceedings of the 14th International Conference on Software Reuse (ICSR)}, author={Mohr, Felix and Walther, Sven}, year={2014}, pages={188–203}, collection={LNCS} }","mla":"Mohr, Felix, and Sven Walther. “Template-Based Generation of Semantic Services.” Proceedings of the 14th International Conference on Software Reuse (ICSR), 2014, pp. 188–203, doi:10.1007/978-3-319-14130-5_14."},"type":"conference","page":"188-203","_id":"353","file":[{"file_size":431778,"creator":"florida","file_id":"1414","date_updated":"2018-03-20T07:23:32Z","content_type":"application/pdf","success":1,"relation":"main_file","file_name":"353-icsr2015_submission_17.pdf","date_created":"2018-03-20T07:23:32Z","access_level":"closed"}],"author":[{"last_name":"Mohr","full_name":"Mohr, Felix","first_name":"Felix"},{"first_name":"Sven","full_name":"Walther, Sven","last_name":"Walther"}],"file_date_updated":"2018-03-20T07:23:32Z","publication":"Proceedings of the 14th International Conference on Software Reuse (ICSR)","status":"public","has_accepted_license":"1","date_created":"2017-10-17T12:42:00Z","abstract":[{"lang":"eng","text":"There are many technologies for the automation of processesthat deal with services; examples are service discovery and composition.Automation of these processes requires that the services are described semantically. However, semantically described services are currently not oronly rarely available, which limits the applicability of discovery and composition approaches. The systematic support for creating new semanticservices usable by automated technologies is an open problem.We tackle this problem with a template based approach: Domain independent templates are instantiated with domain specific services andboolean expressions. The obtained services have semantic descriptionswhose correctness directly follows from the correctness of the template.Besides the theory, we present experimental results for a service repository in which 85% of the services were generated automatically."}],"user_id":"477","ddc":["040"],"series_title":"LNCS","language":[{"iso":"eng"}],"date_updated":"2022-01-06T06:59:22Z","doi":"10.1007/978-3-319-14130-5_14","department":[{"_id":"77"},{"_id":"355"}],"project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Subprojekt B3","_id":"11"},{"_id":"3","name":"SFB 901 - Project Area B"},{"_id":"10","name":"SFB 901 - Subproject B2"}],"title":"Template-based Generation of Semantic Services"},{"series_title":"Lecture Notes in Informatics (LNI)","language":[{"iso":"eng"}],"date_updated":"2022-01-06T06:59:38Z","department":[{"_id":"77"}],"project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"title":"Programs from Proofs -- Approach and Applications","main_file_link":[{"url":"http://eprints.uni-kiel.de/23752/"}],"citation":{"apa":"Wonisch, D., Schremmer, A., & Wehrheim, H. (2014). Programs from Proofs -- Approach and Applications. In Proceedings of the Software Engineering Conference (SE) (pp. 67–68).","ama":"Wonisch D, Schremmer A, Wehrheim H. Programs from Proofs -- Approach and Applications. In: Proceedings of the Software Engineering Conference (SE). Lecture Notes in Informatics (LNI). ; 2014:67-68.","chicago":"Wonisch, Daniel, Alexander Schremmer, and Heike Wehrheim. “Programs from Proofs -- Approach and Applications.” In Proceedings of the Software Engineering Conference (SE), 67–68. Lecture Notes in Informatics (LNI), 2014.","mla":"Wonisch, Daniel, et al. “Programs from Proofs -- Approach and Applications.” Proceedings of the Software Engineering Conference (SE), 2014, pp. 67–68.","bibtex":"@inproceedings{Wonisch_Schremmer_Wehrheim_2014, series={Lecture Notes in Informatics (LNI)}, title={Programs from Proofs -- Approach and Applications}, booktitle={Proceedings of the Software Engineering Conference (SE)}, author={Wonisch, Daniel and Schremmer, Alexander and Wehrheim, Heike}, year={2014}, pages={67–68}, collection={Lecture Notes in Informatics (LNI)} }","short":"D. Wonisch, A. Schremmer, H. Wehrheim, in: Proceedings of the Software Engineering Conference (SE), 2014, pp. 67–68.","ieee":"D. Wonisch, A. Schremmer, and H. Wehrheim, “Programs from Proofs -- Approach and Applications,” in Proceedings of the Software Engineering Conference (SE), 2014, pp. 67–68."},"year":"2014","type":"conference","page":"67-68","_id":"383","author":[{"first_name":"Daniel","full_name":"Wonisch, Daniel","last_name":"Wonisch"},{"last_name":"Schremmer","first_name":"Alexander","full_name":"Schremmer, Alexander"},{"full_name":"Wehrheim, Heike","first_name":"Heike","id":"573","last_name":"Wehrheim"}],"publication":"Proceedings of the Software Engineering Conference (SE)","file_date_updated":"2018-03-20T07:04:52Z","file":[{"access_level":"closed","date_created":"2018-03-20T07:04:52Z","file_name":"383-programmsFromProofsSE.pdf","success":1,"relation":"main_file","date_updated":"2018-03-20T07:04:52Z","content_type":"application/pdf","creator":"florida","file_id":"1392","file_size":66474}],"has_accepted_license":"1","status":"public","date_created":"2017-10-17T12:42:06Z","abstract":[{"lang":"eng","text":"Proof-carrying code approaches aim at safe execution of untrusted code by having the code producer attach a safety proof to the code which the code consumer only has to validate. Depending on the type of safety property, proofs can however become quite large and their validation - though faster than their construction - still time consuming. In this paper we introduce a new concept for safe execution of untrusted code. It keeps the idea of putting the time consuming part of proving on the side of the code producer, however, attaches no proofs to code anymore but instead uses the proof to transform the program into an equivalent but more efficiently verifiable program. Code consumers thus still do proving themselves, however, on a computationally inexpensive level only. Experimental results show that the proof effort can be reduced by several orders of magnitude, both with respect to time and space."}],"ddc":["040"],"user_id":"477"},{"user_id":"29719","title":"The behavioural semantics of Event-B refinement","publication":"Formal Asp. Comput.","department":[{"_id":"77"}],"author":[{"full_name":"Schneider, Steve","first_name":"Steve","last_name":"Schneider"},{"first_name":"Helen","full_name":"Treharne, Helen","last_name":"Treharne"},{"full_name":"Wehrheim, Heike","first_name":"Heike","id":"573","last_name":"Wehrheim"}],"date_created":"2018-06-13T07:55:10Z","status":"public","date_updated":"2022-01-06T06:59:01Z","_id":"3167","issue":"2","doi":"10.1007/s00165-012-0265-0","page":"251--280","citation":{"ieee":"S. Schneider, H. Treharne, and H. Wehrheim, “The behavioural semantics of Event-B refinement,” Formal Asp. Comput., no. 2, pp. 251--280, 2014.","short":"S. Schneider, H. Treharne, H. Wehrheim, Formal Asp. Comput. (2014) 251--280.","mla":"Schneider, Steve, et al. “The Behavioural Semantics of Event-B Refinement.” Formal Asp. Comput., no. 2, 2014, pp. 251--280, doi:10.1007/s00165-012-0265-0.","bibtex":"@article{Schneider_Treharne_Wehrheim_2014, title={The behavioural semantics of Event-B refinement}, DOI={10.1007/s00165-012-0265-0}, number={2}, journal={Formal Asp. Comput.}, author={Schneider, Steve and Treharne, Helen and Wehrheim, Heike}, year={2014}, pages={251--280} }","apa":"Schneider, S., Treharne, H., & Wehrheim, H. (2014). The behavioural semantics of Event-B refinement. Formal Asp. Comput., (2), 251--280. https://doi.org/10.1007/s00165-012-0265-0","ama":"Schneider S, Treharne H, Wehrheim H. The behavioural semantics of Event-B refinement. Formal Asp Comput. 2014;(2):251--280. doi:10.1007/s00165-012-0265-0","chicago":"Schneider, Steve, Helen Treharne, and Heike Wehrheim. “The Behavioural Semantics of Event-B Refinement.” Formal Asp. Comput., no. 2 (2014): 251--280. https://doi.org/10.1007/s00165-012-0265-0."},"type":"journal_article","year":"2014"},{"publication":"Sci. Comput. Program.","department":[{"_id":"77"}],"author":[{"last_name":"Tofan","first_name":"Bogdan","full_name":"Tofan, Bogdan"},{"last_name":"Travkin","first_name":"Oleg","full_name":"Travkin, Oleg"},{"last_name":"Schellhorn","full_name":"Schellhorn, Gerhard","first_name":"Gerhard"},{"id":"573","last_name":"Wehrheim","full_name":"Wehrheim, Heike","first_name":"Heike"}],"date_created":"2018-06-13T07:56:12Z","status":"public","title":"Two approaches for proving linearizability of multiset","user_id":"29719","page":"297--314","citation":{"short":"B. Tofan, O. Travkin, G. Schellhorn, H. Wehrheim, Sci. Comput. Program. (2014) 297--314.","ieee":"B. Tofan, O. Travkin, G. Schellhorn, and H. Wehrheim, “Two approaches for proving linearizability of multiset,” Sci. Comput. Program., pp. 297--314, 2014.","chicago":"Tofan, Bogdan, Oleg Travkin, Gerhard Schellhorn, and Heike Wehrheim. “Two Approaches for Proving Linearizability of Multiset.” Sci. Comput. Program., 2014, 297--314. https://doi.org/10.1016/j.scico.2014.04.001.","ama":"Tofan B, Travkin O, Schellhorn G, Wehrheim H. Two approaches for proving linearizability of multiset. Sci Comput Program. 2014:297--314. doi:10.1016/j.scico.2014.04.001","apa":"Tofan, B., Travkin, O., Schellhorn, G., & Wehrheim, H. (2014). Two approaches for proving linearizability of multiset. Sci. Comput. Program., 297--314. https://doi.org/10.1016/j.scico.2014.04.001","mla":"Tofan, Bogdan, et al. “Two Approaches for Proving Linearizability of Multiset.” Sci. Comput. Program., 2014, pp. 297--314, doi:10.1016/j.scico.2014.04.001.","bibtex":"@article{Tofan_Travkin_Schellhorn_Wehrheim_2014, title={Two approaches for proving linearizability of multiset}, DOI={10.1016/j.scico.2014.04.001}, journal={Sci. Comput. Program.}, author={Tofan, Bogdan and Travkin, Oleg and Schellhorn, Gerhard and Wehrheim, Heike}, year={2014}, pages={297--314} }"},"year":"2014","type":"journal_article","_id":"3168","date_updated":"2022-01-06T06:59:01Z","doi":"10.1016/j.scico.2014.04.001"},{"status":"public","date_created":"2018-06-13T07:57:31Z","author":[{"full_name":"Schellhorn, Gerhard","first_name":"Gerhard","last_name":"Schellhorn"},{"first_name":"John","full_name":"Derrick, John","last_name":"Derrick"},{"first_name":"Heike","full_name":"Wehrheim, Heike","last_name":"Wehrheim","id":"573"}],"publication":"{ACM} Trans. Comput. Log.","department":[{"_id":"77"}],"user_id":"29719","title":"A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures","year":"2014","citation":{"short":"G. Schellhorn, J. Derrick, H. Wehrheim, {ACM} Trans. Comput. Log. (2014) 31:1--31:37.","ieee":"G. Schellhorn, J. Derrick, and H. Wehrheim, “A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures,” {ACM} Trans. Comput. Log., no. 4, pp. 31:1--31:37, 2014.","apa":"Schellhorn, G., Derrick, J., & Wehrheim, H. (2014). A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. {ACM} Trans. Comput. Log., (4), 31:1--31:37. https://doi.org/10.1145/2629496","ama":"Schellhorn G, Derrick J, Wehrheim H. A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. {ACM} Trans Comput Log. 2014;(4):31:1--31:37. doi:10.1145/2629496","chicago":"Schellhorn, Gerhard, John Derrick, and Heike Wehrheim. “A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures.” {ACM} Trans. Comput. Log., no. 4 (2014): 31:1--31:37. https://doi.org/10.1145/2629496.","bibtex":"@article{Schellhorn_Derrick_Wehrheim_2014, title={A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures}, DOI={10.1145/2629496}, number={4}, journal={{ACM} Trans. Comput. Log.}, author={Schellhorn, Gerhard and Derrick, John and Wehrheim, Heike}, year={2014}, pages={31:1--31:37} }","mla":"Schellhorn, Gerhard, et al. “A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures.” {ACM} Trans. Comput. Log., no. 4, 2014, pp. 31:1--31:37, doi:10.1145/2629496."},"type":"journal_article","page":"31:1--31:37","issue":"4","doi":"10.1145/2629496","date_updated":"2022-01-06T06:59:01Z","_id":"3169"},{"page":"200--214","type":"conference","citation":{"bibtex":"@inproceedings{Derrick_Dongol_Schellhorn_Tofan_Travkin_Wehrheim_2014, series={Lecture Notes in Computer Science}, title={Quiescent Consistency: Defining and Verifying Relaxed Linearizability}, DOI={10.1007/978-3-319-06410-9_15}, booktitle={{FM} 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings}, author={Derrick, John and Dongol, Brijesh and Schellhorn, Gerhard and Tofan, Bogdan and Travkin, Oleg and Wehrheim, Heike}, editor={B. Jones, Cliff and Pihlajasaari, Pekka and Sun, JunEditors}, year={2014}, pages={200--214}, collection={Lecture Notes in Computer Science} }","mla":"Derrick, John, et al. “Quiescent Consistency: Defining and Verifying Relaxed Linearizability.” {FM} 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, edited by Cliff B. Jones et al., 2014, pp. 200--214, doi:10.1007/978-3-319-06410-9_15.","ama":"Derrick J, Dongol B, Schellhorn G, Tofan B, Travkin O, Wehrheim H. Quiescent Consistency: Defining and Verifying Relaxed Linearizability. In: B. Jones C, Pihlajasaari P, Sun J, eds. {FM} 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings. Lecture Notes in Computer Science. ; 2014:200--214. doi:10.1007/978-3-319-06410-9_15","apa":"Derrick, J., Dongol, B., Schellhorn, G., Tofan, B., Travkin, O., & Wehrheim, H. (2014). Quiescent Consistency: Defining and Verifying Relaxed Linearizability. In C. B. Jones, P. Pihlajasaari, & J. Sun (Eds.), {FM} 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings (pp. 200--214). https://doi.org/10.1007/978-3-319-06410-9_15","chicago":"Derrick, John, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, and Heike Wehrheim. “Quiescent Consistency: Defining and Verifying Relaxed Linearizability.” In {FM} 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, edited by Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, 200--214. Lecture Notes in Computer Science, 2014. https://doi.org/10.1007/978-3-319-06410-9_15.","ieee":"J. Derrick, B. Dongol, G. Schellhorn, B. Tofan, O. Travkin, and H. Wehrheim, “Quiescent Consistency: Defining and Verifying Relaxed Linearizability,” in {FM} 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, 2014, pp. 200--214.","short":"J. Derrick, B. Dongol, G. Schellhorn, B. Tofan, O. Travkin, H. Wehrheim, in: C. B. Jones, P. Pihlajasaari, J. Sun (Eds.), {FM} 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, 2014, pp. 200--214."},"year":"2014","series_title":"Lecture Notes in Computer Science","doi":"10.1007/978-3-319-06410-9_15","date_updated":"2022-01-06T06:59:02Z","_id":"3170","date_created":"2018-06-13T07:58:40Z","status":"public","editor":[{"last_name":"B. Jones","full_name":"B. Jones, Cliff","first_name":"Cliff"},{"last_name":"Pihlajasaari","full_name":"Pihlajasaari, Pekka","first_name":"Pekka"},{"last_name":"Sun","first_name":"Jun","full_name":"Sun, Jun"}],"publication":"{FM} 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings","department":[{"_id":"77"}],"author":[{"last_name":"Derrick","first_name":"John","full_name":"Derrick, John"},{"last_name":"Dongol","full_name":"Dongol, Brijesh","first_name":"Brijesh"},{"last_name":"Schellhorn","full_name":"Schellhorn, Gerhard","first_name":"Gerhard"},{"last_name":"Tofan","first_name":"Bogdan","full_name":"Tofan, Bogdan"},{"full_name":"Travkin, Oleg","first_name":"Oleg","last_name":"Travkin"},{"id":"573","last_name":"Wehrheim","full_name":"Wehrheim, Heike","first_name":"Heike"}],"user_id":"29719","title":"Quiescent Consistency: Defining and Verifying Relaxed Linearizability"},{"department":[{"_id":"77"}],"publication":"Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, {HVC} 2014, Haifa, Israel, November 18-20, 2014. Proceedings","author":[{"last_name":"Travkin","full_name":"Travkin, Oleg","first_name":"Oleg"},{"first_name":"Heike","full_name":"Wehrheim, Heike","last_name":"Wehrheim","id":"573"}],"date_created":"2018-06-13T07:59:46Z","status":"public","editor":[{"first_name":"Eran","full_name":"Yahav, Eran","last_name":"Yahav"}],"user_id":"29719","title":"Handling {TSO} in Mechanized Linearizability Proofs","series_title":"Lecture Notes in Computer Science","page":"132--147","type":"conference","year":"2014","citation":{"chicago":"Travkin, Oleg, and Heike Wehrheim. “Handling {TSO} in Mechanized Linearizability Proofs.” In Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, {HVC} 2014, Haifa, Israel, November 18-20, 2014. Proceedings, edited by Eran Yahav, 132--147. Lecture Notes in Computer Science, 2014. https://doi.org/10.1007/978-3-319-13338-6_11.","apa":"Travkin, O., & Wehrheim, H. (2014). Handling {TSO} in Mechanized Linearizability Proofs. In E. Yahav (Ed.), Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, {HVC} 2014, Haifa, Israel, November 18-20, 2014. Proceedings (pp. 132--147). https://doi.org/10.1007/978-3-319-13338-6_11","ama":"Travkin O, Wehrheim H. Handling {TSO} in Mechanized Linearizability Proofs. In: Yahav E, ed. Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, {HVC} 2014, Haifa, Israel, November 18-20, 2014. Proceedings. Lecture Notes in Computer Science. ; 2014:132--147. doi:10.1007/978-3-319-13338-6_11","mla":"Travkin, Oleg, and Heike Wehrheim. “Handling {TSO} in Mechanized Linearizability Proofs.” Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, {HVC} 2014, Haifa, Israel, November 18-20, 2014. Proceedings, edited by Eran Yahav, 2014, pp. 132--147, doi:10.1007/978-3-319-13338-6_11.","bibtex":"@inproceedings{Travkin_Wehrheim_2014, series={Lecture Notes in Computer Science}, title={Handling {TSO} in Mechanized Linearizability Proofs}, DOI={10.1007/978-3-319-13338-6_11}, booktitle={Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, {HVC} 2014, Haifa, Israel, November 18-20, 2014. Proceedings}, author={Travkin, Oleg and Wehrheim, Heike}, editor={Yahav, EranEditor}, year={2014}, pages={132--147}, collection={Lecture Notes in Computer Science} }","short":"O. Travkin, H. Wehrheim, in: E. Yahav (Ed.), Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, {HVC} 2014, Haifa, Israel, November 18-20, 2014. Proceedings, 2014, pp. 132--147.","ieee":"O. Travkin and H. Wehrheim, “Handling {TSO} in Mechanized Linearizability Proofs,” in Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, {HVC} 2014, Haifa, Israel, November 18-20, 2014. Proceedings, 2014, pp. 132--147."},"_id":"3171","date_updated":"2022-01-06T06:59:02Z","doi":"10.1007/978-3-319-13338-6_11"},{"editor":[{"last_name":"Merz","first_name":"Stephan","full_name":"Merz, Stephan"},{"last_name":"Pang","first_name":"Jun","full_name":"Pang, Jun"}],"status":"public","date_created":"2018-06-13T08:01:04Z","author":[{"first_name":"Tobias","full_name":"Isenberg, Tobias","last_name":"Isenberg"},{"last_name":"Wehrheim","id":"573","first_name":"Heike","full_name":"Wehrheim, Heike"}],"department":[{"_id":"77"}],"publication":"Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, {ICFEM} 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings","title":"Timed Automata Verification via {IC3} with Zones","user_id":"29719","year":"2014","citation":{"ieee":"T. Isenberg and H. Wehrheim, “Timed Automata Verification via {IC3} with Zones,” in Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, {ICFEM} 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings, 2014, pp. 203--218.","short":"T. Isenberg, H. Wehrheim, in: S. Merz, J. Pang (Eds.), Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, {ICFEM} 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings, 2014, pp. 203--218.","bibtex":"@inproceedings{Isenberg_Wehrheim_2014, series={Lecture Notes in Computer Science}, title={Timed Automata Verification via {IC3} with Zones}, DOI={10.1007/978-3-319-11737-9_14}, booktitle={Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, {ICFEM} 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings}, author={Isenberg, Tobias and Wehrheim, Heike}, editor={Merz, Stephan and Pang, JunEditors}, year={2014}, pages={203--218}, collection={Lecture Notes in Computer Science} }","mla":"Isenberg, Tobias, and Heike Wehrheim. “Timed Automata Verification via {IC3} with Zones.” Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, {ICFEM} 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings, edited by Stephan Merz and Jun Pang, 2014, pp. 203--218, doi:10.1007/978-3-319-11737-9_14.","chicago":"Isenberg, Tobias, and Heike Wehrheim. “Timed Automata Verification via {IC3} with Zones.” In Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, {ICFEM} 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings, edited by Stephan Merz and Jun Pang, 203--218. Lecture Notes in Computer Science, 2014. https://doi.org/10.1007/978-3-319-11737-9_14.","apa":"Isenberg, T., & Wehrheim, H. (2014). Timed Automata Verification via {IC3} with Zones. In S. Merz & J. Pang (Eds.), Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, {ICFEM} 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings (pp. 203--218). https://doi.org/10.1007/978-3-319-11737-9_14","ama":"Isenberg T, Wehrheim H. Timed Automata Verification via {IC3} with Zones. In: Merz S, Pang J, eds. Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, {ICFEM} 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings. Lecture Notes in Computer Science. ; 2014:203--218. doi:10.1007/978-3-319-11737-9_14"},"type":"conference","page":"203--218","series_title":"Lecture Notes in Computer Science","doi":"10.1007/978-3-319-11737-9_14","date_updated":"2022-01-06T06:59:02Z","_id":"3172"},{"title":"Managing {LTL} Properties in Event-B Refinement","user_id":"29719","editor":[{"full_name":"Albert, Elvira","first_name":"Elvira","last_name":"Albert"},{"last_name":"Sekerinski","full_name":"Sekerinski, Emil","first_name":"Emil"}],"date_created":"2018-06-13T08:04:33Z","status":"public","publication":"Integrated Formal Methods - 11th International Conference, {IFM} 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings","department":[{"_id":"77"}],"author":[{"first_name":"Steve","full_name":"A. Schneider, Steve","last_name":"A. Schneider"},{"last_name":"Treharne","full_name":"Treharne, Helen","first_name":"Helen"},{"id":"573","last_name":"Wehrheim","full_name":"Wehrheim, Heike","first_name":"Heike"},{"first_name":"David","full_name":"M. Williams, David","last_name":"M. Williams"}],"doi":"10.1007/978-3-319-10181-1_14","date_updated":"2022-01-06T06:59:02Z","_id":"3173","page":"221--237","year":"2014","type":"conference","citation":{"bibtex":"@inproceedings{A. Schneider_Treharne_Wehrheim_M. Williams_2014, series={Lecture Notes in Computer Science}, title={Managing {LTL} Properties in Event-B Refinement}, DOI={10.1007/978-3-319-10181-1_14}, booktitle={Integrated Formal Methods - 11th International Conference, {IFM} 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings}, author={A. Schneider, Steve and Treharne, Helen and Wehrheim, Heike and M. Williams, David}, editor={Albert, Elvira and Sekerinski, EmilEditors}, year={2014}, pages={221--237}, collection={Lecture Notes in Computer Science} }","mla":"A. Schneider, Steve, et al. “Managing {LTL} Properties in Event-B Refinement.” Integrated Formal Methods - 11th International Conference, {IFM} 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings, edited by Elvira Albert and Emil Sekerinski, 2014, pp. 221--237, doi:10.1007/978-3-319-10181-1_14.","chicago":"A. Schneider, Steve, Helen Treharne, Heike Wehrheim, and David M. Williams. “Managing {LTL} Properties in Event-B Refinement.” In Integrated Formal Methods - 11th International Conference, {IFM} 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings, edited by Elvira Albert and Emil Sekerinski, 221--237. Lecture Notes in Computer Science, 2014. https://doi.org/10.1007/978-3-319-10181-1_14.","apa":"A. Schneider, S., Treharne, H., Wehrheim, H., & M. Williams, D. (2014). Managing {LTL} Properties in Event-B Refinement. In E. Albert & E. Sekerinski (Eds.), Integrated Formal Methods - 11th International Conference, {IFM} 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings (pp. 221--237). https://doi.org/10.1007/978-3-319-10181-1_14","ama":"A. Schneider S, Treharne H, Wehrheim H, M. Williams D. Managing {LTL} Properties in Event-B Refinement. In: Albert E, Sekerinski E, eds. Integrated Formal Methods - 11th International Conference, {IFM} 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings. Lecture Notes in Computer Science. ; 2014:221--237. doi:10.1007/978-3-319-10181-1_14","ieee":"S. A. Schneider, H. Treharne, H. Wehrheim, and D. M. Williams, “Managing {LTL} Properties in Event-B Refinement,” in Integrated Formal Methods - 11th International Conference, {IFM} 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings, 2014, pp. 221--237.","short":"S. A. Schneider, H. Treharne, H. Wehrheim, D. M. Williams, in: E. Albert, E. Sekerinski (Eds.), Integrated Formal Methods - 11th International Conference, {IFM} 2014, Bertinoro, Italy, September 9-11, 2014, Proceedings, 2014, pp. 221--237."},"series_title":"Lecture Notes in Computer Science"},{"status":"public","date_created":"2018-06-13T08:05:39Z","author":[{"first_name":"Steve","full_name":"Schneider, Steve","last_name":"Schneider"},{"last_name":"Treharne","first_name":"Helen","full_name":"Treharne, Helen"},{"first_name":"Heike","full_name":"Wehrheim, Heike","last_name":"Wehrheim","id":"573"},{"last_name":"M. Williams","first_name":"David","full_name":"M. Williams, David"}],"publication":"CoRR","department":[{"_id":"77"}],"user_id":"29719","title":"Managing {LTL} properties in Event-B refinement","type":"journal_article","citation":{"ama":"Schneider S, Treharne H, Wehrheim H, M. Williams D. Managing {LTL} properties in Event-B refinement. CoRR. 2014.","apa":"Schneider, S., Treharne, H., Wehrheim, H., & M. Williams, D. (2014). Managing {LTL} properties in Event-B refinement. CoRR.","chicago":"Schneider, Steve, Helen Treharne, Heike Wehrheim, and David M. Williams. “Managing {LTL} Properties in Event-B Refinement.” CoRR, 2014.","mla":"Schneider, Steve, et al. “Managing {LTL} Properties in Event-B Refinement.” CoRR, 2014.","bibtex":"@article{Schneider_Treharne_Wehrheim_M. Williams_2014, title={Managing {LTL} properties in Event-B refinement}, journal={CoRR}, author={Schneider, Steve and Treharne, Helen and Wehrheim, Heike and M. Williams, David}, year={2014} }","short":"S. Schneider, H. Treharne, H. Wehrheim, D. M. Williams, CoRR (2014).","ieee":"S. Schneider, H. Treharne, H. Wehrheim, and D. M. Williams, “Managing {LTL} properties in Event-B refinement,” CoRR, 2014."},"year":"2014","date_updated":"2022-01-06T06:59:02Z","_id":"3174"},{"date_updated":"2022-01-06T06:59:02Z","_id":"3175","citation":{"ieee":"T. Isenberg and H. Wehrheim, “Proof-Carrying Hardware via {IC3},” CoRR, 2014.","short":"T. Isenberg, H. Wehrheim, CoRR (2014).","mla":"Isenberg, Tobias, and Heike Wehrheim. “Proof-Carrying Hardware via {IC3}.” CoRR, 2014.","bibtex":"@article{Isenberg_Wehrheim_2014, title={Proof-Carrying Hardware via {IC3}}, journal={CoRR}, author={Isenberg, Tobias and Wehrheim, Heike}, year={2014} }","chicago":"Isenberg, Tobias, and Heike Wehrheim. “Proof-Carrying Hardware via {IC3}.” CoRR, 2014.","apa":"Isenberg, T., & Wehrheim, H. (2014). Proof-Carrying Hardware via {IC3}. CoRR.","ama":"Isenberg T, Wehrheim H. Proof-Carrying Hardware via {IC3}. CoRR. 2014."},"type":"journal_article","year":"2014","user_id":"29719","title":"Proof-Carrying Hardware via {IC3}","date_created":"2018-06-13T08:07:24Z","status":"public","department":[{"_id":"77"}],"publication":"CoRR","author":[{"full_name":"Isenberg, Tobias","first_name":"Tobias","last_name":"Isenberg"},{"full_name":"Wehrheim, Heike","first_name":"Heike","id":"573","last_name":"Wehrheim"}]},{"_id":"450","page":"30-39","year":"2014","type":"conference","citation":{"bibtex":"@inproceedings{Jakobs_Wehrheim_2014, series={SPIN 2014}, title={Certification for Configurable Program Analysis}, DOI={10.1145/2632362.2632372}, booktitle={Proceedings of the 21st International Symposium on Model Checking of Software (SPIN)}, author={Jakobs, Marie-Christine and Wehrheim, Heike}, year={2014}, pages={30–39}, collection={SPIN 2014} }","mla":"Jakobs, Marie-Christine, and Heike Wehrheim. “Certification for Configurable Program Analysis.” Proceedings of the 21st International Symposium on Model Checking of Software (SPIN), 2014, pp. 30–39, doi:10.1145/2632362.2632372.","apa":"Jakobs, M.-C., & Wehrheim, H. (2014). Certification for Configurable Program Analysis. In Proceedings of the 21st International Symposium on Model Checking of Software (SPIN) (pp. 30–39). https://doi.org/10.1145/2632362.2632372","ama":"Jakobs M-C, Wehrheim H. Certification for Configurable Program Analysis. In: Proceedings of the 21st International Symposium on Model Checking of Software (SPIN). SPIN 2014. ; 2014:30-39. doi:10.1145/2632362.2632372","chicago":"Jakobs, Marie-Christine, and Heike Wehrheim. “Certification for Configurable Program Analysis.” In Proceedings of the 21st International Symposium on Model Checking of Software (SPIN), 30–39. SPIN 2014, 2014. https://doi.org/10.1145/2632362.2632372.","ieee":"M.-C. Jakobs and H. Wehrheim, “Certification for Configurable Program Analysis,” in Proceedings of the 21st International Symposium on Model Checking of Software (SPIN), 2014, pp. 30–39.","short":"M.-C. Jakobs, H. Wehrheim, in: Proceedings of the 21st International Symposium on Model Checking of Software (SPIN), 2014, pp. 30–39."},"ddc":["040"],"user_id":"477","abstract":[{"lang":"eng","text":"Configurable program analysis (CPA) is a generic concept for the formalization of different software analysis techniques in a single framework. With the tool CPAchecker, this framework allows for an easy configuration and subsequent automatic execution of analysis procedures ranging from data-flow analysis to model checking. The focus of the tool CPAchecker is thus on analysis. In this paper, we study configurability from the point of view of software certification. Certification aims at providing (via a prior analysis) a certificate of correctness for a program which is (a) tamper-proof and (b) more efficient to check for validity than a full analysis. Here, we will show how, given an analysis instance of a CPA, to construct a corresponding sound certification instance, thereby arriving at configurable program certification. We report on experiments with certification based on different analysis techniques, and in particular explain which characteristics of an underlying analysis allow us to design an efficient (in the above (b) sense) certification procedure. "}],"date_created":"2017-10-17T12:42:19Z","status":"public","has_accepted_license":"1","publication":"Proceedings of the 21st International Symposium on Model Checking of Software (SPIN)","file_date_updated":"2018-03-16T11:25:35Z","author":[{"first_name":"Marie-Christine","full_name":"Jakobs, Marie-Christine","last_name":"Jakobs"},{"full_name":"Wehrheim, Heike","first_name":"Heike","id":"573","last_name":"Wehrheim"}],"file":[{"creator":"florida","file_id":"1345","file_size":487366,"relation":"main_file","success":1,"date_updated":"2018-03-16T11:25:35Z","content_type":"application/pdf","file_name":"450-p30-jakobs.pdf","date_created":"2018-03-16T11:25:35Z","access_level":"closed"}],"doi":"10.1145/2632362.2632372","date_updated":"2022-01-06T07:01:07Z","language":[{"iso":"eng"}],"series_title":"SPIN 2014","title":"Certification for Configurable Program Analysis","project":[{"_id":"1","name":"SFB 901"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"department":[{"_id":"77"}]}]