[{"language":[{"iso":"eng"}],"ddc":["000"],"publication":"Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019)","file":[{"file_size":504897,"file_name":"main.pdf","file_id":"7627","access_level":"closed","date_updated":"2019-02-12T07:18:17Z","creator":"pdschbrt","date_created":"2019-02-12T07:18:17Z","success":1,"relation":"main_file","content_type":"application/pdf"}],"date_created":"2019-02-12T07:20:07Z","title":"PhASAR: An Inter-Procedural Static Analysis Framework for C/C++","year":"2019","department":[{"_id":"76"}],"user_id":"60543","_id":"7626","project":[{"_id":"1","name":"SFB 901"},{"_id":"12","name":"SFB 901 - Subproject B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"file_date_updated":"2019-02-12T07:18:17Z","type":"conference","status":"public","volume":"II","author":[{"first_name":"Philipp","last_name":"Schubert","orcid":"0000-0002-8674-1859","full_name":"Schubert, Philipp","id":"60543"},{"full_name":"Hermann, Ben","id":"66173","orcid":"0000-0001-9848-2017","last_name":"Hermann","first_name":"Ben"},{"orcid":"0000-0003-3470-3647","last_name":"Bodden","id":"59256","full_name":"Bodden, Eric","first_name":"Eric"}],"date_updated":"2022-03-25T07:48:36Z","oa":"1","conference":{"end_date":"2019-04-11","location":"Prague, Czech Republic","name":"25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","start_date":"2019-04-08"},"doi":"10.1007/978-3-030-17465-1_22","main_file_link":[{"open_access":"1","url":"https://link.springer.com/chapter/10.1007/978-3-030-17465-1_22"}],"has_accepted_license":"1","publication_status":"published","page":"393-410","citation":{"mla":"Schubert, Philipp, et al. “PhASAR: An Inter-Procedural Static Analysis Framework for C/C++.” <i>Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019)</i>, vol. II, 2019, pp. 393–410, doi:<a href=\"https://doi.org/10.1007/978-3-030-17465-1_22\">10.1007/978-3-030-17465-1_22</a>.","short":"P. Schubert, B. Hermann, E. Bodden, in: Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019), 2019, pp. 393–410.","bibtex":"@inproceedings{Schubert_Hermann_Bodden_2019, title={PhASAR: An Inter-Procedural Static Analysis Framework for C/C++}, volume={II}, DOI={<a href=\"https://doi.org/10.1007/978-3-030-17465-1_22\">10.1007/978-3-030-17465-1_22</a>}, booktitle={Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019)}, author={Schubert, Philipp and Hermann, Ben and Bodden, Eric}, year={2019}, pages={393–410} }","apa":"Schubert, P., Hermann, B., &#38; Bodden, E. (2019). PhASAR: An Inter-Procedural Static Analysis Framework for C/C++. <i>Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019)</i>, <i>II</i>, 393–410. <a href=\"https://doi.org/10.1007/978-3-030-17465-1_22\">https://doi.org/10.1007/978-3-030-17465-1_22</a>","ama":"Schubert P, Hermann B, Bodden E. PhASAR: An Inter-Procedural Static Analysis Framework for C/C++. In: <i>Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019)</i>. Vol II. ; 2019:393-410. doi:<a href=\"https://doi.org/10.1007/978-3-030-17465-1_22\">10.1007/978-3-030-17465-1_22</a>","chicago":"Schubert, Philipp, Ben Hermann, and Eric Bodden. “PhASAR: An Inter-Procedural Static Analysis Framework for C/C++.” In <i>Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019)</i>, II:393–410, 2019. <a href=\"https://doi.org/10.1007/978-3-030-17465-1_22\">https://doi.org/10.1007/978-3-030-17465-1_22</a>.","ieee":"P. Schubert, B. Hermann, and E. Bodden, “PhASAR: An Inter-Procedural Static Analysis Framework for C/C++,” in <i>Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019)</i>, Prague, Czech Republic, 2019, vol. II, pp. 393–410, doi: <a href=\"https://doi.org/10.1007/978-3-030-17465-1_22\">10.1007/978-3-030-17465-1_22</a>."}},{"file_date_updated":"2019-08-20T08:47:20Z","_id":"10108","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Project Area B","_id":"3"},{"_id":"12","name":"SFB 901 - Subproject B4"}],"department":[{"_id":"77"}],"user_id":"22398","status":"public","type":"conference","doi":"10.1145/3338906.3338915","date_updated":"2023-01-18T08:32:47Z","author":[{"first_name":"Felix","last_name":"Pauck","id":"22398","full_name":"Pauck, Felix"},{"id":"573","full_name":"Wehrheim, Heike","last_name":"Wehrheim","first_name":"Heike"}],"page":"374-384","citation":{"mla":"Pauck, Felix, and Heike Wehrheim. “Together Strong: Cooperative Android App Analysis.” <i>Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering</i>, 2019, pp. 374–84, doi:<a href=\"https://doi.org/10.1145/3338906.3338915\">10.1145/3338906.3338915</a>.","bibtex":"@inproceedings{Pauck_Wehrheim_2019, title={Together Strong: Cooperative Android App Analysis}, DOI={<a href=\"https://doi.org/10.1145/3338906.3338915\">10.1145/3338906.3338915</a>}, booktitle={Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering}, author={Pauck, Felix and Wehrheim, Heike}, year={2019}, pages={374–384} }","short":"F. Pauck, H. Wehrheim, in: Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2019, pp. 374–384.","apa":"Pauck, F., &#38; Wehrheim, H. (2019). Together Strong: Cooperative Android App Analysis. <i>Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering</i>, 374–384. <a href=\"https://doi.org/10.1145/3338906.3338915\">https://doi.org/10.1145/3338906.3338915</a>","ama":"Pauck F, Wehrheim H. Together Strong: Cooperative Android App Analysis. In: <i>Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering</i>. ; 2019:374-384. doi:<a href=\"https://doi.org/10.1145/3338906.3338915\">10.1145/3338906.3338915</a>","chicago":"Pauck, Felix, and Heike Wehrheim. “Together Strong: Cooperative Android App Analysis.” In <i>Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering</i>, 374–84, 2019. <a href=\"https://doi.org/10.1145/3338906.3338915\">https://doi.org/10.1145/3338906.3338915</a>.","ieee":"F. Pauck and H. Wehrheim, “Together Strong: Cooperative Android App Analysis,” in <i>Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering</i>, 2019, pp. 374–384, doi: <a href=\"https://doi.org/10.1145/3338906.3338915\">10.1145/3338906.3338915</a>."},"publication_identifier":{"isbn":["978-1-4503-5572-8"]},"has_accepted_license":"1","publication_status":"published","keyword":["Android Taint Analysis","Cooperation","Precision","Tools"],"ddc":["004"],"language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"Recent years have seen the development of numerous tools for the analysis of taint flows in Android apps. Taint analyses aim at detecting data leaks, accidentally or by purpose programmed into apps. Often, such tools specialize in the treatment of specific features impeding precise taint analysis (like reflection or inter-app communication). This multitude of tools, their specific applicability and their various combination options complicate the selection of a tool (or multiple tools) when faced with an analysis instance, even for knowledgeable users, and hence hinders the successful adoption of taint analyses.\r\n\r\nIn this work, we thus present CoDiDroid, a framework for cooperative Android app analysis. CoDiDroid (1) allows users to ask questions about flows in apps in varying degrees of detail, (2) automatically generates subtasks for answering such questions, (3) distributes tasks onto analysis tools (currently DroidRA, FlowDroid, HornDroid, IC3 and two novel tools) and (4) at the end merges tool answers on subtasks into an overall answer. Thereby, users are freed from having to learn about the use and functionality of all these tools while still being able to leverage their capabilities. Moreover, we experimentally show that cooperation among tools pays off with respect to effectiveness, precision and scalability."}],"file":[{"date_created":"2019-08-20T08:47:20Z","creator":"fpauck","date_updated":"2019-08-20T08:47:20Z","file_name":"fse19main-id44-p-ef9ce42-41855-final.pdf","access_level":"closed","file_id":"12947","file_size":442603,"content_type":"application/pdf","relation":"main_file"}],"publication":"Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering","title":"Together Strong: Cooperative Android App Analysis","date_created":"2019-06-04T11:15:25Z","year":"2019"},{"language":[{"iso":"eng"}],"department":[{"_id":"77"}],"user_id":"22398","_id":"13874","project":[{"_id":"12","name":"SFB 901 - Subproject B4"},{"_id":"3","name":"SFB 901 - Project Area B"},{"name":"SFB 901","_id":"1"}],"status":"public","publication":"Tests and Proofs - 13th International Conference, {TAP} 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings","type":"conference","doi":"10.1007/978-3-030-31157-5_1","title":"When Are Software Verification Results Valid for Approximate Hardware?","author":[{"first_name":"Tobias","last_name":"Isenberg","full_name":"Isenberg, Tobias"},{"first_name":"Marie-Christine","last_name":"Jakobs","full_name":"Jakobs, Marie-Christine"},{"id":"22398","full_name":"Pauck, Felix","last_name":"Pauck","first_name":"Felix"},{"last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike","first_name":"Heike"}],"date_created":"2019-10-16T09:40:20Z","date_updated":"2023-01-18T08:41:17Z","page":"3-20","citation":{"bibtex":"@inproceedings{Isenberg_Jakobs_Pauck_Wehrheim_2019, title={When Are Software Verification Results Valid for Approximate Hardware?}, DOI={<a href=\"https://doi.org/10.1007/978-3-030-31157-5_1\">10.1007/978-3-030-31157-5_1</a>}, booktitle={Tests and Proofs - 13th International Conference, {TAP} 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings}, author={Isenberg, Tobias and Jakobs, Marie-Christine and Pauck, Felix and Wehrheim, Heike}, year={2019}, pages={3–20} }","mla":"Isenberg, Tobias, et al. “When Are Software Verification Results Valid for Approximate Hardware?” <i>Tests and Proofs - 13th International Conference, {TAP} 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings</i>, 2019, pp. 3–20, doi:<a href=\"https://doi.org/10.1007/978-3-030-31157-5_1\">10.1007/978-3-030-31157-5_1</a>.","short":"T. Isenberg, M.-C. Jakobs, F. Pauck, H. Wehrheim, in: Tests and Proofs - 13th International Conference, {TAP} 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings, 2019, pp. 3–20.","apa":"Isenberg, T., Jakobs, M.-C., Pauck, F., &#38; Wehrheim, H. (2019). When Are Software Verification Results Valid for Approximate Hardware? <i>Tests and Proofs - 13th International Conference, {TAP} 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings</i>, 3–20. <a href=\"https://doi.org/10.1007/978-3-030-31157-5_1\">https://doi.org/10.1007/978-3-030-31157-5_1</a>","ieee":"T. Isenberg, M.-C. Jakobs, F. Pauck, and H. Wehrheim, “When Are Software Verification Results Valid for Approximate Hardware?,” in <i>Tests and Proofs - 13th International Conference, {TAP} 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings</i>, 2019, pp. 3–20, doi: <a href=\"https://doi.org/10.1007/978-3-030-31157-5_1\">10.1007/978-3-030-31157-5_1</a>.","chicago":"Isenberg, Tobias, Marie-Christine Jakobs, Felix Pauck, and Heike Wehrheim. “When Are Software Verification Results Valid for Approximate Hardware?” In <i>Tests and Proofs - 13th International Conference, {TAP} 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings</i>, 3–20, 2019. <a href=\"https://doi.org/10.1007/978-3-030-31157-5_1\">https://doi.org/10.1007/978-3-030-31157-5_1</a>.","ama":"Isenberg T, Jakobs M-C, Pauck F, Wehrheim H. When Are Software Verification Results Valid for Approximate Hardware? In: <i>Tests and Proofs - 13th International Conference, {TAP} 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings</i>. ; 2019:3-20. doi:<a href=\"https://doi.org/10.1007/978-3-030-31157-5_1\">10.1007/978-3-030-31157-5_1</a>"},"year":"2019","publication_status":"published"},{"main_file_link":[{"open_access":"1"}],"doi":"10.1007/978-3-030-17227-5_10","conference":{"start_date":"2019-04-09","name":"15th International Symposium on Applied Reconfigurable Computing (ARC 2019)","location":"Darmstadt, Germany","end_date":"2019-04-11"},"date_updated":"2023-05-15T08:13:37Z","oa":"1","author":[{"first_name":"Qazi Arbab","full_name":"Ahmed, Qazi Arbab","id":"72764","last_name":"Ahmed","orcid":"0000-0002-1837-2254"},{"first_name":"Tobias","last_name":"Wiersema","full_name":"Wiersema, Tobias","id":"3118"},{"first_name":"Marco","last_name":"Platzner","full_name":"Platzner, Marco","id":"398"}],"volume":11444,"place":"Cham","citation":{"ama":"Ahmed QA, Wiersema T, Platzner M. Proof-Carrying Hardware Versus the Stealthy Malicious LUT Hardware Trojan. In: Hochberger C, Nelson B, Koch A, Woods R, Diniz P, eds. <i>Applied Reconfigurable Computing</i>. Vol 11444. Lecture Notes in Computer Science. Springer International Publishing; 2019:127-136. doi:<a href=\"https://doi.org/10.1007/978-3-030-17227-5_10\">10.1007/978-3-030-17227-5_10</a>","chicago":"Ahmed, Qazi Arbab, Tobias Wiersema, and Marco Platzner. “Proof-Carrying Hardware Versus the Stealthy Malicious LUT Hardware Trojan.” In <i>Applied Reconfigurable Computing</i>, edited by Christian Hochberger, Brent Nelson, Andreas Koch, Roger Woods, and Pedro Diniz, 11444:127–36. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2019. <a href=\"https://doi.org/10.1007/978-3-030-17227-5_10\">https://doi.org/10.1007/978-3-030-17227-5_10</a>.","ieee":"Q. A. Ahmed, T. Wiersema, and M. Platzner, “Proof-Carrying Hardware Versus the Stealthy Malicious LUT Hardware Trojan,” in <i>Applied Reconfigurable Computing</i>, Darmstadt, Germany, 2019, vol. 11444, pp. 127–136, doi: <a href=\"https://doi.org/10.1007/978-3-030-17227-5_10\">10.1007/978-3-030-17227-5_10</a>.","apa":"Ahmed, Q. A., Wiersema, T., &#38; Platzner, M. (2019). Proof-Carrying Hardware Versus the Stealthy Malicious LUT Hardware Trojan. In C. Hochberger, B. Nelson, A. Koch, R. Woods, &#38; P. Diniz (Eds.), <i>Applied Reconfigurable Computing</i> (Vol. 11444, pp. 127–136). Springer International Publishing. <a href=\"https://doi.org/10.1007/978-3-030-17227-5_10\">https://doi.org/10.1007/978-3-030-17227-5_10</a>","bibtex":"@inproceedings{Ahmed_Wiersema_Platzner_2019, place={Cham}, series={Lecture Notes in Computer Science}, title={Proof-Carrying Hardware Versus the Stealthy Malicious LUT Hardware Trojan}, volume={11444}, DOI={<a href=\"https://doi.org/10.1007/978-3-030-17227-5_10\">10.1007/978-3-030-17227-5_10</a>}, booktitle={Applied Reconfigurable Computing}, publisher={Springer International Publishing}, author={Ahmed, Qazi Arbab and Wiersema, Tobias and Platzner, Marco}, editor={Hochberger, Christian and Nelson, Brent and Koch, Andreas and Woods, Roger and Diniz, Pedro}, year={2019}, pages={127–136}, collection={Lecture Notes in Computer Science} }","short":"Q.A. Ahmed, T. Wiersema, M. Platzner, in: C. Hochberger, B. Nelson, A. Koch, R. Woods, P. Diniz (Eds.), Applied Reconfigurable Computing, Springer International Publishing, Cham, 2019, pp. 127–136.","mla":"Ahmed, Qazi Arbab, et al. “Proof-Carrying Hardware Versus the Stealthy Malicious LUT Hardware Trojan.” <i>Applied Reconfigurable Computing</i>, edited by Christian Hochberger et al., vol. 11444, Springer International Publishing, 2019, pp. 127–36, doi:<a href=\"https://doi.org/10.1007/978-3-030-17227-5_10\">10.1007/978-3-030-17227-5_10</a>."},"page":"127-136","intvolume":"     11444","publication_status":"published","has_accepted_license":"1","publication_identifier":{"isbn":["978-3-030-17227-5"]},"file_date_updated":"2023-05-11T09:12:33Z","project":[{"name":"SFB 901 - Subproject B4","_id":"12"},{"name":"SFB 901","_id":"1"},{"_id":"3","name":"SFB 901 - Project Area B"}],"_id":"9913","series_title":"Lecture Notes in Computer Science","user_id":"72764","department":[{"_id":"78"}],"editor":[{"last_name":"Hochberger","full_name":"Hochberger, Christian","first_name":"Christian"},{"full_name":"Nelson, Brent","last_name":"Nelson","first_name":"Brent"},{"first_name":"Andreas","last_name":"Koch","full_name":"Koch, Andreas"},{"last_name":"Woods","full_name":"Woods, Roger","first_name":"Roger"},{"first_name":"Pedro","last_name":"Diniz","full_name":"Diniz, Pedro"}],"status":"public","type":"conference","title":"Proof-Carrying Hardware Versus the Stealthy Malicious LUT Hardware Trojan","publisher":"Springer International Publishing","date_created":"2019-05-22T07:36:05Z","year":"2019","ddc":["000"],"language":[{"iso":"eng"}],"abstract":[{"text":"Reconfigurable hardware has received considerable attention as a platform that enables dynamic hardware updates and thus is able to adapt new configurations at runtime. However, due to their dynamic nature, e.g., field-programmable gate arrays (FPGA) are subject to a constant possibility of attacks, since each new configuration might be compromised. Trojans for reconfigurable hardware that evade state-of-the-art detection techniques and even formal verification, are thus a large threat to these devices. One such stealthy hardware Trojan, that is inserted and activated in two stages by compromised electronic design automation (EDA) tools, has recently been presented and shown to evade all forms of classical pre-configuration detection techniques. This paper presents a successful pre-configuration countermeasure against this ``Malicious Look-up-table (LUT)''-hardware Trojan, by employing bitstream-level Proof-Carrying Hardware (PCH). We show that the method is able to alert innocent module creators to infected EDA tools, and to prohibit malicious ones to sell infected modules to unsuspecting customers.","lang":"eng"}],"file":[{"file_id":"44749","file_name":"978-3-030-17227-5_10.pdf","access_level":"closed","file_size":661354,"date_created":"2023-05-11T09:12:33Z","creator":"qazi","date_updated":"2023-05-11T09:12:33Z","relation":"main_file","success":1,"content_type":"application/pdf"}],"publication":"Applied Reconfigurable Computing"},{"date_created":"2019-11-12T12:22:16Z","author":[{"first_name":"Philipp","id":"60543","full_name":"Schubert, Philipp","last_name":"Schubert","orcid":"0000-0002-8674-1859"},{"full_name":"Leer, Richard","last_name":"Leer","first_name":"Richard"},{"first_name":"Ben","last_name":"Hermann","orcid":"0000-0001-9848-2017","id":"66173","full_name":"Hermann, Ben"},{"first_name":"Eric","orcid":"0000-0003-3470-3647","last_name":"Bodden","id":"59256","full_name":"Bodden, Eric"}],"date_updated":"2023-06-15T08:52:37Z","doi":"10.1145/3315568.3329965","title":"Know your analysis: how instrumentation aids understanding static analysis","publication_identifier":{"isbn":["9781450367202"]},"publication_status":"published","citation":{"ama":"Schubert P, Leer R, Hermann B, Bodden E. Know your analysis: how instrumentation aids understanding static analysis. In: <i>Proceedings of the 8th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis  - SOAP 2019</i>. ; 2019. doi:<a href=\"https://doi.org/10.1145/3315568.3329965\">10.1145/3315568.3329965</a>","apa":"Schubert, P., Leer, R., Hermann, B., &#38; Bodden, E. (2019). Know your analysis: how instrumentation aids understanding static analysis. <i>Proceedings of the 8th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis  - SOAP 2019</i>. <a href=\"https://doi.org/10.1145/3315568.3329965\">https://doi.org/10.1145/3315568.3329965</a>","mla":"Schubert, Philipp, et al. “Know Your Analysis: How Instrumentation Aids Understanding Static Analysis.” <i>Proceedings of the 8th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis  - SOAP 2019</i>, 2019, doi:<a href=\"https://doi.org/10.1145/3315568.3329965\">10.1145/3315568.3329965</a>.","short":"P. Schubert, R. Leer, B. Hermann, E. Bodden, in: Proceedings of the 8th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis  - SOAP 2019, 2019.","bibtex":"@inproceedings{Schubert_Leer_Hermann_Bodden_2019, title={Know your analysis: how instrumentation aids understanding static analysis}, DOI={<a href=\"https://doi.org/10.1145/3315568.3329965\">10.1145/3315568.3329965</a>}, booktitle={Proceedings of the 8th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis  - SOAP 2019}, author={Schubert, Philipp and Leer, Richard and Hermann, Ben and Bodden, Eric}, year={2019} }","chicago":"Schubert, Philipp, Richard Leer, Ben Hermann, and Eric Bodden. “Know Your Analysis: How Instrumentation Aids Understanding Static Analysis.” In <i>Proceedings of the 8th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis  - SOAP 2019</i>, 2019. <a href=\"https://doi.org/10.1145/3315568.3329965\">https://doi.org/10.1145/3315568.3329965</a>.","ieee":"P. Schubert, R. Leer, B. Hermann, and E. Bodden, “Know your analysis: how instrumentation aids understanding static analysis,” 2019, doi: <a href=\"https://doi.org/10.1145/3315568.3329965\">10.1145/3315568.3329965</a>."},"year":"2019","department":[{"_id":"76"},{"_id":"34"},{"_id":"26"}],"user_id":"15249","_id":"14898","project":[{"_id":"12","name":"SFB 901 - B4: SFB 901 - Subproject B4"},{"name":"SFB 901 - B: SFB 901 - Project Area B","_id":"3"},{"grant_number":"160364472","_id":"1","name":"SFB 901: SFB 901: On-The-Fly Computing - Individualisierte IT-Dienstleistungen in dynamischen Märkten "}],"language":[{"iso":"eng"}],"publication":"Proceedings of the 8th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis  - SOAP 2019","type":"conference","status":"public"},{"has_accepted_license":"1","publication_identifier":{"isbn":["9783319788890","9783319788906"],"issn":["0302-9743","1611-3349"]},"publication_status":"published","page":"153-165","intvolume":"     10824","citation":{"ama":"Hansmeier T, Platzner M, Andrews D. An FPGA/HMC-Based Accelerator for Resolution Proof Checking. In: <i>ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications</i>. Vol 10824. Lecture Notes in Computer Science. Springer International Publishing; 2018:153-165. doi:<a href=\"https://doi.org/10.1007/978-3-319-78890-6_13\">10.1007/978-3-319-78890-6_13</a>","ieee":"T. Hansmeier, M. Platzner, and D. Andrews, “An FPGA/HMC-Based Accelerator for Resolution Proof Checking,” in <i>ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications</i>, Santorini, Greece, 2018, vol. 10824, pp. 153–165.","chicago":"Hansmeier, Tim, Marco Platzner, and David Andrews. “An FPGA/HMC-Based Accelerator for Resolution Proof Checking.” In <i>ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications</i>, 10824:153–65. Lecture Notes in Computer Science. Springer International Publishing, 2018. <a href=\"https://doi.org/10.1007/978-3-319-78890-6_13\">https://doi.org/10.1007/978-3-319-78890-6_13</a>.","apa":"Hansmeier, T., Platzner, M., &#38; Andrews, D. (2018). An FPGA/HMC-Based Accelerator for Resolution Proof Checking. In <i>ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications</i> (Vol. 10824, pp. 153–165). Santorini, Greece: Springer International Publishing. <a href=\"https://doi.org/10.1007/978-3-319-78890-6_13\">https://doi.org/10.1007/978-3-319-78890-6_13</a>","mla":"Hansmeier, Tim, et al. “An FPGA/HMC-Based Accelerator for Resolution Proof Checking.” <i>ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications</i>, vol. 10824, Springer International Publishing, 2018, pp. 153–65, doi:<a href=\"https://doi.org/10.1007/978-3-319-78890-6_13\">10.1007/978-3-319-78890-6_13</a>.","bibtex":"@inproceedings{Hansmeier_Platzner_Andrews_2018, series={Lecture Notes in Computer Science}, title={An FPGA/HMC-Based Accelerator for Resolution Proof Checking}, volume={10824}, DOI={<a href=\"https://doi.org/10.1007/978-3-319-78890-6_13\">10.1007/978-3-319-78890-6_13</a>}, booktitle={ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications}, publisher={Springer International Publishing}, author={Hansmeier, Tim and Platzner, Marco and Andrews, David}, year={2018}, pages={153–165}, collection={Lecture Notes in Computer Science} }","short":"T. Hansmeier, M. Platzner, D. Andrews, in: ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications, Springer International Publishing, 2018, pp. 153–165."},"volume":10824,"author":[{"first_name":"Tim","id":"49992","full_name":"Hansmeier, Tim","orcid":"0000-0003-1377-3339","last_name":"Hansmeier"},{"full_name":"Platzner, Marco","id":"398","last_name":"Platzner","first_name":"Marco"},{"first_name":"David","last_name":"Andrews","full_name":"Andrews, David"}],"date_updated":"2022-01-06T06:59:13Z","doi":"10.1007/978-3-319-78890-6_13","conference":{"start_date":"2018-05-02","name":"ARC: International Symposium on Applied Reconfigurable Computing","location":"Santorini, Greece","end_date":"2018-05-04"},"type":"conference","status":"public","department":[{"_id":"78"}],"user_id":"3118","series_title":"Lecture Notes in Computer Science","_id":"3373","project":[{"name":"SFB 901 - Subproject B4","_id":"12"},{"_id":"1","name":"SFB 901"},{"_id":"3","name":"SFB 901 - Project Area B"}],"file_date_updated":"2018-11-02T13:55:07Z","year":"2018","date_created":"2018-06-27T09:30:24Z","publisher":"Springer International Publishing","title":"An FPGA/HMC-Based Accelerator for Resolution Proof Checking","publication":"ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications","file":[{"relation":"main_file","success":1,"content_type":"application/pdf","file_name":"AnFPGAHMC-BasedAcceleratorForR.pdf","file_id":"5257","access_level":"closed","file_size":612367,"creator":"ups","date_created":"2018-11-02T13:55:07Z","date_updated":"2018-11-02T13:55:07Z"}],"abstract":[{"text":"Modern Boolean satisfiability solvers can emit proofs of unsatisfiability. There is substantial interest in being able to verify such proofs and also in using them for further computations. In this paper, we present an FPGA accelerator for checking resolution proofs, a popular proof format. Our accelerator exploits parallelism at the low level by implementing the basic resolution step in hardware, and at the high level by instantiating a number of parallel modules for proof checking. Since proof checking involves highly irregular memory accesses, we employ Hybrid Memory Cube technology for accelerator memory. The results show that while the accelerator is scalable and achieves speedups for all benchmark proofs, performance improvements are currently limited by the overhead of transitioning the proof into the accelerator memory.","lang":"eng"}],"language":[{"iso":"eng"}],"ddc":["000"]},{"date_updated":"2022-01-06T06:59:26Z","author":[{"id":"49051","full_name":"Witschen, Linus Matthias","last_name":"Witschen","first_name":"Linus Matthias"},{"first_name":"Tobias","last_name":"Wiersema","id":"3118","full_name":"Wiersema, Tobias"},{"last_name":"Ghasemzadeh Mohammadi","full_name":"Ghasemzadeh Mohammadi, Hassan","id":"61186","first_name":"Hassan"},{"first_name":"Muhammad","id":"64665","full_name":"Awais, Muhammad","last_name":"Awais","orcid":"https://orcid.org/0000-0003-4148-2969"},{"last_name":"Platzner","id":"398","full_name":"Platzner, Marco","first_name":"Marco"}],"date_created":"2018-07-20T14:10:46Z","title":"CIRCA: Towards a Modular and Extensible Framework for Approximate Circuit Generation","has_accepted_license":"1","publication_status":"accepted","year":"2018","page":"6","citation":{"apa":"Witschen, L. M., Wiersema, T., Ghasemzadeh Mohammadi, H., Awais, M., &#38; Platzner, M. (n.d.). CIRCA: Towards a Modular and Extensible Framework for Approximate Circuit Generation. <i>Third Workshop on Approximate Computing (AxC 2018)</i>.","mla":"Witschen, Linus Matthias, et al. “CIRCA: Towards a Modular and Extensible Framework for Approximate Circuit Generation.” <i>Third Workshop on Approximate Computing (AxC 2018)</i>.","bibtex":"@article{Witschen_Wiersema_Ghasemzadeh Mohammadi_Awais_Platzner, title={CIRCA: Towards a Modular and Extensible Framework for Approximate Circuit Generation}, journal={Third Workshop on Approximate Computing (AxC 2018)}, author={Witschen, Linus Matthias and Wiersema, Tobias and Ghasemzadeh Mohammadi, Hassan and Awais, Muhammad and Platzner, Marco} }","short":"L.M. Witschen, T. Wiersema, H. Ghasemzadeh Mohammadi, M. Awais, M. Platzner, Third Workshop on Approximate Computing (AxC 2018) (n.d.).","chicago":"Witschen, Linus Matthias, Tobias Wiersema, Hassan Ghasemzadeh Mohammadi, Muhammad Awais, and Marco Platzner. “CIRCA: Towards a Modular and Extensible Framework for Approximate Circuit Generation.” <i>Third Workshop on Approximate Computing (AxC 2018)</i>, n.d.","ieee":"L. M. Witschen, T. Wiersema, H. Ghasemzadeh Mohammadi, M. Awais, and M. Platzner, “CIRCA: Towards a Modular and Extensible Framework for Approximate Circuit Generation,” <i>Third Workshop on Approximate Computing (AxC 2018)</i>. .","ama":"Witschen LM, Wiersema T, Ghasemzadeh Mohammadi H, Awais M, Platzner M. CIRCA: Towards a Modular and Extensible Framework for Approximate Circuit Generation. <i>Third Workshop on Approximate Computing (AxC 2018)</i>."},"_id":"3586","project":[{"name":"SFB 901 - Subproject B4","_id":"12"},{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Project Area B","_id":"3"},{"name":"Computing Resources Provided by the Paderborn Center for Parallel Computing","_id":"52"}],"department":[{"_id":"78"}],"user_id":"49051","keyword":["Approximate Computing","Framework","Pareto Front","Accuracy"],"ddc":["000"],"file_date_updated":"2018-07-20T14:13:31Z","language":[{"iso":"eng"}],"publication":"Third Workshop on Approximate Computing (AxC 2018)","type":"preprint","abstract":[{"lang":"eng","text":"Existing approaches and tools for the generation of approximate circuits often lack generality and are restricted to certain circuit types, approximation techniques, and quality assurance methods. Moreover, only few tools are publicly available. This hinders the development and evaluation of new techniques for approximating circuits and their comparison to previous approaches. In this paper, we first analyze and classify related approaches and then present CIRCA, our flexible framework for search-based approximate circuit generation. CIRCA is developed with a focus on modularity and extensibility. We present the architecture of CIRCA with its clear separation into stages and functional blocks, report on the current prototype, and show initial experiments."}],"status":"public","file":[{"file_size":285348,"file_id":"3587","access_level":"closed","file_name":"WitschenWMAP2018.pdf","date_updated":"2018-07-20T14:13:31Z","creator":"tobias82","date_created":"2018-07-20T14:13:31Z","success":1,"relation":"main_file","content_type":"application/pdf"}]},{"publication_status":"published","year":"2018","page":"139","citation":{"ama":"Ho N. <i>FPGA-Based Reconfigurable Cache Mapping Schemes: Design and Optimization</i>. Universität Paderborn; 2018. doi:<a href=\"https://doi.org/10.17619/UNIPB/1-376\">10.17619/UNIPB/1-376</a>","ieee":"N. Ho, <i>FPGA-based Reconfigurable Cache Mapping Schemes: Design and Optimization</i>. Universität Paderborn, 2018.","chicago":"Ho, Nam. <i>FPGA-Based Reconfigurable Cache Mapping Schemes: Design and Optimization</i>. Universität Paderborn, 2018. <a href=\"https://doi.org/10.17619/UNIPB/1-376\">https://doi.org/10.17619/UNIPB/1-376</a>.","apa":"Ho, N. (2018). <i>FPGA-based Reconfigurable Cache Mapping Schemes: Design and Optimization</i>. Universität Paderborn. <a href=\"https://doi.org/10.17619/UNIPB/1-376\">https://doi.org/10.17619/UNIPB/1-376</a>","mla":"Ho, Nam. <i>FPGA-Based Reconfigurable Cache Mapping Schemes: Design and Optimization</i>. Universität Paderborn, 2018, doi:<a href=\"https://doi.org/10.17619/UNIPB/1-376\">10.17619/UNIPB/1-376</a>.","short":"N. Ho, FPGA-Based Reconfigurable Cache Mapping Schemes: Design and Optimization, Universität Paderborn, 2018.","bibtex":"@book{Ho_2018, title={FPGA-based Reconfigurable Cache Mapping Schemes: Design and Optimization}, DOI={<a href=\"https://doi.org/10.17619/UNIPB/1-376\">10.17619/UNIPB/1-376</a>}, publisher={Universität Paderborn}, author={Ho, Nam}, year={2018} }"},"publisher":"Universität Paderborn","date_updated":"2022-01-06T06:59:31Z","author":[{"first_name":"Nam","full_name":"Ho, Nam","last_name":"Ho"}],"date_created":"2018-07-27T06:41:13Z","supervisor":[{"first_name":"Paul","last_name":"Kaufmann","full_name":"Kaufmann, Paul"},{"first_name":"Marco","last_name":"Platzner","id":"398","full_name":"Platzner, Marco"}],"title":"FPGA-based Reconfigurable Cache Mapping Schemes: Design and Optimization","doi":"10.17619/UNIPB/1-376","type":"dissertation","abstract":[{"lang":"eng","text":"Traditional cache design uses a consolidated block of memory address bits to index a cache set, equivalent to the use of modulo functions. While this module-based mapping scheme is widely used in contemporary cache structures due to the simplicity of its hardware design and its good performance for sequences of consecutive addresses, its use may not be satisfactory for a variety of application domains having different characteristics.This thesis presents a new type of cache mapping scheme, motivated by programmable capabilities combined with Nature-inspired optimization of reconfigurable hardware. This research has focussed on an FPGA-based evolvable cache structure of the first level cache in a multi-core processor architecture, able to dynamically change cache indexing. To solve the challenge of reconfigurable cache mappings, a programmable Boolean circuit based on a combination of Look-up Table (LUT) memory elements is proposed. Focusing on optimization aspects at the system level, a Performance Measurement Infrastructure is introduced that is able to monitor the underlying microarchitectural metrics, and an adaptive evaluation strategy is presented that leverages on Evolutionary Algorithms, that is not only capable of evolving application-specific address-to-cache-index mappings for level one split caches but also of reducing optimization times. Putting this all together and prototyping in an FPGA for a LEON3/Linux-based multi-core processor, the creation of a system architecture reduces cache misses and improves performance over the use of conventional caches."},{"lang":"ger","text":"Traditionelle Cachedesigns verwenden konsolidierte Blöcke von Speicheradressbits um einen Cachesatz zu indizieren, vergleichbar mit der Anwendung einer Modulofunktion. Obwohl dieses modulobasierte Abbildungsschema in heutigen Cachestrukturen weit verbreitet ist, vor allem wegen seiner einfachen Anforderungen an das Hardwaredesign und seiner Effizienz für die Indizierung eufeinanderfolgender Speicheradressen, kann seine Verwendung für eine Vielzahl von Anwendungsdomänen mit unterschiedlichen Charakteristiken zu suboptimalen Ergebnissen führen. Diese Dissertation präsentiert einen neuen Typ von Cacheabbildungsschema, motiviert durch die Kombination programmierbarer Ressourcen mit der naturinspirierten Optimierung rekonfigurierbarer Hardware. Im Fokus dieser Forschung steht eine FPGA-basierte Cachestruktur für den first level Cache einer Mehrkernprozessorarchitektur, welche die Cacheindizierung dynamisch ändern kann. Um die Herausforderung rekonfigurierbarer Cacheabbildungen zu lösen, wird eine reprogrammierbare Boolesche Schaltung eingeführt, die auf Look-up Table (LUT) Speicherelementen basiert. Weiterhin wird eine Infrastruktur zur Effizienzmessung eingeführt, welche die zugrundeliege Mikroarchitektur überwachen kann, sowie eine adaptive Evaluationsstrategie präsentiert, die evolutionäre Algorithmen wirksam einsetzt, und die nicht nur anwendungsspezifische Abbildungen von Speicheradressen zu Cacheindizes für level one Caches evolvieren sondern dabei auch die Optimierungszeiten reduzieren kann. All diese Aspekte zusammen in einer prototypischen Implementierung auf einem FPGA für einen LEON3/Linux-basierten Mehrkernprozessor zeigen, dass evolvierbare Cacheabbildungsfunktionen Cache Misses reduzieren, sowie die Effizienz im Vergleich zu konventionellen Caches erhöhen können."}],"status":"public","_id":"3720","project":[{"name":"SFB 901 - Subproject B4","_id":"12"},{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Project Area B","_id":"3"}],"department":[{"_id":"78"}],"user_id":"477","language":[{"iso":"eng"}]},{"department":[{"_id":"77"},{"_id":"76"}],"user_id":"477","_id":"2711","project":[{"_id":"1","name":"SFB 901"},{"_id":"3","name":"SFB 901 - Project Area B"},{"_id":"12","name":"SFB 901 - Subproject B4"}],"file_date_updated":"2018-11-21T10:49:23Z","language":[{"iso":"eng"}],"ddc":["000"],"publication":"arXiv:1804.02903","type":"preprint","status":"public","file":[{"success":1,"relation":"main_file","content_type":"application/pdf","file_size":1045861,"access_level":"closed","file_id":"5781","file_name":"Do Android Taint Analysis Tools Keep their Promises.pdf","date_updated":"2018-11-21T10:49:23Z","date_created":"2018-11-21T10:49:23Z","creator":"florida"}],"abstract":[{"lang":"eng","text":"In recent years, researchers have developed a number of tools to conduct\r\ntaint analysis of Android applications. While all the respective papers aim at\r\nproviding a thorough empirical evaluation, comparability is hindered by varying\r\nor unclear evaluation targets. Sometimes, the apps used for evaluation are not\r\nprecisely described. In other cases, authors use an established benchmark but\r\ncover it only partially. In yet other cases, the evaluations differ in terms of\r\nthe data leaks searched for, or lack a ground truth to compare against. All\r\nthose limitations make it impossible to truly compare the tools based on those\r\npublished evaluations.\r\n  We thus present ReproDroid, a framework allowing the accurate comparison of\r\nAndroid taint analysis tools. ReproDroid supports researchers in inferring the\r\nground truth for data leaks in apps, in automatically applying tools to\r\nbenchmarks, and in evaluating the obtained results. We use ReproDroid to\r\ncomparatively evaluate on equal grounds the six prominent taint analysis tools\r\nAmandroid, DIALDroid, DidFail, DroidSafe, FlowDroid and IccTA. The results are\r\nlargely positive although four tools violate some promises concerning features\r\nand accuracy. Finally, we contribute to the area of unbiased benchmarking with\r\na new and improved version of the open test suite DroidBench."}],"author":[{"first_name":"Felix","full_name":"Pauck, Felix","id":"22398","last_name":"Pauck"},{"first_name":"Eric","id":"59256","full_name":"Bodden, Eric","last_name":"Bodden","orcid":"0000-0003-3470-3647"},{"first_name":"Heike","last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike"}],"date_created":"2018-05-09T08:27:11Z","date_updated":"2022-01-06T06:57:35Z","title":"Do Android Taint Analysis Tools Keep their Promises?","has_accepted_license":"1","citation":{"apa":"Pauck, F., Bodden, E., &#38; Wehrheim, H. (2018). Do Android Taint Analysis Tools Keep their Promises? <i>ArXiv:1804.02903</i>.","short":"F. Pauck, E. Bodden, H. Wehrheim, ArXiv:1804.02903 (2018).","mla":"Pauck, Felix, et al. “Do Android Taint Analysis Tools Keep Their Promises?” <i>ArXiv:1804.02903</i>, 2018.","bibtex":"@article{Pauck_Bodden_Wehrheim_2018, title={Do Android Taint Analysis Tools Keep their Promises?}, journal={arXiv:1804.02903}, author={Pauck, Felix and Bodden, Eric and Wehrheim, Heike}, year={2018} }","ieee":"F. Pauck, E. Bodden, and H. Wehrheim, “Do Android Taint Analysis Tools Keep their Promises?,” <i>arXiv:1804.02903</i>. 2018.","chicago":"Pauck, Felix, Eric Bodden, and Heike Wehrheim. “Do Android Taint Analysis Tools Keep Their Promises?” <i>ArXiv:1804.02903</i>, 2018.","ama":"Pauck F, Bodden E, Wehrheim H. Do Android Taint Analysis Tools Keep their Promises? <i>arXiv:180402903</i>. 2018."},"year":"2018"},{"status":"public","file":[{"file_id":"5821","file_name":"WitschenWP2018[1].pdf","access_level":"closed","file_size":287224,"date_created":"2018-11-26T08:00:53Z","creator":"tobias82","date_updated":"2018-11-26T08:00:53Z","relation":"main_file","success":1,"content_type":"application/pdf"}],"publication":"4th Workshop On Approximate Computing (WAPCO 2018)","type":"preprint","language":[{"iso":"eng"}],"file_date_updated":"2018-11-26T08:00:53Z","ddc":["000"],"department":[{"_id":"7"},{"_id":"34"},{"_id":"78"}],"user_id":"49051","_id":"1165","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Project Area B","_id":"3"},{"name":"SFB 901 - Subproject B4","_id":"12"},{"name":"Computing Resources Provided by the Paderborn Center for Parallel Computing","_id":"52"}],"citation":{"ama":"Witschen LM, Wiersema T, Platzner M. Making the Case for Proof-carrying Approximate Circuits. <i>4th Workshop On Approximate Computing (WAPCO 2018)</i>. 2018.","ieee":"L. M. Witschen, T. Wiersema, and M. Platzner, “Making the Case for Proof-carrying Approximate Circuits,” <i>4th Workshop On Approximate Computing (WAPCO 2018)</i>. 2018.","chicago":"Witschen, Linus Matthias, Tobias Wiersema, and Marco Platzner. “Making the Case for Proof-Carrying Approximate Circuits.” <i>4th Workshop On Approximate Computing (WAPCO 2018)</i>, 2018.","bibtex":"@article{Witschen_Wiersema_Platzner_2018, title={Making the Case for Proof-carrying Approximate Circuits}, journal={4th Workshop On Approximate Computing (WAPCO 2018)}, author={Witschen, Linus Matthias and Wiersema, Tobias and Platzner, Marco}, year={2018} }","mla":"Witschen, Linus Matthias, et al. “Making the Case for Proof-Carrying Approximate Circuits.” <i>4th Workshop On Approximate Computing (WAPCO 2018)</i>, 2018.","short":"L.M. Witschen, T. Wiersema, M. Platzner, 4th Workshop On Approximate Computing (WAPCO 2018) (2018).","apa":"Witschen, L. M., Wiersema, T., &#38; Platzner, M. (2018). Making the Case for Proof-carrying Approximate Circuits. <i>4th Workshop On Approximate Computing (WAPCO 2018)</i>."},"year":"2018","has_accepted_license":"1","title":"Making the Case for Proof-carrying Approximate Circuits","author":[{"last_name":"Witschen","id":"49051","full_name":"Witschen, Linus Matthias","first_name":"Linus Matthias"},{"last_name":"Wiersema","id":"3118","full_name":"Wiersema, Tobias","first_name":"Tobias"},{"last_name":"Platzner","id":"398","full_name":"Platzner, Marco","first_name":"Marco"}],"date_created":"2018-02-01T14:24:54Z","date_updated":"2022-01-06T06:51:06Z"},{"date_created":"2018-11-21T09:51:37Z","publisher":"Springer International Publishing","title":"Information Flow Certificates","year":"2018","language":[{"iso":"eng"}],"ddc":["000"],"publication":"Theoretical Aspects of Computing – ICTAC 2018","file":[{"content_type":"application/pdf","success":1,"relation":"main_file","date_updated":"2018-11-26T15:11:32Z","date_created":"2018-11-26T15:11:32Z","creator":"mtoews","file_size":518016,"file_name":"Töws-Wehrheim2018_Chapter_InformationFlowCertificates.pdf","file_id":"5837","access_level":"closed"}],"abstract":[{"text":"Information flow analysis investigates the flow of data in applications, checking in particular for flows from private sources to public sinks. Flow- and path-sensitive analyses are, however, often too costly to be performed every time a security-critical application is run. In this paper, we propose a variant of proof carrying code for information flow security. To this end, we develop information flow (IF) certificates which get attached to programs as well as a method for IF certificate validation. We prove soundness of our technique, i.e., show it to be tamper-free. The technique is implemented within the program analysis tool CPAchecker. Our experiments confirm that the use of certificates pays off for costly analysis runs.","lang":"eng"}],"author":[{"full_name":"Töws, Manuel","id":"11315","last_name":"Töws","first_name":"Manuel"},{"first_name":"Heike","last_name":"Wehrheim","full_name":"Wehrheim, Heike","id":"573"}],"date_updated":"2022-01-06T07:02:40Z","doi":"10.1007/978-3-030-02508-3_23","publication_status":"published","has_accepted_license":"1","publication_identifier":{"issn":["0302-9743","1611-3349"],"isbn":["9783030025076","9783030025083"]},"citation":{"apa":"Töws, M., &#38; Wehrheim, H. (2018). Information Flow Certificates. In <i>Theoretical Aspects of Computing – ICTAC 2018</i> (pp. 435–454). Cham: Springer International Publishing. <a href=\"https://doi.org/10.1007/978-3-030-02508-3_23\">https://doi.org/10.1007/978-3-030-02508-3_23</a>","bibtex":"@inproceedings{Töws_Wehrheim_2018, place={Cham}, title={Information Flow Certificates}, DOI={<a href=\"https://doi.org/10.1007/978-3-030-02508-3_23\">10.1007/978-3-030-02508-3_23</a>}, booktitle={Theoretical Aspects of Computing – ICTAC 2018}, publisher={Springer International Publishing}, author={Töws, Manuel and Wehrheim, Heike}, year={2018}, pages={435–454} }","mla":"Töws, Manuel, and Heike Wehrheim. “Information Flow Certificates.” <i>Theoretical Aspects of Computing – ICTAC 2018</i>, Springer International Publishing, 2018, pp. 435–54, doi:<a href=\"https://doi.org/10.1007/978-3-030-02508-3_23\">10.1007/978-3-030-02508-3_23</a>.","short":"M. Töws, H. Wehrheim, in: Theoretical Aspects of Computing – ICTAC 2018, Springer International Publishing, Cham, 2018, pp. 435–454.","ama":"Töws M, Wehrheim H. Information Flow Certificates. In: <i>Theoretical Aspects of Computing – ICTAC 2018</i>. Cham: Springer International Publishing; 2018:435-454. doi:<a href=\"https://doi.org/10.1007/978-3-030-02508-3_23\">10.1007/978-3-030-02508-3_23</a>","ieee":"M. Töws and H. Wehrheim, “Information Flow Certificates,” in <i>Theoretical Aspects of Computing – ICTAC 2018</i>, 2018, pp. 435–454.","chicago":"Töws, Manuel, and Heike Wehrheim. “Information Flow Certificates.” In <i>Theoretical Aspects of Computing – ICTAC 2018</i>, 435–54. Cham: Springer International Publishing, 2018. <a href=\"https://doi.org/10.1007/978-3-030-02508-3_23\">https://doi.org/10.1007/978-3-030-02508-3_23</a>."},"page":"435-454","place":"Cham","user_id":"477","department":[{"_id":"77"}],"project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Project Area B","_id":"3"},{"name":"SFB 901 - Subproject B4","_id":"12"}],"_id":"5774","file_date_updated":"2018-11-26T15:11:32Z","type":"conference","status":"public"},{"year":"2018","title":"Do Android taint analysis tools keep their promises?","publisher":"ACM Press","date_created":"2018-10-30T08:03:17Z","file":[{"content_type":"application/pdf","relation":"main_file","success":1,"date_created":"2018-11-02T13:37:38Z","creator":"ups","date_updated":"2018-11-02T13:37:38Z","file_id":"5251","access_level":"closed","file_name":"fse18main-id76-p.pdf","file_size":524169}],"publication":"Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering  - ESEC/FSE 2018","ddc":["004"],"language":[{"iso":"eng"}],"citation":{"ama":"Pauck F, Bodden E, Wehrheim H. Do Android taint analysis tools keep their promises? In: <i>Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering  - ESEC/FSE 2018</i>. ACM Press; 2018. doi:<a href=\"https://doi.org/10.1145/3236024.3236029\">10.1145/3236024.3236029</a>","ieee":"F. Pauck, E. Bodden, and H. Wehrheim, “Do Android taint analysis tools keep their promises?,” in <i>Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering  - ESEC/FSE 2018</i>, 2018.","chicago":"Pauck, Felix, Eric Bodden, and Heike Wehrheim. “Do Android Taint Analysis Tools Keep Their Promises?” In <i>Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering  - ESEC/FSE 2018</i>. ACM Press, 2018. <a href=\"https://doi.org/10.1145/3236024.3236029\">https://doi.org/10.1145/3236024.3236029</a>.","mla":"Pauck, Felix, et al. “Do Android Taint Analysis Tools Keep Their Promises?” <i>Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering  - ESEC/FSE 2018</i>, ACM Press, 2018, doi:<a href=\"https://doi.org/10.1145/3236024.3236029\">10.1145/3236024.3236029</a>.","short":"F. Pauck, E. Bodden, H. Wehrheim, in: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering  - ESEC/FSE 2018, ACM Press, 2018.","bibtex":"@inproceedings{Pauck_Bodden_Wehrheim_2018, title={Do Android taint analysis tools keep their promises?}, DOI={<a href=\"https://doi.org/10.1145/3236024.3236029\">10.1145/3236024.3236029</a>}, booktitle={Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering  - ESEC/FSE 2018}, publisher={ACM Press}, author={Pauck, Felix and Bodden, Eric and Wehrheim, Heike}, year={2018} }","apa":"Pauck, F., Bodden, E., &#38; Wehrheim, H. (2018). Do Android taint analysis tools keep their promises? In <i>Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering  - ESEC/FSE 2018</i>. ACM Press. <a href=\"https://doi.org/10.1145/3236024.3236029\">https://doi.org/10.1145/3236024.3236029</a>"},"publication_identifier":{"isbn":["9781450355735"]},"has_accepted_license":"1","publication_status":"published","doi":"10.1145/3236024.3236029","date_updated":"2022-01-06T07:01:34Z","author":[{"last_name":"Pauck","id":"22398","full_name":"Pauck, Felix","first_name":"Felix"},{"first_name":"Eric","id":"59256","full_name":"Bodden, Eric","last_name":"Bodden","orcid":"0000-0003-3470-3647"},{"last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike","first_name":"Heike"}],"status":"public","type":"conference","file_date_updated":"2018-11-02T13:37:38Z","_id":"4999","project":[{"_id":"3","name":"SFB 901 - Project Area B"},{"name":"SFB 901 - Subproject B4","_id":"12"},{"name":"SFB 901","_id":"1"}],"department":[{"_id":"77"},{"_id":"76"}],"user_id":"477"},{"keyword":["ITSECWEBSITE","CROSSING"],"ddc":["000"],"file_date_updated":"2018-11-02T13:51:05Z","language":[{"iso":"eng"}],"_id":"5203","project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Project Area B","_id":"3"},{"_id":"12","name":"SFB 901 - Subproject B4"}],"department":[{"_id":"76"}],"user_id":"477","status":"public","file":[{"success":1,"relation":"main_file","content_type":"application/pdf","file_size":747259,"file_id":"5255","access_level":"closed","file_name":"ksa+18crysl.pdf","date_updated":"2018-11-02T13:51:05Z","creator":"ups","date_created":"2018-11-02T13:51:05Z"}],"publication":"European Conference on Object-Oriented Programming (ECOOP)","type":"conference","title":"CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs","main_file_link":[{"url":"http://bodden.de/pubs/ksa+18crysl.pdf"}],"date_updated":"2022-01-06T07:01:44Z","author":[{"first_name":"Stefan","last_name":"Krüger","full_name":"Krüger, Stefan"},{"last_name":"Späth","full_name":"Späth, Johannes","first_name":"Johannes"},{"first_name":"Karim","last_name":"Ali","full_name":"Ali, Karim"},{"id":"59256","full_name":"Bodden, Eric","orcid":"0000-0003-3470-3647","last_name":"Bodden","first_name":"Eric"},{"full_name":"Mezini, Mira","last_name":"Mezini","first_name":"Mira"}],"date_created":"2018-10-31T12:37:29Z","year":"2018","page":"10:1-10:27","citation":{"chicago":"Krüger, Stefan, Johannes Späth, Karim Ali, Eric Bodden, and Mira Mezini. “CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs.” In <i>European Conference on Object-Oriented Programming (ECOOP)</i>, 10:1-10:27, 2018.","ieee":"S. Krüger, J. Späth, K. Ali, E. Bodden, and M. Mezini, “CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs,” in <i>European Conference on Object-Oriented Programming (ECOOP)</i>, 2018, pp. 10:1-10:27.","ama":"Krüger S, Späth J, Ali K, Bodden E, Mezini M. CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs. In: <i>European Conference on Object-Oriented Programming (ECOOP)</i>. ; 2018:10:1-10:27.","bibtex":"@inproceedings{Krüger_Späth_Ali_Bodden_Mezini_2018, title={CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs}, booktitle={European Conference on Object-Oriented Programming (ECOOP)}, author={Krüger, Stefan and Späth, Johannes and Ali, Karim and Bodden, Eric and Mezini, Mira}, year={2018}, pages={10:1-10:27} }","mla":"Krüger, Stefan, et al. “CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs.” <i>European Conference on Object-Oriented Programming (ECOOP)</i>, 2018, pp. 10:1-10:27.","short":"S. Krüger, J. Späth, K. Ali, E. Bodden, M. Mezini, in: European Conference on Object-Oriented Programming (ECOOP), 2018, pp. 10:1-10:27.","apa":"Krüger, S., Späth, J., Ali, K., Bodden, E., &#38; Mezini, M. (2018). CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs. In <i>European Conference on Object-Oriented Programming (ECOOP)</i> (pp. 10:1-10:27)."},"has_accepted_license":"1"},{"year":"2018","title":"Validity of Software Verification Results on Approximate Hardware","publisher":"Institute of Electrical and Electronics Engineers (IEEE)","date_created":"2017-12-11T16:11:00Z","abstract":[{"text":"Approximate computing (AC) is an emerging paradigm for energy-efficient computation. The basic idea of AC is to sacrifice high precision for low energy by allowing hardware to carry out “approximately correct” calculations. This provides a major challenge for software quality assurance: programs successfully verified to be correct might be erroneous on approximate hardware. In this letter, we present a novel approach for determining under what conditions a software verification result is valid for approximate hardware. To this end, we compute the allowed tolerances for AC hardware from successful verification runs. More precisely, we derive a set of constraints which—when met by the AC hardware—guarantees the verification result to carry over to AC. On the practical side, we furthermore: 1) show how to extract tolerances from verification runs employing predicate abstraction as verification technology and 2) show how to check such constraints on hardware designs. We have implemented all techniques, and exemplify them on example C programs and a number of recently proposed approximate adders.","lang":"eng"}],"file":[{"date_updated":"2018-11-02T15:27:04Z","creator":"ups","date_created":"2018-11-02T15:27:04Z","file_size":523362,"file_name":"08053741.pdf","file_id":"5303","access_level":"closed","content_type":"application/pdf","success":1,"relation":"main_file"}],"publication":"IEEE Embedded Systems Letters","ddc":["000"],"language":[{"iso":"eng"}],"citation":{"ama":"Isenberg T, Jakobs M-C, Pauck F, Wehrheim H. Validity of Software Verification Results on Approximate Hardware. <i>IEEE Embedded Systems Letters</i>. 2018:22-25. doi:<a href=\"https://doi.org/10.1109/LES.2017.2758200\">10.1109/LES.2017.2758200</a>","chicago":"Isenberg, Tobias, Marie-Christine Jakobs, Felix Pauck, and Heike Wehrheim. “Validity of Software Verification Results on Approximate Hardware.” <i>IEEE Embedded Systems Letters</i>, 2018, 22–25. <a href=\"https://doi.org/10.1109/LES.2017.2758200\">https://doi.org/10.1109/LES.2017.2758200</a>.","ieee":"T. Isenberg, M.-C. Jakobs, F. Pauck, and H. Wehrheim, “Validity of Software Verification Results on Approximate Hardware,” <i>IEEE Embedded Systems Letters</i>, pp. 22–25, 2018.","apa":"Isenberg, T., Jakobs, M.-C., Pauck, F., &#38; Wehrheim, H. (2018). Validity of Software Verification Results on Approximate Hardware. <i>IEEE Embedded Systems Letters</i>, 22–25. <a href=\"https://doi.org/10.1109/LES.2017.2758200\">https://doi.org/10.1109/LES.2017.2758200</a>","bibtex":"@article{Isenberg_Jakobs_Pauck_Wehrheim_2018, title={Validity of Software Verification Results on Approximate Hardware}, DOI={<a href=\"https://doi.org/10.1109/LES.2017.2758200\">10.1109/LES.2017.2758200</a>}, journal={IEEE Embedded Systems Letters}, publisher={Institute of Electrical and Electronics Engineers (IEEE)}, author={Isenberg, Tobias and Jakobs, Marie-Christine and Pauck, Felix and Wehrheim, Heike}, year={2018}, pages={22–25} }","mla":"Isenberg, Tobias, et al. “Validity of Software Verification Results on Approximate Hardware.” <i>IEEE Embedded Systems Letters</i>, Institute of Electrical and Electronics Engineers (IEEE), 2018, pp. 22–25, doi:<a href=\"https://doi.org/10.1109/LES.2017.2758200\">10.1109/LES.2017.2758200</a>.","short":"T. Isenberg, M.-C. Jakobs, F. Pauck, H. Wehrheim, IEEE Embedded Systems Letters (2018) 22–25."},"page":"22-25","publication_status":"published","has_accepted_license":"1","publication_identifier":{"issn":["1943-0663","1943-0671"]},"doi":"10.1109/LES.2017.2758200","date_updated":"2022-01-06T06:50:39Z","author":[{"full_name":"Isenberg, Tobias","last_name":"Isenberg","first_name":"Tobias"},{"first_name":"Marie-Christine","last_name":"Jakobs","full_name":"Jakobs, Marie-Christine"},{"first_name":"Felix","last_name":"Pauck","full_name":"Pauck, Felix","id":"22398"},{"id":"573","full_name":"Wehrheim, Heike","last_name":"Wehrheim","first_name":"Heike"}],"status":"public","type":"journal_article","file_date_updated":"2018-11-02T15:27:04Z","project":[{"_id":"1","name":"SFB 901"},{"_id":"3","name":"SFB 901 - Project Area B"},{"name":"SFB 901 - Subproject B4","_id":"12"}],"_id":"1043","user_id":"477","department":[{"_id":"77"}]},{"author":[{"full_name":"Leer, Richard","last_name":"Leer","first_name":"Richard"}],"date_created":"2017-12-13T07:52:01Z","supervisor":[{"full_name":"Bodden, Eric","id":"59256","orcid":"0000-0003-3470-3647","last_name":"Bodden","first_name":"Eric"}],"publisher":"Universität Paderborn","date_updated":"2022-01-06T06:50:39Z","title":"Measuring Performance of a Static Analysis Framework with an application to Immutability Analysis","has_accepted_license":"1","citation":{"ama":"Leer R. <i>Measuring Performance of a Static Analysis Framework with an Application to Immutability Analysis</i>. Universität Paderborn; 2018.","chicago":"Leer, Richard. <i>Measuring Performance of a Static Analysis Framework with an Application to Immutability Analysis</i>. Universität Paderborn, 2018.","ieee":"R. Leer, <i>Measuring Performance of a Static Analysis Framework with an application to Immutability Analysis</i>. Universität Paderborn, 2018.","apa":"Leer, R. (2018). <i>Measuring Performance of a Static Analysis Framework with an application to Immutability Analysis</i>. Universität Paderborn.","short":"R. Leer, Measuring Performance of a Static Analysis Framework with an Application to Immutability Analysis, Universität Paderborn, 2018.","bibtex":"@book{Leer_2018, title={Measuring Performance of a Static Analysis Framework with an application to Immutability Analysis}, publisher={Universität Paderborn}, author={Leer, Richard}, year={2018} }","mla":"Leer, Richard. <i>Measuring Performance of a Static Analysis Framework with an Application to Immutability Analysis</i>. Universität Paderborn, 2018."},"year":"2018","user_id":"15504","department":[{"_id":"76"}],"project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Project Area B","_id":"3"},{"name":"SFB 901 - Subproject B4","_id":"12"}],"_id":"1044","file_date_updated":"2018-11-21T06:15:51Z","language":[{"iso":"eng"}],"ddc":["000"],"type":"bachelorsthesis","file":[{"relation":"main_file","success":1,"content_type":"application/pdf","file_name":"ba_leer.pdf","file_id":"5768","access_level":"closed","file_size":1383049,"date_created":"2018-11-21T06:15:51Z","creator":"florida","date_updated":"2018-11-21T06:15:51Z"}],"status":"public"},{"year":"2018","citation":{"ama":"Strüwer JN. <i>Interactive Data Visualization for Exploded Supergraphs</i>. Universität Paderborn; 2018.","ieee":"J. N. Strüwer, <i>Interactive Data Visualization for Exploded Supergraphs</i>. Universität Paderborn, 2018.","chicago":"Strüwer, Jan Niclas. <i>Interactive Data Visualization for Exploded Supergraphs</i>. Universität Paderborn, 2018.","mla":"Strüwer, Jan Niclas. <i>Interactive Data Visualization for Exploded Supergraphs</i>. Universität Paderborn, 2018.","short":"J.N. Strüwer, Interactive Data Visualization for Exploded Supergraphs, Universität Paderborn, 2018.","bibtex":"@book{Strüwer_2018, title={Interactive Data Visualization for Exploded Supergraphs}, publisher={Universität Paderborn}, author={Strüwer, Jan Niclas}, year={2018} }","apa":"Strüwer, J. N. (2018). <i>Interactive Data Visualization for Exploded Supergraphs</i>. Universität Paderborn."},"has_accepted_license":"1","title":"Interactive Data Visualization for Exploded Supergraphs","date_updated":"2022-01-06T06:50:40Z","publisher":"Universität Paderborn","author":[{"first_name":"Jan Niclas","full_name":"Strüwer, Jan Niclas","last_name":"Strüwer"}],"date_created":"2017-12-13T07:53:49Z","supervisor":[{"first_name":"Eric","orcid":"0000-0003-3470-3647","last_name":"Bodden","full_name":"Bodden, Eric","id":"59256"}],"file":[{"success":1,"relation":"main_file","content_type":"application/pdf","file_size":15839765,"file_id":"5767","access_level":"closed","file_name":"ba_struewer.pdf","date_updated":"2018-11-21T06:14:15Z","creator":"florida","date_created":"2018-11-21T06:14:15Z"}],"status":"public","type":"bachelorsthesis","ddc":["000"],"file_date_updated":"2018-11-21T06:14:15Z","language":[{"iso":"eng"}],"project":[{"_id":"1","name":"SFB 901"},{"_id":"3","name":"SFB 901 - Project Area B"},{"name":"SFB 901 - Subproject B4","_id":"12"}],"_id":"1045","user_id":"15504","department":[{"_id":"76"}]},{"page":"1182--1193","citation":{"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.","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} }","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.","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.","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."},"has_accepted_license":"1","conference":{"name":"40th International Conference on Software Engineering","start_date":"2018-05-27","end_date":"2018-06-03","location":"Gothenburg, Sweden"},"date_updated":"2022-01-06T06:50:54Z","author":[{"last_name":"Beyer","full_name":"Beyer, Dirk","first_name":"Dirk"},{"full_name":"Jakobs, Marie-Christine","last_name":"Jakobs","first_name":"Marie-Christine"},{"full_name":"Lemberger, Thomas","last_name":"Lemberger","first_name":"Thomas"},{"id":"573","full_name":"Wehrheim, Heike","last_name":"Wehrheim","first_name":"Heike"}],"status":"public","type":"conference","file_date_updated":"2018-11-21T10:50:51Z","_id":"1096","project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Project Area B","_id":"3"},{"_id":"12","name":"SFB 901 - Subproject B4"},{"name":"Kooperative Softwareverifikation","_id":"85"}],"department":[{"_id":"77"}],"user_id":"29719","year":"2018","title":"Reducer-Based Construction of Conditional Verifiers","publisher":"ACM","date_created":"2018-01-08T10:52:51Z","abstract":[{"text":"to appear","lang":"eng"}],"file":[{"file_id":"5783","file_name":"Reducer-Based Construction of Conditional Verifiers.pdf","access_level":"closed","file_size":826719,"creator":"florida","date_created":"2018-11-21T10:50:51Z","date_updated":"2018-11-21T10:50:51Z","relation":"main_file","success":1,"content_type":"application/pdf"}],"publication":"Proceedings of the 40th International Conference on Software Engineering (ICSE)","ddc":["000"],"language":[{"iso":"eng"}]},{"year":"2018","citation":{"short":"F.P. Jentzsch, Enforcing IP Core Connection Properties with Verifiable Security Monitors, Universität Paderborn, 2018.","bibtex":"@book{Jentzsch_2018, title={Enforcing IP Core Connection Properties with Verifiable Security Monitors}, publisher={Universität Paderborn}, author={Jentzsch, Felix Paul}, year={2018} }","mla":"Jentzsch, Felix Paul. <i>Enforcing IP Core Connection Properties with Verifiable Security Monitors</i>. Universität Paderborn, 2018.","apa":"Jentzsch, F. P. (2018). <i>Enforcing IP Core Connection Properties with Verifiable Security Monitors</i>. Universität Paderborn.","ieee":"F. P. Jentzsch, <i>Enforcing IP Core Connection Properties with Verifiable Security Monitors</i>. Universität Paderborn, 2018.","chicago":"Jentzsch, Felix Paul. <i>Enforcing IP Core Connection Properties with Verifiable Security Monitors</i>. Universität Paderborn, 2018.","ama":"Jentzsch FP. <i>Enforcing IP Core Connection Properties with Verifiable Security Monitors</i>. Universität Paderborn; 2018."},"date_updated":"2022-01-06T06:50:54Z","publisher":"Universität Paderborn","author":[{"full_name":"Jentzsch, Felix Paul","last_name":"Jentzsch","first_name":"Felix Paul"}],"date_created":"2018-01-15T16:48:05Z","supervisor":[{"first_name":"Tobias","last_name":"Wiersema","full_name":"Wiersema, Tobias","id":"3118"}],"title":"Enforcing IP Core Connection Properties with Verifiable Security Monitors","type":"bachelorsthesis","status":"public","_id":"1097","project":[{"name":"SFB 901 - Subproject B4","_id":"12"},{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Project Area B","_id":"3"}],"department":[{"_id":"78"}],"user_id":"477","keyword":["Approximate Computing","Proof-Carrying Hardware","Formal Verification"],"language":[{"iso":"eng"}]},{"supervisor":[{"id":"398","full_name":"Platzner, Marco","last_name":"Platzner","first_name":"Marco"}],"date_created":"2018-07-20T13:44:34Z","author":[{"first_name":"Tim","last_name":"Hansmeier","orcid":"0000-0003-1377-3339","full_name":"Hansmeier, Tim","id":"49992"}],"date_updated":"2022-01-06T06:59:25Z","publisher":"Universität Paderborn","title":"An FPGA Accelerator for Checking Resolution Proofs","citation":{"ieee":"T. Hansmeier, <i>An FPGA Accelerator for Checking Resolution Proofs</i>. Universität Paderborn, 2017.","chicago":"Hansmeier, Tim. <i>An FPGA Accelerator for Checking Resolution Proofs</i>. Universität Paderborn, 2017.","ama":"Hansmeier T. <i>An FPGA Accelerator for Checking Resolution Proofs</i>. Universität Paderborn; 2017.","short":"T. Hansmeier, An FPGA Accelerator for Checking Resolution Proofs, Universität Paderborn, 2017.","mla":"Hansmeier, Tim. <i>An FPGA Accelerator for Checking Resolution Proofs</i>. Universität Paderborn, 2017.","bibtex":"@book{Hansmeier_2017, title={An FPGA Accelerator for Checking Resolution Proofs}, publisher={Universität Paderborn}, author={Hansmeier, Tim}, year={2017} }","apa":"Hansmeier, T. (2017). <i>An FPGA Accelerator for Checking Resolution Proofs</i>. Universität Paderborn."},"year":"2017","department":[{"_id":"78"},{"_id":"34"},{"_id":"7"}],"user_id":"3118","_id":"3580","project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Project Area B","_id":"3"},{"_id":"12","name":"SFB 901 - Subproject B4"}],"language":[{"iso":"eng"}],"type":"bachelorsthesis","status":"public"},{"citation":{"ieee":"M.-C. Jakobs and H. Wehrheim, “Compact Proof Witnesses,” in <i>NASA Formal Methods: 9th International Symposium</i>, 2017, pp. 389–403.","chicago":"Jakobs, Marie-Christine, and Heike Wehrheim. “Compact Proof Witnesses.” In <i>NASA Formal Methods: 9th International Symposium</i>, edited by Clark Barrett, Misty Davies, and Temesghen Kahsai, 389–403. Lecture Notes in Computer Science, 2017. <a href=\"https://doi.org/10.1007/978-3-319-57288-8_28\">https://doi.org/10.1007/978-3-319-57288-8_28</a>.","ama":"Jakobs M-C, Wehrheim H. Compact Proof Witnesses. In: Barrett C, Davies M, Kahsai T, eds. <i>NASA Formal Methods: 9th International Symposium</i>. Lecture Notes in Computer Science. ; 2017:389-403. doi:<a href=\"https://doi.org/10.1007/978-3-319-57288-8_28\">10.1007/978-3-319-57288-8_28</a>","apa":"Jakobs, M.-C., &#38; Wehrheim, H. (2017). Compact Proof Witnesses. In C. Barrett, M. Davies, &#38; T. Kahsai (Eds.), <i>NASA Formal Methods: 9th International Symposium</i> (pp. 389–403). <a href=\"https://doi.org/10.1007/978-3-319-57288-8_28\">https://doi.org/10.1007/978-3-319-57288-8_28</a>","bibtex":"@inproceedings{Jakobs_Wehrheim_2017, series={Lecture Notes in Computer Science}, title={Compact Proof Witnesses}, DOI={<a href=\"https://doi.org/10.1007/978-3-319-57288-8_28\">10.1007/978-3-319-57288-8_28</a>}, booktitle={NASA Formal Methods: 9th International Symposium}, author={Jakobs, Marie-Christine and Wehrheim, Heike}, editor={Barrett, Clark and Davies, Misty and Kahsai, TemesghenEditors}, year={2017}, pages={389–403}, collection={Lecture Notes in Computer Science} }","mla":"Jakobs, Marie-Christine, and Heike Wehrheim. “Compact Proof Witnesses.” <i>NASA Formal Methods: 9th International Symposium</i>, edited by Clark Barrett et al., 2017, pp. 389–403, doi:<a href=\"https://doi.org/10.1007/978-3-319-57288-8_28\">10.1007/978-3-319-57288-8_28</a>.","short":"M.-C. Jakobs, H. Wehrheim, in: C. Barrett, M. Davies, T. Kahsai (Eds.), NASA Formal Methods: 9th International Symposium, 2017, pp. 389–403."},"page":"389-403","has_accepted_license":"1","doi":"10.1007/978-3-319-57288-8_28","author":[{"last_name":"Jakobs","full_name":"Jakobs, Marie-Christine","first_name":"Marie-Christine"},{"first_name":"Heike","last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike"}],"date_updated":"2022-01-06T06:51:00Z","status":"public","editor":[{"first_name":"Clark","last_name":"Barrett","full_name":"Barrett, Clark"},{"first_name":"Misty","full_name":"Davies, Misty","last_name":"Davies"},{"first_name":"Temesghen","full_name":"Kahsai, Temesghen","last_name":"Kahsai"}],"type":"conference","file_date_updated":"2018-03-21T13:05:02Z","user_id":"477","series_title":"Lecture Notes in Computer Science","department":[{"_id":"77"}],"project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"name":"SFB 901 - Project Area B","_id":"3"}],"_id":"114","year":"2017","title":"Compact Proof Witnesses","date_created":"2017-10-17T12:41:13Z","file":[{"date_updated":"2018-03-21T13:05:02Z","date_created":"2018-03-21T13:05:02Z","creator":"florida","file_size":492800,"access_level":"closed","file_name":"114-chp_3A10.1007_2F978-3-319-57288-8_28.pdf","file_id":"1565","content_type":"application/pdf","success":1,"relation":"main_file"}],"abstract":[{"text":"Proof witnesses are proof artifacts showing correctness of programs wrt. safety properties. The recent past has seen a rising interest in witnesses as (a) proofs in a proof-carrying-code context, (b) certificates for the correct functioning of verification tools, or simply (c) exchange formats for (partial) verification results. As witnesses in all theses scenarios need to be stored and processed, witnesses are required to be as small as possible. However, software verification tools – the prime suppliers of witnesses – do not necessarily construct small witnesses. In this paper, we present a formal account of proof witnesses. We introduce the concept of weakenings, reducing the complexity of proof witnesses while preserving the ability of witnessing safety. We develop aweakening technique for a specific class of program analyses, and prove it to be sound. Finally, we experimentally demonstrate our weakening technique to indeed achieve a size reduction of proof witnesses.","lang":"eng"}],"publication":"NASA Formal Methods: 9th International Symposium","language":[{"iso":"eng"}],"ddc":["040"]}]