[{"title":"Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework","doi":"10.1007/978-3-030-61362-4\\_8","publisher":"Springer","date_updated":"2022-01-06T06:54:25Z","volume":12476,"date_created":"2020-11-04T08:36:22Z","author":[{"first_name":"Dirk","last_name":"Beyer","full_name":"Beyer, Dirk"},{"last_name":"Wehrheim","full_name":"Wehrheim, Heike","id":"573","first_name":"Heike"}],"year":"2020","intvolume":"     12476","page":"143-167","citation":{"ieee":"D. Beyer and H. Wehrheim, “Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework,” in <i>Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {I}</i>, 2020, vol. 12476, pp. 143–167.","chicago":"Beyer, Dirk, and Heike Wehrheim. “Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework.” In <i>Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {I}</i>, edited by Tiziana Margaria and Bernhard Steffen, 12476:143–67. Lecture Notes in Computer Science. Springer, 2020. <a href=\"https://doi.org/10.1007/978-3-030-61362-4\\_8\">https://doi.org/10.1007/978-3-030-61362-4\\_8</a>.","ama":"Beyer D, Wehrheim H. Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework. In: Margaria T, Steffen B, eds. <i>Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {I}</i>. Vol 12476. Lecture Notes in Computer Science. Springer; 2020:143-167. doi:<a href=\"https://doi.org/10.1007/978-3-030-61362-4\\_8\">10.1007/978-3-030-61362-4\\_8</a>","apa":"Beyer, D., &#38; Wehrheim, H. (2020). Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework. In T. Margaria &#38; B. Steffen (Eds.), <i>Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {I}</i> (Vol. 12476, pp. 143–167). Springer. <a href=\"https://doi.org/10.1007/978-3-030-61362-4\\_8\">https://doi.org/10.1007/978-3-030-61362-4\\_8</a>","bibtex":"@inproceedings{Beyer_Wehrheim_2020, series={Lecture Notes in Computer Science}, title={Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework}, volume={12476}, DOI={<a href=\"https://doi.org/10.1007/978-3-030-61362-4\\_8\">10.1007/978-3-030-61362-4\\_8</a>}, booktitle={Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {I}}, publisher={Springer}, author={Beyer, Dirk and Wehrheim, Heike}, editor={Margaria, Tiziana and Steffen, BernhardEditors}, year={2020}, pages={143–167}, collection={Lecture Notes in Computer Science} }","short":"D. Beyer, H. Wehrheim, in: T. Margaria, B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {I}, Springer, 2020, pp. 143–167.","mla":"Beyer, Dirk, and Heike Wehrheim. “Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework.” <i>Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {I}</i>, edited by Tiziana Margaria and Bernhard Steffen, vol. 12476, Springer, 2020, pp. 143–67, doi:<a href=\"https://doi.org/10.1007/978-3-030-61362-4\\_8\">10.1007/978-3-030-61362-4\\_8</a>."},"language":[{"iso":"eng"}],"_id":"20276","project":[{"_id":"85","name":"Kooperative Softwareverifikation"}],"department":[{"_id":"77"}],"user_id":"29719","series_title":"Lecture Notes in Computer Science","editor":[{"first_name":"Tiziana","full_name":"Margaria, Tiziana","last_name":"Margaria"},{"full_name":"Steffen, Bernhard","last_name":"Steffen","first_name":"Bernhard"}],"status":"public","publication":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {I}","type":"conference"},{"year":"2020","citation":{"apa":"Haltermann, J. F., &#38; Wehrheim, H. (2020). Cooperative Verification via Collective Invariant Generation. <i>ArXiv:2008.04551</i>.","bibtex":"@article{Haltermann_Wehrheim_2020, title={Cooperative Verification via Collective Invariant Generation}, journal={arXiv:2008.04551}, author={Haltermann, Jan Frederik and Wehrheim, Heike}, year={2020} }","mla":"Haltermann, Jan Frederik, and Heike Wehrheim. “Cooperative Verification via Collective Invariant Generation.” <i>ArXiv:2008.04551</i>, 2020.","short":"J.F. Haltermann, H. Wehrheim, ArXiv:2008.04551 (2020).","ama":"Haltermann JF, Wehrheim H. Cooperative Verification via Collective Invariant Generation. <i>arXiv:200804551</i>. 2020.","ieee":"J. F. Haltermann and H. Wehrheim, “Cooperative Verification via Collective Invariant Generation,” <i>arXiv:2008.04551</i>. 2020.","chicago":"Haltermann, Jan Frederik, and Heike Wehrheim. “Cooperative Verification via Collective Invariant Generation.” <i>ArXiv:2008.04551</i>, 2020."},"title":"Cooperative Verification via Collective Invariant Generation","date_updated":"2022-01-06T06:53:20Z","author":[{"last_name":"Haltermann","id":"44413","full_name":"Haltermann, Jan Frederik","first_name":"Jan Frederik"},{"last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike","first_name":"Heike"}],"date_created":"2020-08-12T06:49:18Z","abstract":[{"text":"Software verification has recently made enormous progress due to the\r\ndevelopment of novel verification methods and the speed-up of supporting\r\ntechnologies like SMT solving. To keep software verification tools up to date\r\nwith these advances, tool developers keep on integrating newly designed methods\r\ninto their tools, almost exclusively by re-implementing the method within their\r\nown framework. While this allows for a conceptual re-use of methods, it\r\nrequires novel implementations for every new technique.\r\n  In this paper, we employ cooperative verification in order to avoid\r\nreimplementation and enable usage of novel tools as black-box components in\r\nverification. Specifically, cooperation is employed for the core ingredient of\r\nsoftware verification which is invariant generation. Finding an adequate loop\r\ninvariant is key to the success of a verification run. Our framework named\r\nCoVerCIG allows a master verification tool to delegate the task of invariant\r\ngeneration to one or several specialized helper invariant generators. Their\r\nresults are then utilized within the verification run of the master verifier,\r\nallowing in particular for crosschecking the validity of the invariant. We\r\nexperimentally evaluate our framework on an instance with two masters and three\r\ndifferent invariant generators using a number of benchmarks from SV-COMP 2020.\r\nThe experiments show that the use of CoVerCIG can increase the number of\r\ncorrectly verified tasks without increasing the used resources","lang":"eng"}],"status":"public","type":"preprint","publication":"arXiv:2008.04551","language":[{"iso":"eng"}],"project":[{"name":"Kooperative Softwareverifikation","_id":"85"}],"_id":"17825","user_id":"44413","department":[{"_id":"77"}]},{"project":[{"name":"Kooperative Softwareverifikation","_id":"85"}],"_id":"13872","user_id":"44413","department":[{"_id":"77"}],"language":[{"iso":"eng"}],"type":"book_chapter","publication":"Fundamental Approaches to Software Engineering","status":"public","date_updated":"2022-01-06T06:51:45Z","author":[{"full_name":"Beyer, Dirk","last_name":"Beyer","first_name":"Dirk"},{"first_name":"Marie-Christine","last_name":"Jakobs","full_name":"Jakobs, Marie-Christine"}],"date_created":"2019-10-16T06:39:51Z","title":"CoVeriTest: Cooperative Verifier-Based Testing","doi":"10.1007/978-3-030-16722-6_23","publication_status":"published","publication_identifier":{"issn":["0302-9743","1611-3349"],"isbn":["9783030167219","9783030167226"]},"place":"Cham","year":"2019","citation":{"ama":"Beyer D, Jakobs M-C. CoVeriTest: Cooperative Verifier-Based Testing. In: <i>Fundamental Approaches to Software Engineering</i>. Cham; 2019. doi:<a href=\"https://doi.org/10.1007/978-3-030-16722-6_23\">10.1007/978-3-030-16722-6_23</a>","ieee":"D. Beyer and M.-C. Jakobs, “CoVeriTest: Cooperative Verifier-Based Testing,” in <i>Fundamental Approaches to Software Engineering</i>, Cham, 2019.","chicago":"Beyer, Dirk, and Marie-Christine Jakobs. “CoVeriTest: Cooperative Verifier-Based Testing.” In <i>Fundamental Approaches to Software Engineering</i>. Cham, 2019. <a href=\"https://doi.org/10.1007/978-3-030-16722-6_23\">https://doi.org/10.1007/978-3-030-16722-6_23</a>.","apa":"Beyer, D., &#38; Jakobs, M.-C. (2019). CoVeriTest: Cooperative Verifier-Based Testing. In <i>Fundamental Approaches to Software Engineering</i>. Cham. <a href=\"https://doi.org/10.1007/978-3-030-16722-6_23\">https://doi.org/10.1007/978-3-030-16722-6_23</a>","mla":"Beyer, Dirk, and Marie-Christine Jakobs. “CoVeriTest: Cooperative Verifier-Based Testing.” <i>Fundamental Approaches to Software Engineering</i>, 2019, doi:<a href=\"https://doi.org/10.1007/978-3-030-16722-6_23\">10.1007/978-3-030-16722-6_23</a>.","bibtex":"@inbook{Beyer_Jakobs_2019, place={Cham}, title={CoVeriTest: Cooperative Verifier-Based Testing}, DOI={<a href=\"https://doi.org/10.1007/978-3-030-16722-6_23\">10.1007/978-3-030-16722-6_23</a>}, booktitle={Fundamental Approaches to Software Engineering}, author={Beyer, Dirk and Jakobs, Marie-Christine}, year={2019} }","short":"D. Beyer, M.-C. Jakobs, in: Fundamental Approaches to Software Engineering, Cham, 2019."}},{"title":"Reducer-Based Construction of Conditional Verifiers","date_created":"2018-01-08T10:52:51Z","publisher":"ACM","year":"2018","language":[{"iso":"eng"}],"ddc":["000"],"file":[{"file_size":826719,"file_name":"Reducer-Based Construction of Conditional Verifiers.pdf","access_level":"closed","file_id":"5783","date_updated":"2018-11-21T10:50:51Z","date_created":"2018-11-21T10:50:51Z","creator":"florida","success":1,"relation":"main_file","content_type":"application/pdf"}],"abstract":[{"lang":"eng","text":"to appear"}],"publication":"Proceedings of the 40th International Conference on Software Engineering (ICSE)","conference":{"end_date":"2018-06-03","location":"Gothenburg, Sweden","name":"40th International Conference on Software Engineering","start_date":"2018-05-27"},"author":[{"first_name":"Dirk","last_name":"Beyer","full_name":"Beyer, Dirk"},{"last_name":"Jakobs","full_name":"Jakobs, Marie-Christine","first_name":"Marie-Christine"},{"last_name":"Lemberger","full_name":"Lemberger, Thomas","first_name":"Thomas"},{"first_name":"Heike","full_name":"Wehrheim, Heike","id":"573","last_name":"Wehrheim"}],"date_updated":"2022-01-06T06:50:54Z","citation":{"ama":"Beyer D, Jakobs M-C, Lemberger T, Wehrheim H. Reducer-Based Construction of Conditional Verifiers. In: <i>Proceedings of the 40th International Conference on Software Engineering (ICSE)</i>. ACM; 2018:1182--1193.","ieee":"D. Beyer, M.-C. Jakobs, T. Lemberger, and H. Wehrheim, “Reducer-Based Construction of Conditional Verifiers,” in <i>Proceedings of the 40th International Conference on Software Engineering (ICSE)</i>, Gothenburg, Sweden, 2018, pp. 1182--1193.","chicago":"Beyer, Dirk, Marie-Christine Jakobs, Thomas Lemberger, and Heike Wehrheim. “Reducer-Based Construction of Conditional Verifiers.” In <i>Proceedings of the 40th International Conference on Software Engineering (ICSE)</i>, 1182--1193. ACM, 2018.","mla":"Beyer, Dirk, et al. “Reducer-Based Construction of Conditional Verifiers.” <i>Proceedings of the 40th International Conference on Software Engineering (ICSE)</i>, ACM, 2018, pp. 1182--1193.","short":"D. Beyer, M.-C. Jakobs, T. Lemberger, H. Wehrheim, in: Proceedings of the 40th International Conference on Software Engineering (ICSE), ACM, 2018, pp. 1182--1193.","bibtex":"@inproceedings{Beyer_Jakobs_Lemberger_Wehrheim_2018, title={Reducer-Based Construction of Conditional Verifiers}, booktitle={Proceedings of the 40th International Conference on Software Engineering (ICSE)}, publisher={ACM}, author={Beyer, Dirk and Jakobs, Marie-Christine and Lemberger, Thomas and Wehrheim, Heike}, year={2018}, pages={1182--1193} }","apa":"Beyer, D., Jakobs, M.-C., Lemberger, T., &#38; Wehrheim, H. (2018). Reducer-Based Construction of Conditional Verifiers. In <i>Proceedings of the 40th International Conference on Software Engineering (ICSE)</i> (pp. 1182--1193). Gothenburg, Sweden: ACM."},"page":"1182--1193","has_accepted_license":"1","file_date_updated":"2018-11-21T10:50:51Z","user_id":"29719","department":[{"_id":"77"}],"project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Project Area B","_id":"3"},{"name":"SFB 901 - Subproject B4","_id":"12"},{"_id":"85","name":"Kooperative Softwareverifikation"}],"_id":"1096","status":"public","type":"conference"}]