[{"status":"public","type":"mastersthesis","language":[{"iso":"eng"}],"department":[{"_id":"77"}],"user_id":"15504","_id":"162","project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"citation":{"apa":"Zhang, G. (2016). <i>Program Slicing: A Way of Separating WHILE Programs into Precise and Approximate Portions</i>. Universität Paderborn.","bibtex":"@book{Zhang_2016, title={Program Slicing: A Way of Separating WHILE Programs into Precise and Approximate Portions}, publisher={Universität Paderborn}, author={Zhang, Guangli}, year={2016} }","short":"G. Zhang, Program Slicing: A Way of Separating WHILE Programs into Precise and Approximate Portions, Universität Paderborn, 2016.","mla":"Zhang, Guangli. <i>Program Slicing: A Way of Separating WHILE Programs into Precise and Approximate Portions</i>. Universität Paderborn, 2016.","ama":"Zhang G. <i>Program Slicing: A Way of Separating WHILE Programs into Precise and Approximate Portions</i>. Universität Paderborn; 2016.","chicago":"Zhang, Guangli. <i>Program Slicing: A Way of Separating WHILE Programs into Precise and Approximate Portions</i>. Universität Paderborn, 2016.","ieee":"G. Zhang, <i>Program Slicing: A Way of Separating WHILE Programs into Precise and Approximate Portions</i>. Universität Paderborn, 2016."},"year":"2016","title":"Program Slicing: A Way of Separating WHILE Programs into Precise and Approximate Portions","author":[{"full_name":"Zhang, Guangli","last_name":"Zhang","first_name":"Guangli"}],"supervisor":[{"last_name":"Wehrheim","full_name":"Wehrheim, Heike","first_name":"Heike"}],"date_created":"2017-10-17T12:41:23Z","publisher":"Universität Paderborn","date_updated":"2022-01-06T06:52:45Z"},{"author":[{"first_name":"Tobias","last_name":"Wiersema","id":"3118","full_name":"Wiersema, Tobias"},{"first_name":"Marco","id":"398","full_name":"Platzner, Marco","last_name":"Platzner"}],"date_created":"2017-10-17T12:41:17Z","date_updated":"2022-01-06T06:51:30Z","doi":"10.1109/ReCoSoC.2016.7533910","title":"Verifying Worst-Case Completion Times for Reconfigurable Hardware Modules using Proof-Carrying Hardware","has_accepted_license":"1","citation":{"short":"T. Wiersema, M. Platzner, in: Proceedings of the 11th International Symposium on Reconfigurable Communication-Centric Systems-on-Chip (ReCoSoC 2016), 2016, pp. 1--8.","mla":"Wiersema, Tobias, and Marco Platzner. “Verifying Worst-Case Completion Times for Reconfigurable Hardware Modules Using Proof-Carrying Hardware.” <i>Proceedings of the 11th International Symposium on Reconfigurable Communication-Centric Systems-on-Chip (ReCoSoC 2016)</i>, 2016, pp. 1--8, doi:<a href=\"https://doi.org/10.1109/ReCoSoC.2016.7533910\">10.1109/ReCoSoC.2016.7533910</a>.","bibtex":"@inproceedings{Wiersema_Platzner_2016, title={Verifying Worst-Case Completion Times for Reconfigurable Hardware Modules using Proof-Carrying Hardware}, DOI={<a href=\"https://doi.org/10.1109/ReCoSoC.2016.7533910\">10.1109/ReCoSoC.2016.7533910</a>}, booktitle={Proceedings of the 11th International Symposium on Reconfigurable Communication-centric Systems-on-Chip (ReCoSoC 2016)}, author={Wiersema, Tobias and Platzner, Marco}, year={2016}, pages={1--8} }","apa":"Wiersema, T., &#38; Platzner, M. (2016). Verifying Worst-Case Completion Times for Reconfigurable Hardware Modules using Proof-Carrying Hardware. In <i>Proceedings of the 11th International Symposium on Reconfigurable Communication-centric Systems-on-Chip (ReCoSoC 2016)</i> (pp. 1--8). <a href=\"https://doi.org/10.1109/ReCoSoC.2016.7533910\">https://doi.org/10.1109/ReCoSoC.2016.7533910</a>","ieee":"T. Wiersema and M. Platzner, “Verifying Worst-Case Completion Times for Reconfigurable Hardware Modules using Proof-Carrying Hardware,” in <i>Proceedings of the 11th International Symposium on Reconfigurable Communication-centric Systems-on-Chip (ReCoSoC 2016)</i>, 2016, pp. 1--8.","chicago":"Wiersema, Tobias, and Marco Platzner. “Verifying Worst-Case Completion Times for Reconfigurable Hardware Modules Using Proof-Carrying Hardware.” In <i>Proceedings of the 11th International Symposium on Reconfigurable Communication-Centric Systems-on-Chip (ReCoSoC 2016)</i>, 1--8, 2016. <a href=\"https://doi.org/10.1109/ReCoSoC.2016.7533910\">https://doi.org/10.1109/ReCoSoC.2016.7533910</a>.","ama":"Wiersema T, Platzner M. Verifying Worst-Case Completion Times for Reconfigurable Hardware Modules using Proof-Carrying Hardware. In: <i>Proceedings of the 11th International Symposium on Reconfigurable Communication-Centric Systems-on-Chip (ReCoSoC 2016)</i>. ; 2016:1--8. doi:<a href=\"https://doi.org/10.1109/ReCoSoC.2016.7533910\">10.1109/ReCoSoC.2016.7533910</a>"},"page":"1--8","year":"2016","user_id":"477","department":[{"_id":"78"}],"project":[{"_id":"1","name":"SFB 901"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"_id":"132","language":[{"iso":"eng"}],"file_date_updated":"2018-03-21T13:02:30Z","ddc":["040"],"type":"conference","publication":"Proceedings of the 11th International Symposium on Reconfigurable Communication-centric Systems-on-Chip (ReCoSoC 2016)","file":[{"creator":"florida","date_created":"2018-03-21T13:02:30Z","date_updated":"2018-03-21T13:02:30Z","access_level":"closed","file_name":"132-07533910.pdf","file_id":"1562","file_size":911171,"content_type":"application/pdf","relation":"main_file","success":1}],"status":"public","abstract":[{"lang":"eng","text":"Runtime reconfiguration can be used to replace hardware modules in the field and even to continuously improve them during operation. Runtime reconfiguration poses new challenges for validation, since the required properties of newly arriving modules may be difficult to check fast enough to sustain the intended system dynamics. In this paper we present a method for just-in-time verification of the worst-case completion time of a reconfigurable hardware module. We assume so-called run-to-completion modules that exhibit start and done signals indicating the start and end of execution, respectively. We present a formal verification approach that exploits the concept of proof-carrying hardware. The approach tasks the creator of a hardware module with constructing a proof of the worst-case completion time, which can then easily be checked by the user of the module, just prior to reconfiguration. After explaining the verification approach and a corresponding tool flow, we present results from two case studies, a short term synthesis filter and a multihead weigher. The resultsclearly show that cost of verifying the completion time of the module is paid by the creator instead of the user of the module."}]},{"publication":"Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM)","abstract":[{"text":"Before execution, users should formally validate the correctness of software received from untrusted providers. To accelerate this validation, in the proof carrying code (PCC) paradigm the provider delivers the software together with a certificate, a formal proof of the software’s correctness. Thus, the user only checks if the attached certificate shows correctness of the delivered software.Recently, we introduced configurable program certification, a generic, PCC based framework supporting various software analyses and safety properties. Evaluation of our framework revealed that validation suffers from certificate reading. In this paper, we present two orthogonal approaches which improve certificate validation, both reducing the impact of certificate reading. The first approach reduces the certificate size, storing information only if it cannot easily be recomputed. The second approach partitions the certificate into independently checkable parts. The trick is to read parts of the certificate while already checking read parts. Our experiments show that validation highly benefits from our improvements.","lang":"eng"}],"file":[{"date_updated":"2018-03-21T09:45:15Z","creator":"florida","date_created":"2018-03-21T09:45:15Z","file_size":724308,"file_id":"1489","access_level":"closed","file_name":"250-Jakobs2015.pdf","content_type":"application/pdf","success":1,"relation":"main_file"}],"ddc":["040"],"language":[{"iso":"eng"}],"year":"2015","date_created":"2017-10-17T12:41:40Z","title":"Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning","type":"conference","status":"public","project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"_id":"3","name":"SFB 901 - Project Area B"}],"_id":"250","user_id":"477","series_title":"LNCS","department":[{"_id":"77"}],"file_date_updated":"2018-03-21T09:45:15Z","has_accepted_license":"1","citation":{"chicago":"Jakobs, Marie-Christine. “Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning.” In <i>Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM)</i>, 159--174. LNCS, 2015. <a href=\"https://doi.org/10.1007/978-3-319-22969-0_12\">https://doi.org/10.1007/978-3-319-22969-0_12</a>.","ieee":"M.-C. Jakobs, “Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning,” in <i>Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM)</i>, 2015, pp. 159--174.","ama":"Jakobs M-C. Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning. In: <i>Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM)</i>. LNCS. ; 2015:159--174. doi:<a href=\"https://doi.org/10.1007/978-3-319-22969-0_12\">10.1007/978-3-319-22969-0_12</a>","apa":"Jakobs, M.-C. (2015). Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning. In <i>Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM)</i> (pp. 159--174). <a href=\"https://doi.org/10.1007/978-3-319-22969-0_12\">https://doi.org/10.1007/978-3-319-22969-0_12</a>","bibtex":"@inproceedings{Jakobs_2015, series={LNCS}, title={Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning}, DOI={<a href=\"https://doi.org/10.1007/978-3-319-22969-0_12\">10.1007/978-3-319-22969-0_12</a>}, booktitle={Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM)}, author={Jakobs, Marie-Christine}, year={2015}, pages={159--174}, collection={LNCS} }","short":"M.-C. Jakobs, in: Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM), 2015, pp. 159--174.","mla":"Jakobs, Marie-Christine. “Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning.” <i>Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM)</i>, 2015, pp. 159--174, doi:<a href=\"https://doi.org/10.1007/978-3-319-22969-0_12\">10.1007/978-3-319-22969-0_12</a>."},"page":"159--174","date_updated":"2022-01-06T06:56:43Z","author":[{"full_name":"Jakobs, Marie-Christine","last_name":"Jakobs","first_name":"Marie-Christine"}],"doi":"10.1007/978-3-319-22969-0_12"},{"_id":"283","project":[{"_id":"1","name":"SFB 901"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"department":[{"_id":"77"}],"user_id":"477","series_title":"Lecture Notes in Computer Science","ddc":["040"],"file_date_updated":"2018-03-21T09:25:36Z","language":[{"iso":"eng"}],"publication":"Fundamental Approaches to Software Engineering","type":"conference","abstract":[{"lang":"eng","text":"Today, software verification is an established analysis method which can provide high guarantees for software safety. However, the resources (time and/or memory) for an exhaustive verification are not always available, and analysis then has to resort to other techniques, like testing. Most often, the already achieved partial verification results arediscarded in this case, and testing has to start from scratch.In this paper, we propose a method for combining verification and testing in which testing only needs to check the residual fraction of an uncompleted verification. To this end, the partial results of a verification run are used to construct a residual program (and residual assertions to be checked on it). The residual program can afterwards be fed into standardtesting tools. The proposed technique is sound modulo the soundness of the testing procedure. Experimental results show that this combinedusage of verification and testing can significantly reduce the effort for the subsequent testing."}],"editor":[{"first_name":"Alexander","full_name":"Egyed, Alexander","last_name":"Egyed"},{"first_name":"Ina","last_name":"Schaefer","full_name":"Schaefer, Ina"}],"status":"public","file":[{"date_updated":"2018-03-21T09:25:36Z","creator":"florida","date_created":"2018-03-21T09:25:36Z","file_size":391253,"file_id":"1469","access_level":"closed","file_name":"283-FASEsubmission38_01.pdf","content_type":"application/pdf","success":1,"relation":"main_file"}],"date_updated":"2022-01-06T06:58:00Z","author":[{"last_name":"Czech","full_name":"Czech, Mike","first_name":"Mike"},{"full_name":"Jakobs, Marie-Christine","last_name":"Jakobs","first_name":"Marie-Christine"},{"last_name":"Wehrheim","full_name":"Wehrheim, Heike","id":"573","first_name":"Heike"}],"date_created":"2017-10-17T12:41:47Z","title":"Just test what you cannot verify!","doi":"10.1007/978-3-662-46675-9_7","has_accepted_license":"1","year":"2015","page":"100-114","citation":{"ieee":"M. Czech, M.-C. Jakobs, and H. Wehrheim, “Just test what you cannot verify!,” in <i>Fundamental Approaches to Software Engineering</i>, 2015, pp. 100–114.","chicago":"Czech, Mike, Marie-Christine Jakobs, and Heike Wehrheim. “Just Test What You Cannot Verify!” In <i>Fundamental Approaches to Software Engineering</i>, edited by Alexander Egyed and Ina Schaefer, 100–114. Lecture Notes in Computer Science, 2015. <a href=\"https://doi.org/10.1007/978-3-662-46675-9_7\">https://doi.org/10.1007/978-3-662-46675-9_7</a>.","ama":"Czech M, Jakobs M-C, Wehrheim H. Just test what you cannot verify! In: Egyed A, Schaefer I, eds. <i>Fundamental Approaches to Software Engineering</i>. Lecture Notes in Computer Science. ; 2015:100-114. doi:<a href=\"https://doi.org/10.1007/978-3-662-46675-9_7\">10.1007/978-3-662-46675-9_7</a>","apa":"Czech, M., Jakobs, M.-C., &#38; Wehrheim, H. (2015). Just test what you cannot verify! In A. Egyed &#38; I. Schaefer (Eds.), <i>Fundamental Approaches to Software Engineering</i> (pp. 100–114). <a href=\"https://doi.org/10.1007/978-3-662-46675-9_7\">https://doi.org/10.1007/978-3-662-46675-9_7</a>","mla":"Czech, Mike, et al. “Just Test What You Cannot Verify!” <i>Fundamental Approaches to Software Engineering</i>, edited by Alexander Egyed and Ina Schaefer, 2015, pp. 100–14, doi:<a href=\"https://doi.org/10.1007/978-3-662-46675-9_7\">10.1007/978-3-662-46675-9_7</a>.","short":"M. Czech, M.-C. Jakobs, H. Wehrheim, in: A. Egyed, I. Schaefer (Eds.), Fundamental Approaches to Software Engineering, 2015, pp. 100–114.","bibtex":"@inproceedings{Czech_Jakobs_Wehrheim_2015, series={Lecture Notes in Computer Science}, title={Just test what you cannot verify!}, DOI={<a href=\"https://doi.org/10.1007/978-3-662-46675-9_7\">10.1007/978-3-662-46675-9_7</a>}, booktitle={Fundamental Approaches to Software Engineering}, author={Czech, Mike and Jakobs, Marie-Christine and Wehrheim, Heike}, editor={Egyed, Alexander and Schaefer, InaEditors}, year={2015}, pages={100–114}, collection={Lecture Notes in Computer Science} }"}},{"date_updated":"2022-01-06T06:58:07Z","author":[{"first_name":"Tobias","last_name":"Isenberg","full_name":"Isenberg, Tobias"}],"date_created":"2017-10-17T12:41:47Z","title":"Incremental Inductive Verification of Parameterized Timed Systems","doi":"10.1109/ACSD.2015.13","has_accepted_license":"1","year":"2015","page":"1-9 ","citation":{"apa":"Isenberg, T. (2015). Incremental Inductive Verification of Parameterized Timed Systems. In <i>Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD)</i> (pp. 1–9). <a href=\"https://doi.org/10.1109/ACSD.2015.13\">https://doi.org/10.1109/ACSD.2015.13</a>","short":"T. Isenberg, in: Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD), 2015, pp. 1–9.","mla":"Isenberg, Tobias. “Incremental Inductive Verification of Parameterized Timed Systems.” <i>Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD)</i>, 2015, pp. 1–9, doi:<a href=\"https://doi.org/10.1109/ACSD.2015.13\">10.1109/ACSD.2015.13</a>.","bibtex":"@inproceedings{Isenberg_2015, title={Incremental Inductive Verification of Parameterized Timed Systems}, DOI={<a href=\"https://doi.org/10.1109/ACSD.2015.13\">10.1109/ACSD.2015.13</a>}, booktitle={Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD)}, author={Isenberg, Tobias}, year={2015}, pages={1–9} }","ama":"Isenberg T. Incremental Inductive Verification of Parameterized Timed Systems. In: <i>Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD)</i>. ; 2015:1-9. doi:<a href=\"https://doi.org/10.1109/ACSD.2015.13\">10.1109/ACSD.2015.13</a>","chicago":"Isenberg, Tobias. “Incremental Inductive Verification of Parameterized Timed Systems.” In <i>Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD)</i>, 1–9, 2015. <a href=\"https://doi.org/10.1109/ACSD.2015.13\">https://doi.org/10.1109/ACSD.2015.13</a>.","ieee":"T. Isenberg, “Incremental Inductive Verification of Parameterized Timed Systems,” in <i>Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD)</i>, 2015, pp. 1–9."},"_id":"285","project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"name":"SFB 901 - Project Area B","_id":"3"}],"department":[{"_id":"77"}],"user_id":"477","ddc":["040"],"file_date_updated":"2018-03-21T09:23:45Z","language":[{"iso":"eng"}],"publication":"Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD)","type":"conference","abstract":[{"text":"We propose an incremental workflow for the verification of parameterized systems modeled as symmetric networks of timed automata. Starting with a small number of timed automata in the network, a safety property is verified using IC3, a state-of-the-art algorithm based on induction.The result of the verification, an inductive strengthening, is reused proposing a candidate inductive strengthening for a larger network.If the candidate is valid, our main theorem states that the safety property holds for all sizes of the network of timed automata. Otherwise the number of automata is increased and the next iteration is started with a new run of IC3.We propose and thoroughly examine optimizations to our workflow, e.g. Feedback mechanisms to speed up the run of IC3.","lang":"eng"}],"status":"public","file":[{"content_type":"application/pdf","relation":"main_file","success":1,"date_created":"2018-03-21T09:23:45Z","creator":"florida","date_updated":"2018-03-21T09:23:45Z","file_name":"285-07352419.pdf","access_level":"closed","file_id":"1466","file_size":479808}]},{"title":"Programs from Proofs of Predicated Dataflow Analyses","doi":"10.1145/2695664.2695690","date_updated":"2022-01-06T06:57:18Z","author":[{"full_name":"Jakobs, Marie-Christine","last_name":"Jakobs","first_name":"Marie-Christine"},{"last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike","first_name":"Heike"}],"date_created":"2017-10-17T12:41:43Z","year":"2015","page":"1729-1736","citation":{"ama":"Jakobs M-C, Wehrheim H. Programs from Proofs of Predicated Dataflow Analyses. In: <i>Proceedings of the 30th Annual ACM Symposium on Applied Computing</i>. SAC ’15. ; 2015:1729-1736. doi:<a href=\"https://doi.org/10.1145/2695664.2695690\">10.1145/2695664.2695690</a>","ieee":"M.-C. Jakobs and H. Wehrheim, “Programs from Proofs of Predicated Dataflow Analyses,” in <i>Proceedings of the 30th Annual ACM Symposium on Applied Computing</i>, 2015, pp. 1729–1736.","chicago":"Jakobs, Marie-Christine, and Heike Wehrheim. “Programs from Proofs of Predicated Dataflow Analyses.” In <i>Proceedings of the 30th Annual ACM Symposium on Applied Computing</i>, 1729–36. SAC ’15, 2015. <a href=\"https://doi.org/10.1145/2695664.2695690\">https://doi.org/10.1145/2695664.2695690</a>.","bibtex":"@inproceedings{Jakobs_Wehrheim_2015, series={SAC ’15}, title={Programs from Proofs of Predicated Dataflow Analyses}, DOI={<a href=\"https://doi.org/10.1145/2695664.2695690\">10.1145/2695664.2695690</a>}, booktitle={Proceedings of the 30th Annual ACM Symposium on Applied Computing}, author={Jakobs, Marie-Christine and Wehrheim, Heike}, year={2015}, pages={1729–1736}, collection={SAC ’15} }","mla":"Jakobs, Marie-Christine, and Heike Wehrheim. “Programs from Proofs of Predicated Dataflow Analyses.” <i>Proceedings of the 30th Annual ACM Symposium on Applied Computing</i>, 2015, pp. 1729–36, doi:<a href=\"https://doi.org/10.1145/2695664.2695690\">10.1145/2695664.2695690</a>.","short":"M.-C. Jakobs, H. Wehrheim, in: Proceedings of the 30th Annual ACM Symposium on Applied Computing, 2015, pp. 1729–1736.","apa":"Jakobs, M.-C., &#38; Wehrheim, H. (2015). Programs from Proofs of Predicated Dataflow Analyses. In <i>Proceedings of the 30th Annual ACM Symposium on Applied Computing</i> (pp. 1729–1736). <a href=\"https://doi.org/10.1145/2695664.2695690\">https://doi.org/10.1145/2695664.2695690</a>"},"has_accepted_license":"1","ddc":["040"],"file_date_updated":"2018-03-21T09:35:34Z","language":[{"iso":"eng"}],"_id":"262","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"_id":"3","name":"SFB 901 - Project Area B"}],"department":[{"_id":"77"}],"user_id":"477","series_title":"SAC '15","abstract":[{"text":"Programs from Proofs\" is a generic method which generates new programs out of correctness proofs of given programs. The technique ensures that the new and given program are behaviorally equivalent and that the new program is easily verifiable, thus serving as an alternative to proof-carrying code concepts. So far, this generic method has one instantiation that verifies type-state properties of programs. In this paper, we present a whole range of new instantiations, all based on data ow analyses. More precisely, we show how an imprecise but fast data ow analysis can be enhanced with a predicate analysis as to yield a precise but expensive analysis. Out of the safety proofs of this analysis, we generate new programs, again behaviorally equivalent to the given ones, which are easily verifiable\" in the sense that now the data ow analysis alone can yield precise results. An experimental evaluation practically supports our claim of easy verification.","lang":"eng"}],"status":"public","file":[{"content_type":"application/pdf","success":1,"relation":"main_file","date_updated":"2018-03-21T09:35:34Z","creator":"florida","date_created":"2018-03-21T09:35:34Z","file_size":554583,"file_id":"1483","access_level":"closed","file_name":"262-mainSACfinal.pdf"}],"publication":"Proceedings of the 30th Annual ACM Symposium on Applied Computing","type":"conference"},{"title":"On-The-Fly Verification of Reconfigurable Image Processing Modules based on a Proof-Carrying Hardware Approach","date_created":"2017-10-17T12:41:44Z","year":"2015","language":[{"iso":"eng"}],"ddc":["040"],"file":[{"creator":"florida","date_created":"2018-03-21T09:32:42Z","date_updated":"2018-03-21T09:32:42Z","access_level":"closed","file_id":"1477","file_name":"269-paper_53.pdf","file_size":344309,"content_type":"application/pdf","relation":"main_file","success":1}],"abstract":[{"text":"Proof-carrying hardware is an approach that has recently been proposed for the efficient verification of reconfigurable modules. We present an application of proof-carrying hardware to guarantee the correct functionality of dynamically reconfigured image processing modules. Our prototype comprises a reconfigurable-system-on-chip with an embedded virtual FPGA fabric. This setup allows us to leverage open source FPGA synthesis and backend tools to produce FPGA configuration bitstreams with an open format and, thus, to demonstrate and experimentally evaluate proof-carrying hardware at the bitstream level.","lang":"eng"}],"publication":"Proceedings of the International Symposium in Reconfigurable Computing (ARC)","doi":"10.1007/978-3-319-16214-0_32","author":[{"first_name":"Tobias","id":"3118","full_name":"Wiersema, Tobias","last_name":"Wiersema"},{"full_name":"Wu, Sen","last_name":"Wu","first_name":"Sen"},{"first_name":"Marco","last_name":"Platzner","full_name":"Platzner, Marco","id":"398"}],"date_updated":"2022-01-06T06:57:30Z","page":"365--372","citation":{"ieee":"T. Wiersema, S. Wu, and M. Platzner, “On-The-Fly Verification of Reconfigurable Image Processing Modules based on a Proof-Carrying Hardware Approach,” in <i>Proceedings of the International Symposium in Reconfigurable Computing (ARC)</i>, 2015, pp. 365--372.","chicago":"Wiersema, Tobias, Sen Wu, and Marco Platzner. “On-The-Fly Verification of Reconfigurable Image Processing Modules Based on a Proof-Carrying Hardware Approach.” In <i>Proceedings of the International Symposium in Reconfigurable Computing (ARC)</i>, 365--372. LNCS, 2015. <a href=\"https://doi.org/10.1007/978-3-319-16214-0_32\">https://doi.org/10.1007/978-3-319-16214-0_32</a>.","ama":"Wiersema T, Wu S, Platzner M. On-The-Fly Verification of Reconfigurable Image Processing Modules based on a Proof-Carrying Hardware Approach. In: <i>Proceedings of the International Symposium in Reconfigurable Computing (ARC)</i>. LNCS. ; 2015:365--372. doi:<a href=\"https://doi.org/10.1007/978-3-319-16214-0_32\">10.1007/978-3-319-16214-0_32</a>","apa":"Wiersema, T., Wu, S., &#38; Platzner, M. (2015). On-The-Fly Verification of Reconfigurable Image Processing Modules based on a Proof-Carrying Hardware Approach. In <i>Proceedings of the International Symposium in Reconfigurable Computing (ARC)</i> (pp. 365--372). <a href=\"https://doi.org/10.1007/978-3-319-16214-0_32\">https://doi.org/10.1007/978-3-319-16214-0_32</a>","bibtex":"@inproceedings{Wiersema_Wu_Platzner_2015, series={LNCS}, title={On-The-Fly Verification of Reconfigurable Image Processing Modules based on a Proof-Carrying Hardware Approach}, DOI={<a href=\"https://doi.org/10.1007/978-3-319-16214-0_32\">10.1007/978-3-319-16214-0_32</a>}, booktitle={Proceedings of the International Symposium in Reconfigurable Computing (ARC)}, author={Wiersema, Tobias and Wu, Sen and Platzner, Marco}, year={2015}, pages={365--372}, collection={LNCS} }","short":"T. Wiersema, S. Wu, M. Platzner, in: Proceedings of the International Symposium in Reconfigurable Computing (ARC), 2015, pp. 365--372.","mla":"Wiersema, Tobias, et al. “On-The-Fly Verification of Reconfigurable Image Processing Modules Based on a Proof-Carrying Hardware Approach.” <i>Proceedings of the International Symposium in Reconfigurable Computing (ARC)</i>, 2015, pp. 365--372, doi:<a href=\"https://doi.org/10.1007/978-3-319-16214-0_32\">10.1007/978-3-319-16214-0_32</a>."},"has_accepted_license":"1","file_date_updated":"2018-03-21T09:32:42Z","department":[{"_id":"78"}],"user_id":"477","series_title":"LNCS","_id":"269","project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"status":"public","type":"conference"},{"publication":"2015 International Conference on Software Engineering (ICSE)","type":"conference","status":"public","file":[{"success":1,"relation":"main_file","content_type":"application/pdf","file_size":206378,"access_level":"closed","file_name":"lbb+15iccta.pdf","file_id":"5263","date_updated":"2018-11-02T14:10:22Z","creator":"ups","date_created":"2018-11-02T14:10:22Z"}],"department":[{"_id":"76"}],"user_id":"477","_id":"5207","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Project Area B","_id":"3"},{"name":"SFB 901 - Subproject B4","_id":"12"}],"language":[{"iso":"eng"}],"file_date_updated":"2018-11-02T14:10:22Z","extern":"1","keyword":["CROSSING","ATTRACT","ITSECWEBSITE"],"ddc":["000"],"has_accepted_license":"1","publication_identifier":{"isbn":["978-1-4799-1934-5"]},"page":"280-291","citation":{"ama":"Li L, Bartel A, Bissyande TF, et al. IccTA: Detecting Inter-Component Privacy Leaks in Android Apps. In: <i>2015 International Conference on Software Engineering (ICSE)</i>. ; 2015:280-291.","chicago":"Li, Li, Alexandre Bartel, Tegawende F. Bissyande, Jacques Klein, Yves Le Traon, Steven Arzt, Siegfried Rasthofer, Eric Bodden, Damien Octeau, and Patrick McDaniel. “IccTA: Detecting Inter-Component Privacy Leaks in Android Apps.” In <i>2015 International Conference on Software Engineering (ICSE)</i>, 280–91, 2015.","ieee":"L. Li <i>et al.</i>, “IccTA: Detecting Inter-Component Privacy Leaks in Android Apps,” in <i>2015 International Conference on Software Engineering (ICSE)</i>, 2015, pp. 280–291.","bibtex":"@inproceedings{Li_Bartel_Bissyande_Klein_Le Traon_Arzt_Rasthofer_Bodden_Octeau_McDaniel_2015, title={IccTA: Detecting Inter-Component Privacy Leaks in Android Apps}, booktitle={2015 International Conference on Software Engineering (ICSE)}, author={Li, Li and Bartel, Alexandre and Bissyande, Tegawende F. and Klein, Jacques and Le Traon, Yves and Arzt, Steven and Rasthofer, Siegfried and Bodden, Eric and Octeau, Damien and McDaniel, Patrick}, year={2015}, pages={280–291} }","short":"L. Li, A. Bartel, T.F. Bissyande, J. Klein, Y. Le Traon, S. Arzt, S. Rasthofer, E. Bodden, D. Octeau, P. McDaniel, in: 2015 International Conference on Software Engineering (ICSE), 2015, pp. 280–291.","mla":"Li, Li, et al. “IccTA: Detecting Inter-Component Privacy Leaks in Android Apps.” <i>2015 International Conference on Software Engineering (ICSE)</i>, 2015, pp. 280–91.","apa":"Li, L., Bartel, A., Bissyande, T. F., Klein, J., Le Traon, Y., Arzt, S., … McDaniel, P. (2015). IccTA: Detecting Inter-Component Privacy Leaks in Android Apps. In <i>2015 International Conference on Software Engineering (ICSE)</i> (pp. 280–291)."},"year":"2015","author":[{"last_name":"Li","full_name":"Li, Li","first_name":"Li"},{"first_name":"Alexandre","last_name":"Bartel","full_name":"Bartel, Alexandre"},{"first_name":"Tegawende F.","last_name":"Bissyande","full_name":"Bissyande, Tegawende F."},{"first_name":"Jacques","full_name":"Klein, Jacques","last_name":"Klein"},{"last_name":"Le Traon","full_name":"Le Traon, Yves","first_name":"Yves"},{"first_name":"Steven","last_name":"Arzt","full_name":"Arzt, Steven"},{"first_name":"Siegfried","last_name":"Rasthofer","full_name":"Rasthofer, Siegfried"},{"first_name":"Eric","id":"59256","full_name":"Bodden, Eric","last_name":"Bodden","orcid":"0000-0003-3470-3647"},{"first_name":"Damien","full_name":"Octeau, Damien","last_name":"Octeau"},{"last_name":"McDaniel","full_name":"McDaniel, Patrick","first_name":"Patrick"}],"date_created":"2018-10-31T12:59:44Z","date_updated":"2022-01-06T07:01:46Z","main_file_link":[{"url":"http://www.bodden.de/pubs/lbb+15iccta.pdf"}],"title":"IccTA: Detecting Inter-Component Privacy Leaks in Android Apps"},{"title":"Konzept und Implementation einer Benutzeroberfläche zur Generierung virtueller FPGAs","author":[{"last_name":"Meißner","full_name":"Meißner, Roland","first_name":"Roland"}],"supervisor":[{"first_name":"Tobias","last_name":"Wiersema","full_name":"Wiersema, Tobias","id":"3118"}],"date_created":"2019-07-10T11:48:25Z","date_updated":"2022-01-06T06:50:50Z","publisher":"Universität Paderborn","citation":{"chicago":"Meißner, Roland. <i>Konzept Und Implementation Einer Benutzeroberfläche Zur Generierung Virtueller FPGAs</i>. Universität Paderborn, 2015.","ieee":"R. Meißner, <i>Konzept und Implementation einer Benutzeroberfläche zur Generierung virtueller FPGAs</i>. Universität Paderborn, 2015.","ama":"Meißner R. <i>Konzept Und Implementation Einer Benutzeroberfläche Zur Generierung Virtueller FPGAs</i>. Universität Paderborn; 2015.","mla":"Meißner, Roland. <i>Konzept Und Implementation Einer Benutzeroberfläche Zur Generierung Virtueller FPGAs</i>. Universität Paderborn, 2015.","bibtex":"@book{Meißner_2015, title={Konzept und Implementation einer Benutzeroberfläche zur Generierung virtueller FPGAs}, publisher={Universität Paderborn}, author={Meißner, Roland}, year={2015} }","short":"R. Meißner, Konzept Und Implementation Einer Benutzeroberfläche Zur Generierung Virtueller FPGAs, Universität Paderborn, 2015.","apa":"Meißner, R. (2015). <i>Konzept und Implementation einer Benutzeroberfläche zur Generierung virtueller FPGAs</i>. Universität Paderborn."},"year":"2015","language":[{"iso":"eng"}],"user_id":"477","department":[{"_id":"78"}],"project":[{"name":"SFB 901 - Subproject B4","_id":"12"},{"_id":"1","name":"SFB 901"},{"_id":"3","name":"SFB 901 - Project Area B"}],"_id":"10714","status":"public","type":"bachelorsthesis"},{"title":"Webcam application using virtual FPGA","date_created":"2017-10-17T12:41:56Z","author":[{"first_name":"Sen","full_name":"Wu, Sen","last_name":"Wu"}],"user_id":"477","_id":"331","date_updated":"2022-01-06T06:59:10Z","publisher":"Universität Paderborn","project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"status":"public","citation":{"apa":"Wu, S. (2014). <i>Webcam application using virtual FPGA</i>. Universität Paderborn.","mla":"Wu, Sen. <i>Webcam Application Using Virtual FPGA</i>. Universität Paderborn, 2014.","bibtex":"@book{Wu_2014, title={Webcam application using virtual FPGA}, publisher={Universität Paderborn}, author={Wu, Sen}, year={2014} }","short":"S. Wu, Webcam Application Using Virtual FPGA, Universität Paderborn, 2014.","ama":"Wu S. <i>Webcam Application Using Virtual FPGA</i>. Universität Paderborn; 2014.","ieee":"S. Wu, <i>Webcam application using virtual FPGA</i>. Universität Paderborn, 2014.","chicago":"Wu, Sen. <i>Webcam Application Using Virtual FPGA</i>. Universität Paderborn, 2014."},"year":"2014","type":"bachelorsthesis"},{"citation":{"apa":"Korth, P. (2014). <i>Untersuchung transitiver Eigenschaften der Technik “Programs from Proofs.”</i> Universität Paderborn.","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. <i>Untersuchung transitiver Eigenschaften der Technik “Programs from Proofs.”</i> Universität Paderborn, 2014.","ama":"Korth P. <i>Untersuchung transitiver Eigenschaften der Technik “Programs from Proofs.”</i> Universität Paderborn; 2014.","chicago":"Korth, Philipp. <i>Untersuchung transitiver Eigenschaften der Technik “Programs from Proofs.”</i> Universität Paderborn, 2014.","ieee":"P. Korth, <i>Untersuchung transitiver Eigenschaften der Technik “Programs from Proofs.”</i> Universität Paderborn, 2014."},"year":"2014","title":"Untersuchung transitiver Eigenschaften der Technik \"Programs from Proofs\"","author":[{"first_name":"Philipp","full_name":"Korth, Philipp","last_name":"Korth"}],"date_created":"2017-10-17T12:41:58Z","supervisor":[{"first_name":"Heike","last_name":"Wehrheim","full_name":"Wehrheim, Heike"}],"date_updated":"2022-01-06T06:59:14Z","publisher":"Universität Paderborn","status":"public","type":"bachelorsthesis","language":[{"iso":"ger"}],"user_id":"15504","department":[{"_id":"77"}],"project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"name":"SFB 901 - Project Area B","_id":"3"}],"_id":"340"},{"year":"2014","citation":{"bibtex":"@book{Klauke_2014, title={Transformation graphischer Protokollspezifikationen in Model-Checker-Anfragen}, publisher={Universität Paderborn}, author={Klauke, Christoph}, year={2014} }","mla":"Klauke, Christoph. <i>Transformation Graphischer Protokollspezifikationen in Model-Checker-Anfragen</i>. Universität Paderborn, 2014.","short":"C. Klauke, Transformation Graphischer Protokollspezifikationen in Model-Checker-Anfragen, Universität Paderborn, 2014.","apa":"Klauke, C. (2014). <i>Transformation graphischer Protokollspezifikationen in Model-Checker-Anfragen</i>. Universität Paderborn.","ama":"Klauke C. <i>Transformation Graphischer Protokollspezifikationen in Model-Checker-Anfragen</i>. Universität Paderborn; 2014.","chicago":"Klauke, Christoph. <i>Transformation Graphischer Protokollspezifikationen in Model-Checker-Anfragen</i>. Universität Paderborn, 2014.","ieee":"C. Klauke, <i>Transformation graphischer Protokollspezifikationen in Model-Checker-Anfragen</i>. Universität Paderborn, 2014."},"date_updated":"2022-01-06T06:59:15Z","publisher":"Universität Paderborn","date_created":"2017-10-17T12:41:58Z","author":[{"first_name":"Christoph","full_name":"Klauke, Christoph","last_name":"Klauke"}],"title":"Transformation graphischer Protokollspezifikationen in Model-Checker-Anfragen","type":"bachelorsthesis","status":"public","_id":"342","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"name":"SFB 901 - Project Area B","_id":"3"}],"user_id":"477"},{"publication":"Proceedings of the Software Engineering Conference (SE)","file":[{"date_created":"2018-03-20T07:04:52Z","creator":"florida","date_updated":"2018-03-20T07:04:52Z","file_name":"383-programmsFromProofsSE.pdf","access_level":"closed","file_id":"1392","file_size":66474,"content_type":"application/pdf","relation":"main_file","success":1}],"abstract":[{"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.","lang":"eng"}],"language":[{"iso":"eng"}],"ddc":["040"],"year":"2014","date_created":"2017-10-17T12:42:06Z","title":"Programs from Proofs -- Approach and Applications","type":"conference","status":"public","department":[{"_id":"77"}],"series_title":"Lecture Notes in Informatics (LNI)","user_id":"477","_id":"383","project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"file_date_updated":"2018-03-20T07:04:52Z","has_accepted_license":"1","page":"67-68","citation":{"ieee":"D. Wonisch, A. Schremmer, and H. Wehrheim, “Programs from Proofs -- Approach and Applications,” in <i>Proceedings of the Software Engineering Conference (SE)</i>, 2014, pp. 67–68.","chicago":"Wonisch, Daniel, Alexander Schremmer, and Heike Wehrheim. “Programs from Proofs -- Approach and Applications.” In <i>Proceedings of the Software Engineering Conference (SE)</i>, 67–68. Lecture Notes in Informatics (LNI), 2014.","ama":"Wonisch D, Schremmer A, Wehrheim H. Programs from Proofs -- Approach and Applications. In: <i>Proceedings of the Software Engineering Conference (SE)</i>. Lecture Notes in Informatics (LNI). ; 2014:67-68.","mla":"Wonisch, Daniel, et al. “Programs from Proofs -- Approach and Applications.” <i>Proceedings of the Software Engineering Conference (SE)</i>, 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.","apa":"Wonisch, D., Schremmer, A., &#38; Wehrheim, H. (2014). Programs from Proofs -- Approach and Applications. In <i>Proceedings of the Software Engineering Conference (SE)</i> (pp. 67–68)."},"author":[{"first_name":"Daniel","full_name":"Wonisch, Daniel","last_name":"Wonisch"},{"full_name":"Schremmer, Alexander","last_name":"Schremmer","first_name":"Alexander"},{"first_name":"Heike","id":"573","full_name":"Wehrheim, Heike","last_name":"Wehrheim"}],"date_updated":"2022-01-06T06:59:38Z","main_file_link":[{"url":"http://eprints.uni-kiel.de/23752/"}]},{"citation":{"bibtex":"@inproceedings{Jakobs_Wehrheim_2014, series={SPIN 2014}, title={Certification for Configurable Program Analysis}, DOI={<a href=\"https://doi.org/10.1145/2632362.2632372\">10.1145/2632362.2632372</a>}, 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} }","short":"M.-C. Jakobs, H. Wehrheim, in: Proceedings of the 21st International Symposium on Model Checking of Software (SPIN), 2014, pp. 30–39.","mla":"Jakobs, Marie-Christine, and Heike Wehrheim. “Certification for Configurable Program Analysis.” <i>Proceedings of the 21st International Symposium on Model Checking of Software (SPIN)</i>, 2014, pp. 30–39, doi:<a href=\"https://doi.org/10.1145/2632362.2632372\">10.1145/2632362.2632372</a>.","apa":"Jakobs, M.-C., &#38; Wehrheim, H. (2014). Certification for Configurable Program Analysis. In <i>Proceedings of the 21st International Symposium on Model Checking of Software (SPIN)</i> (pp. 30–39). <a href=\"https://doi.org/10.1145/2632362.2632372\">https://doi.org/10.1145/2632362.2632372</a>","ama":"Jakobs M-C, Wehrheim H. Certification for Configurable Program Analysis. In: <i>Proceedings of the 21st International Symposium on Model Checking of Software (SPIN)</i>. SPIN 2014. ; 2014:30-39. doi:<a href=\"https://doi.org/10.1145/2632362.2632372\">10.1145/2632362.2632372</a>","chicago":"Jakobs, Marie-Christine, and Heike Wehrheim. “Certification for Configurable Program Analysis.” In <i>Proceedings of the 21st International Symposium on Model Checking of Software (SPIN)</i>, 30–39. SPIN 2014, 2014. <a href=\"https://doi.org/10.1145/2632362.2632372\">https://doi.org/10.1145/2632362.2632372</a>.","ieee":"M.-C. Jakobs and H. Wehrheim, “Certification for Configurable Program Analysis,” in <i>Proceedings of the 21st International Symposium on Model Checking of Software (SPIN)</i>, 2014, pp. 30–39."},"page":"30-39","year":"2014","has_accepted_license":"1","doi":"10.1145/2632362.2632372","title":"Certification for Configurable Program Analysis","date_created":"2017-10-17T12:42:19Z","author":[{"last_name":"Jakobs","full_name":"Jakobs, Marie-Christine","first_name":"Marie-Christine"},{"id":"573","full_name":"Wehrheim, Heike","last_name":"Wehrheim","first_name":"Heike"}],"date_updated":"2022-01-06T07:01:07Z","file":[{"content_type":"application/pdf","relation":"main_file","success":1,"date_created":"2018-03-16T11:25:35Z","creator":"florida","date_updated":"2018-03-16T11:25:35Z","access_level":"closed","file_name":"450-p30-jakobs.pdf","file_id":"1345","file_size":487366}],"status":"public","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. "}],"type":"conference","publication":"Proceedings of the 21st International Symposium on Model Checking of Software (SPIN)","file_date_updated":"2018-03-16T11:25:35Z","language":[{"iso":"eng"}],"ddc":["040"],"user_id":"477","series_title":"SPIN 2014","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":"450"},{"has_accepted_license":"1","page":"167-174","citation":{"ieee":"T. Wiersema, S. Drzevitzky, and M. Platzner, “Memory Security in Reconfigurable Computers: Combining Formal Verification with Monitoring,” in <i>Proceedings of the International Conference on Field-Programmable Technology (FPT)</i>, 2014, pp. 167–174.","chicago":"Wiersema, Tobias, Stephanie Drzevitzky, and Marco Platzner. “Memory Security in Reconfigurable Computers: Combining Formal Verification with Monitoring.” In <i>Proceedings of the International Conference on Field-Programmable Technology (FPT)</i>, 167–74, 2014. <a href=\"https://doi.org/10.1109/FPT.2014.7082771\">https://doi.org/10.1109/FPT.2014.7082771</a>.","ama":"Wiersema T, Drzevitzky S, Platzner M. Memory Security in Reconfigurable Computers: Combining Formal Verification with Monitoring. In: <i>Proceedings of the International Conference on Field-Programmable Technology (FPT)</i>. ; 2014:167-174. doi:<a href=\"https://doi.org/10.1109/FPT.2014.7082771\">10.1109/FPT.2014.7082771</a>","short":"T. Wiersema, S. Drzevitzky, M. Platzner, in: Proceedings of the International Conference on Field-Programmable Technology (FPT), 2014, pp. 167–174.","bibtex":"@inproceedings{Wiersema_Drzevitzky_Platzner_2014, title={Memory Security in Reconfigurable Computers: Combining Formal Verification with Monitoring}, DOI={<a href=\"https://doi.org/10.1109/FPT.2014.7082771\">10.1109/FPT.2014.7082771</a>}, booktitle={Proceedings of the International Conference on Field-Programmable Technology (FPT)}, author={Wiersema, Tobias and Drzevitzky, Stephanie and Platzner, Marco}, year={2014}, pages={167–174} }","mla":"Wiersema, Tobias, et al. “Memory Security in Reconfigurable Computers: Combining Formal Verification with Monitoring.” <i>Proceedings of the International Conference on Field-Programmable Technology (FPT)</i>, 2014, pp. 167–74, doi:<a href=\"https://doi.org/10.1109/FPT.2014.7082771\">10.1109/FPT.2014.7082771</a>.","apa":"Wiersema, T., Drzevitzky, S., &#38; Platzner, M. (2014). Memory Security in Reconfigurable Computers: Combining Formal Verification with Monitoring. In <i>Proceedings of the International Conference on Field-Programmable Technology (FPT)</i> (pp. 167–174). <a href=\"https://doi.org/10.1109/FPT.2014.7082771\">https://doi.org/10.1109/FPT.2014.7082771</a>"},"year":"2014","author":[{"first_name":"Tobias","last_name":"Wiersema","id":"3118","full_name":"Wiersema, Tobias"},{"first_name":"Stephanie","last_name":"Drzevitzky","full_name":"Drzevitzky, Stephanie"},{"full_name":"Platzner, Marco","id":"398","last_name":"Platzner","first_name":"Marco"}],"date_created":"2017-10-17T12:42:09Z","date_updated":"2022-01-06T07:00:05Z","doi":"10.1109/FPT.2014.7082771","title":"Memory Security in Reconfigurable Computers: Combining Formal Verification with Monitoring","publication":"Proceedings of the International Conference on Field-Programmable Technology (FPT)","type":"conference","status":"public","file":[{"file_size":404328,"file_name":"399-wiersema14_fpt_IEEE_approved.pdf","file_id":"1380","access_level":"closed","date_updated":"2018-03-20T06:57:44Z","date_created":"2018-03-20T06:57:44Z","creator":"florida","success":1,"relation":"main_file","content_type":"application/pdf"}],"abstract":[{"text":"Ensuring memory access security is a challenge for reconfigurable systems with multiple cores. Previous work introduced access monitors attached to the memory subsystem to ensure that the cores adhere to pre-defined protocols when accessing memory. In this paper, we combine access monitors with a formal runtime verification technique known as proof-carrying hardware to guarantee memory security. We extend previous work on proof-carrying hardware by covering sequential circuits and demonstrate our approach with a prototype leveraging ReconOS/Zynq with an embedded ZUMA virtual FPGA overlay. Experiments show the feasibility of the approach and the capabilities of the prototype, which constitutes the first realization of proof-carrying hardware on real FPGAs. The area overheads for the virtual FPGA are measured as 2x-10x, depending on the resource type. The delay overhead is substantial with almost 100x, but this is an extremely pessimistic estimate that will be lowered once accurate timing analysis for FPGA overlays become available. Finally, reconfiguration time for the virtual FPGA is about one order of magnitude lower than for the native Zynq fabric.","lang":"eng"}],"department":[{"_id":"78"}],"user_id":"477","_id":"399","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"name":"SFB 901 - Project Area B","_id":"3"}],"language":[{"iso":"eng"}],"file_date_updated":"2018-03-20T06:57:44Z","ddc":["040"]},{"file_date_updated":"2018-03-16T11:35:28Z","language":[{"iso":"eng"}],"ddc":["040"],"department":[{"_id":"77"},{"_id":"78"}],"user_id":"477","series_title":"LNCS","_id":"408","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"name":"SFB 901 - Project Area B","_id":"3"}],"status":"public","file":[{"date_created":"2018-03-16T11:35:28Z","creator":"florida","date_updated":"2018-03-16T11:35:28Z","file_id":"1364","access_level":"closed","file_name":"408-jakobs14_ifm.pdf","file_size":561325,"content_type":"application/pdf","relation":"main_file","success":1}],"abstract":[{"text":"Verification of hardware and software usually proceeds separately, software analysis relying on the correctness of processors executing instructions. This assumption is valid as long as the software runs on standard CPUs that have been extensively validated and are in wide use. However, for processors exploiting custom instruction set extensions to meet performance and energy constraints the validation might be less extensive, challenging the correctness assumption.In this paper we present an approach for integrating software analyses with hardware verification, specifically targeting custom instruction set extensions. We propose three different techniques for deriving the properties to be proven for the hardware implementation of a custom instruction in order to support software analyses. The techniques are designed to explore the trade-off between generality and efficiency and span from proving functional equivalence over checking the rules of a particular analysis domain to verifying actual pre and post conditions resulting from program analysis. We demonstrate and compare the three techniques on example programs with custom instructions, using stateof-the-art software and hardware verification techniques.","lang":"eng"}],"editor":[{"last_name":"Albert","full_name":"Albert, Elvira","first_name":"Elvira"},{"last_name":"Sekerinski","full_name":"Sekerinski, Emil","first_name":"Emil"}],"publication":"Proceedings of the 11th International Conference on Integrated Formal Methods (iFM)","type":"conference","doi":"10.1007/978-3-319-10181-1_19","title":"Integrating Software and Hardware Verification","date_created":"2017-10-17T12:42:11Z","author":[{"first_name":"Marie-Christine","last_name":"Jakobs","full_name":"Jakobs, Marie-Christine"},{"first_name":"Marco","full_name":"Platzner, Marco","id":"398","last_name":"Platzner"},{"first_name":"Tobias","last_name":"Wiersema","id":"3118","full_name":"Wiersema, Tobias"},{"last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike","first_name":"Heike"}],"date_updated":"2022-01-06T07:00:14Z","page":"307-322","citation":{"short":"M.-C. Jakobs, M. Platzner, T. Wiersema, H. Wehrheim, in: E. Albert, E. Sekerinski (Eds.), Proceedings of the 11th International Conference on Integrated Formal Methods (IFM), 2014, pp. 307–322.","bibtex":"@inproceedings{Jakobs_Platzner_Wiersema_Wehrheim_2014, series={LNCS}, title={Integrating Software and Hardware Verification}, DOI={<a href=\"https://doi.org/10.1007/978-3-319-10181-1_19\">10.1007/978-3-319-10181-1_19</a>}, booktitle={Proceedings of the 11th International Conference on Integrated Formal Methods (iFM)}, author={Jakobs, Marie-Christine and Platzner, Marco and Wiersema, Tobias and Wehrheim, Heike}, editor={Albert, Elvira and Sekerinski, EmilEditors}, year={2014}, pages={307–322}, collection={LNCS} }","mla":"Jakobs, Marie-Christine, et al. “Integrating Software and Hardware Verification.” <i>Proceedings of the 11th International Conference on Integrated Formal Methods (IFM)</i>, edited by Elvira Albert and Emil Sekerinski, 2014, pp. 307–22, doi:<a href=\"https://doi.org/10.1007/978-3-319-10181-1_19\">10.1007/978-3-319-10181-1_19</a>.","apa":"Jakobs, M.-C., Platzner, M., Wiersema, T., &#38; Wehrheim, H. (2014). Integrating Software and Hardware Verification. In E. Albert &#38; E. Sekerinski (Eds.), <i>Proceedings of the 11th International Conference on Integrated Formal Methods (iFM)</i> (pp. 307–322). <a href=\"https://doi.org/10.1007/978-3-319-10181-1_19\">https://doi.org/10.1007/978-3-319-10181-1_19</a>","ama":"Jakobs M-C, Platzner M, Wiersema T, Wehrheim H. Integrating Software and Hardware Verification. In: Albert E, Sekerinski E, eds. <i>Proceedings of the 11th International Conference on Integrated Formal Methods (IFM)</i>. LNCS. ; 2014:307-322. doi:<a href=\"https://doi.org/10.1007/978-3-319-10181-1_19\">10.1007/978-3-319-10181-1_19</a>","chicago":"Jakobs, Marie-Christine, Marco Platzner, Tobias Wiersema, and Heike Wehrheim. “Integrating Software and Hardware Verification.” In <i>Proceedings of the 11th International Conference on Integrated Formal Methods (IFM)</i>, edited by Elvira Albert and Emil Sekerinski, 307–22. LNCS, 2014. <a href=\"https://doi.org/10.1007/978-3-319-10181-1_19\">https://doi.org/10.1007/978-3-319-10181-1_19</a>.","ieee":"M.-C. Jakobs, M. Platzner, T. Wiersema, and H. Wehrheim, “Integrating Software and Hardware Verification,” in <i>Proceedings of the 11th International Conference on Integrated Formal Methods (iFM)</i>, 2014, pp. 307–322."},"year":"2014","has_accepted_license":"1"},{"date_created":"2017-10-17T12:42:13Z","supervisor":[{"last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike","first_name":"Heike"}],"author":[{"first_name":"Felix","id":"22398","full_name":"Pauck, Felix","last_name":"Pauck"}],"date_updated":"2022-01-06T07:00:30Z","publisher":"Universität Paderborn","oa":"1","title":"Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren","has_accepted_license":"1","citation":{"apa":"Pauck, F. (2014). <i>Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren</i>. Universität Paderborn.","bibtex":"@book{Pauck_2014, title={Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren}, publisher={Universität Paderborn}, author={Pauck, Felix}, year={2014} }","mla":"Pauck, Felix. <i>Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren</i>. Universität Paderborn, 2014.","short":"F. Pauck, Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren, Universität Paderborn, 2014.","ieee":"F. Pauck, <i>Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren</i>. Universität Paderborn, 2014.","chicago":"Pauck, Felix. <i>Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren</i>. Universität Paderborn, 2014.","ama":"Pauck F. <i>Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren</i>. Universität Paderborn; 2014."},"year":"2014","user_id":"22398","department":[{"_id":"77"}],"project":[{"_id":"1","name":"SFB 901"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"name":"SFB 901 - Project Area B","_id":"3"}],"_id":"418","file_date_updated":"2019-08-07T09:05:38Z","language":[{"iso":"ger"}],"ddc":["000"],"type":"bachelorsthesis","file":[{"content_type":"application/pdf","relation":"main_file","creator":"fpauck","date_created":"2019-08-07T09:00:20Z","date_updated":"2019-08-07T09:05:38Z","file_name":"fpauck_2014.pdf","access_level":"open_access","file_id":"12906","title":"Bachelorarbeit","file_size":3191756}],"status":"public"},{"has_accepted_license":"1","citation":{"apa":"Wiersema, T., Bockhorn, A., &#38; Platzner, M. (2014). Embedding FPGA Overlays into Configurable Systems-on-Chip: ReconOS meets ZUMA. In <i>Proceedings of the International Conference on ReConFigurable Computing and FPGAs (ReConFig)</i> (pp. 1–6). <a href=\"https://doi.org/10.1109/ReConFig.2014.7032514\">https://doi.org/10.1109/ReConFig.2014.7032514</a>","mla":"Wiersema, Tobias, et al. “Embedding FPGA Overlays into Configurable Systems-on-Chip: ReconOS Meets ZUMA.” <i>Proceedings of the International Conference on ReConFigurable Computing and FPGAs (ReConFig)</i>, 2014, pp. 1–6, doi:<a href=\"https://doi.org/10.1109/ReConFig.2014.7032514\">10.1109/ReConFig.2014.7032514</a>.","short":"T. Wiersema, A. Bockhorn, M. Platzner, in: Proceedings of the International Conference on ReConFigurable Computing and FPGAs (ReConFig), 2014, pp. 1–6.","bibtex":"@inproceedings{Wiersema_Bockhorn_Platzner_2014, title={Embedding FPGA Overlays into Configurable Systems-on-Chip: ReconOS meets ZUMA}, DOI={<a href=\"https://doi.org/10.1109/ReConFig.2014.7032514\">10.1109/ReConFig.2014.7032514</a>}, booktitle={Proceedings of the International Conference on ReConFigurable Computing and FPGAs (ReConFig)}, author={Wiersema, Tobias and Bockhorn, Arne and Platzner, Marco}, year={2014}, pages={1–6} }","ieee":"T. Wiersema, A. Bockhorn, and M. Platzner, “Embedding FPGA Overlays into Configurable Systems-on-Chip: ReconOS meets ZUMA,” in <i>Proceedings of the International Conference on ReConFigurable Computing and FPGAs (ReConFig)</i>, 2014, pp. 1–6.","chicago":"Wiersema, Tobias, Arne Bockhorn, and Marco Platzner. “Embedding FPGA Overlays into Configurable Systems-on-Chip: ReconOS Meets ZUMA.” In <i>Proceedings of the International Conference on ReConFigurable Computing and FPGAs (ReConFig)</i>, 1–6, 2014. <a href=\"https://doi.org/10.1109/ReConFig.2014.7032514\">https://doi.org/10.1109/ReConFig.2014.7032514</a>.","ama":"Wiersema T, Bockhorn A, Platzner M. Embedding FPGA Overlays into Configurable Systems-on-Chip: ReconOS meets ZUMA. In: <i>Proceedings of the International Conference on ReConFigurable Computing and FPGAs (ReConFig)</i>. ; 2014:1-6. doi:<a href=\"https://doi.org/10.1109/ReConFig.2014.7032514\">10.1109/ReConFig.2014.7032514</a>"},"page":"1-6 ","year":"2014","date_created":"2017-10-17T12:42:16Z","author":[{"last_name":"Wiersema","id":"3118","full_name":"Wiersema, Tobias","first_name":"Tobias"},{"first_name":"Arne","last_name":"Bockhorn","full_name":"Bockhorn, Arne"},{"first_name":"Marco","last_name":"Platzner","id":"398","full_name":"Platzner, Marco"}],"date_updated":"2022-01-06T07:00:56Z","doi":"10.1109/ReConFig.2014.7032514","title":"Embedding FPGA Overlays into Configurable Systems-on-Chip: ReconOS meets ZUMA","type":"conference","publication":"Proceedings of the International Conference on ReConFigurable Computing and FPGAs (ReConFig)","file":[{"creator":"florida","date_created":"2018-03-16T11:30:58Z","date_updated":"2018-03-16T11:30:58Z","file_name":"433-wiersema14_reconfig_IEEE_approved.pdf","file_id":"1355","access_level":"closed","file_size":369333,"content_type":"application/pdf","relation":"main_file","success":1}],"status":"public","abstract":[{"lang":"eng","text":"Virtual FPGAs are overlay architectures realized on top of physical FPGAs. They are proposed to enhance or abstract away from the physical FPGA for experimenting with novel architectures and design tool flows. In this paper, we present an embedding of a ZUMA-based virtual FPGA fabric into a complete configurable system-on-chip. Such an embedding is required to fully harness the potential of virtual FPGAs, in particular to give the virtual circuits access to main memory and operating system services, and to enable a concurrent operation of virtualized and non-virtualized circuitry. We discuss our extension to ZUMA and its embedding into the ReconOS operating system for hardware/software systems. Furthermore, we present an open source tool flow to synthesize configurations for the virtual FPGA."}],"user_id":"477","department":[{"_id":"78"}],"project":[{"_id":"1","name":"SFB 901"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"_id":"433","language":[{"iso":"eng"}],"file_date_updated":"2018-03-16T11:30:58Z","ddc":["040"]},{"publication":"Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI '14","file":[{"relation":"main_file","success":1,"content_type":"application/pdf","file_id":"5258","file_name":"p259-arzt.pdf","access_level":"closed","file_size":406920,"creator":"ups","date_created":"2018-11-02T13:59:33Z","date_updated":"2018-11-02T13:59:33Z"}],"language":[{"iso":"eng"}],"ddc":["000"],"year":"2014","date_created":"2018-10-31T10:55:28Z","publisher":"ACM Press","title":"FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware Taint Analysis for Android Apps","type":"conference","status":"public","department":[{"_id":"76"}],"user_id":"477","_id":"5189","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Project Area B","_id":"3"},{"_id":"12","name":"SFB 901 - Subproject B4"}],"extern":"1","file_date_updated":"2018-11-02T13:59:33Z","publication_identifier":{"isbn":["9781450327848"]},"has_accepted_license":"1","publication_status":"published","citation":{"mla":"Arzt, Steven, et al. “FlowDroid: Precise Context, Flow, Field, Object-Sensitive and Lifecycle-Aware Taint Analysis for Android Apps.” <i>Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI ’14</i>, ACM Press, 2014, doi:<a href=\"https://doi.org/10.1145/2594291.2594299\">10.1145/2594291.2594299</a>.","bibtex":"@inproceedings{Arzt_Rasthofer_Fritz_Bodden_Bartel_Klein_Le Traon_Octeau_McDaniel_2014, title={FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware Taint Analysis for Android Apps}, DOI={<a href=\"https://doi.org/10.1145/2594291.2594299\">10.1145/2594291.2594299</a>}, booktitle={Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI ’14}, publisher={ACM Press}, author={Arzt, Steven and Rasthofer, Siegfried and Fritz, Christian and Bodden, Eric and Bartel, Alexandre and Klein, Jacques and Le Traon, Yves and Octeau, Damien and McDaniel, Patrick}, year={2014} }","short":"S. Arzt, S. Rasthofer, C. Fritz, E. Bodden, A. Bartel, J. Klein, Y. Le Traon, D. Octeau, P. McDaniel, in: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI ’14, ACM Press, 2014.","apa":"Arzt, S., Rasthofer, S., Fritz, C., Bodden, E., Bartel, A., Klein, J., … McDaniel, P. (2014). FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware Taint Analysis for Android Apps. In <i>Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI ’14</i>. ACM Press. <a href=\"https://doi.org/10.1145/2594291.2594299\">https://doi.org/10.1145/2594291.2594299</a>","ama":"Arzt S, Rasthofer S, Fritz C, et al. FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware Taint Analysis for Android Apps. In: <i>Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI ’14</i>. ACM Press; 2014. doi:<a href=\"https://doi.org/10.1145/2594291.2594299\">10.1145/2594291.2594299</a>","ieee":"S. Arzt <i>et al.</i>, “FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware Taint Analysis for Android Apps,” in <i>Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI ’14</i>, 2014.","chicago":"Arzt, Steven, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre Bartel, Jacques Klein, Yves Le Traon, Damien Octeau, and Patrick McDaniel. “FlowDroid: Precise Context, Flow, Field, Object-Sensitive and Lifecycle-Aware Taint Analysis for Android Apps.” In <i>Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI ’14</i>. ACM Press, 2014. <a href=\"https://doi.org/10.1145/2594291.2594299\">https://doi.org/10.1145/2594291.2594299</a>."},"author":[{"first_name":"Steven","last_name":"Arzt","full_name":"Arzt, Steven"},{"last_name":"Rasthofer","full_name":"Rasthofer, Siegfried","first_name":"Siegfried"},{"full_name":"Fritz, Christian","last_name":"Fritz","first_name":"Christian"},{"full_name":"Bodden, Eric","id":"59256","orcid":"0000-0003-3470-3647","last_name":"Bodden","first_name":"Eric"},{"first_name":"Alexandre","full_name":"Bartel, Alexandre","last_name":"Bartel"},{"last_name":"Klein","full_name":"Klein, Jacques","first_name":"Jacques"},{"first_name":"Yves","full_name":"Le Traon, Yves","last_name":"Le Traon"},{"full_name":"Octeau, Damien","last_name":"Octeau","first_name":"Damien"},{"full_name":"McDaniel, Patrick","last_name":"McDaniel","first_name":"Patrick"}],"date_updated":"2022-01-06T07:01:42Z","doi":"10.1145/2594291.2594299","main_file_link":[{"url":"http://www.bodden.de/pubs/far+14flowdroid.pdf"}]},{"publication":"International Conference on Availability, Reliability and Security (ARES 2014)","type":"conference","status":"public","file":[{"relation":"main_file","content_type":"application/pdf","file_name":"ralb14droidforce.pdf","access_level":"closed","file_id":"5247","file_size":661565,"date_created":"2018-11-02T13:21:13Z","creator":"ups","date_updated":"2018-11-02T13:21:13Z"}],"_id":"5190","project":[{"_id":"1","name":"SFB 901"},{"_id":"3","name":"SFB 901 - Project Area B"},{"_id":"12","name":"SFB 901 - Subproject B4"}],"department":[{"_id":"76"}],"user_id":"477","ddc":["004"],"extern":"1","language":[{"iso":"eng"}],"file_date_updated":"2018-11-02T13:21:13Z","has_accepted_license":"1","year":"2014","page":"40-49","citation":{"ieee":"S. Arzt, S. Rasthofer, E. Lovat, and E. Bodden, “DroidForce: Enforcing Complex, Data-Centric, System-Wide Policies in Android,” in <i>International Conference on Availability, Reliability and Security (ARES 2014)</i>, 2014, pp. 40–49.","chicago":"Arzt, Steven, Siegfried Rasthofer, Enrico Lovat, and Eric Bodden. “DroidForce: Enforcing Complex, Data-Centric, System-Wide Policies in Android.” In <i>International Conference on Availability, Reliability and Security (ARES 2014)</i>, 40–49. IEEE, 2014.","ama":"Arzt S, Rasthofer S, Lovat E, Bodden E. DroidForce: Enforcing Complex, Data-Centric, System-Wide Policies in Android. In: <i>International Conference on Availability, Reliability and Security (ARES 2014)</i>. IEEE; 2014:40-49.","mla":"Arzt, Steven, et al. “DroidForce: Enforcing Complex, Data-Centric, System-Wide Policies in Android.” <i>International Conference on Availability, Reliability and Security (ARES 2014)</i>, IEEE, 2014, pp. 40–49.","bibtex":"@inproceedings{Arzt_Rasthofer_Lovat_Bodden_2014, title={DroidForce: Enforcing Complex, Data-Centric, System-Wide Policies in Android}, booktitle={International Conference on Availability, Reliability and Security (ARES 2014)}, publisher={IEEE}, author={Arzt, Steven and Rasthofer, Siegfried and Lovat, Enrico and Bodden, Eric}, year={2014}, pages={40–49} }","short":"S. Arzt, S. Rasthofer, E. Lovat, E. Bodden, in: International Conference on Availability, Reliability and Security (ARES 2014), IEEE, 2014, pp. 40–49.","apa":"Arzt, S., Rasthofer, S., Lovat, E., &#38; Bodden, E. (2014). DroidForce: Enforcing Complex, Data-Centric, System-Wide Policies in Android. In <i>International Conference on Availability, Reliability and Security (ARES 2014)</i> (pp. 40–49). IEEE."},"publisher":"IEEE","date_updated":"2022-01-06T07:01:43Z","author":[{"first_name":"Steven","full_name":"Arzt, Steven","last_name":"Arzt"},{"last_name":"Rasthofer","full_name":"Rasthofer, Siegfried","first_name":"Siegfried"},{"full_name":"Lovat, Enrico","last_name":"Lovat","first_name":"Enrico"},{"first_name":"Eric","full_name":"Bodden, Eric","id":"59256","orcid":"0000-0003-3470-3647","last_name":"Bodden"}],"date_created":"2018-10-31T11:04:43Z","title":"DroidForce: Enforcing Complex, Data-Centric, System-Wide Policies in Android","main_file_link":[{"url":"http://www.bodden.de/pubs/ralb14droidforce.pdf"}]}]