[{"date_updated":"2022-01-06T06:51:02Z","author":[{"full_name":"Jakobs, Marie-Christine","last_name":"Jakobs","first_name":"Marie-Christine"},{"last_name":"Krämer","full_name":"Krämer, Julia","first_name":"Julia"},{"first_name":"Dirk","full_name":"van Straaten, Dirk","id":"10311","last_name":"van Straaten"},{"full_name":"Lettmann, Theodor","id":"315","orcid":"0000-0001-5859-2457","last_name":"Lettmann","first_name":"Theodor"}],"page":"7-12","citation":{"ama":"Jakobs M-C, Krämer J, van Straaten D, Lettmann T. Certification Matters for Service Markets. In: Marcelo De Barros, Janusz Klink,Tadeus Uhl TP, ed. <i>The Ninth International Conferences on Advanced Service Computing (SERVICE COMPUTATION)</i>. ; 2017:7-12.","ieee":"M.-C. Jakobs, J. Krämer, D. van Straaten, and T. Lettmann, “Certification Matters for Service Markets,” in <i>The Ninth International Conferences on Advanced Service Computing (SERVICE COMPUTATION)</i>, 2017, pp. 7–12.","chicago":"Jakobs, Marie-Christine, Julia Krämer, Dirk van Straaten, and Theodor Lettmann. “Certification Matters for Service Markets.” In <i>The Ninth International Conferences on Advanced Service Computing (SERVICE COMPUTATION)</i>, edited by Thomas Prinz Marcelo De Barros, Janusz Klink,Tadeus Uhl, 7–12, 2017.","apa":"Jakobs, M.-C., Krämer, J., van Straaten, D., &#38; Lettmann, T. (2017). Certification Matters for Service Markets. In T. P. Marcelo De Barros, Janusz Klink,Tadeus Uhl (Ed.), <i>The Ninth International Conferences on Advanced Service Computing (SERVICE COMPUTATION)</i> (pp. 7–12).","short":"M.-C. Jakobs, J. Krämer, D. van Straaten, T. Lettmann, in: T.P. Marcelo De Barros, Janusz Klink,Tadeus Uhl (Ed.), The Ninth International Conferences on Advanced Service Computing (SERVICE COMPUTATION), 2017, pp. 7–12.","mla":"Jakobs, Marie-Christine, et al. “Certification Matters for Service Markets.” <i>The Ninth International Conferences on Advanced Service Computing (SERVICE COMPUTATION)</i>, edited by Thomas Prinz Marcelo De Barros, Janusz Klink,Tadeus Uhl, 2017, pp. 7–12.","bibtex":"@inproceedings{Jakobs_Krämer_van Straaten_Lettmann_2017, title={Certification Matters for Service Markets}, booktitle={The Ninth International Conferences on Advanced Service Computing (SERVICE COMPUTATION)}, author={Jakobs, Marie-Christine and Krämer, Julia and van Straaten, Dirk and Lettmann, Theodor}, editor={Marcelo De Barros, Janusz Klink,Tadeus Uhl, Thomas PrinzEditor}, year={2017}, pages={7–12} }"},"has_accepted_license":"1","file_date_updated":"2018-03-21T13:04:12Z","_id":"115","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Subprojekt B2","_id":"10"},{"name":"SFB 901 - Subproject B3","_id":"11"},{"_id":"12","name":"SFB 901 - Subproject B4"},{"_id":"8","name":"SFB 901 - Subproject A4"},{"_id":"2","name":"SFB 901 - Project Area A"},{"_id":"3","name":"SFB 901 - Project Area B"}],"department":[{"_id":"77"},{"_id":"355"},{"_id":"179"}],"user_id":"477","editor":[{"first_name":"Thomas Prinz","full_name":"Marcelo De Barros, Janusz Klink,Tadeus Uhl, Thomas Prinz","last_name":"Marcelo De Barros, Janusz Klink,Tadeus Uhl"}],"status":"public","type":"conference","title":"Certification Matters for Service Markets","date_created":"2017-10-17T12:41:14Z","year":"2017","ddc":["040"],"language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"Whenever customers have to decide between different instances of the same product, they are interested in buying the best product. In contrast, companies are interested in reducing the construction effort (and usually as a consequence thereof, the quality) to gain profit. The described setting is widely known as opposed preferences in quality of the product and also applies to the context of service-oriented computing. In general, service-oriented computing emphasizes the construction of large software systems out of existing services, where services are small and self-contained pieces of software that adhere to a specified interface. Several implementations of the same interface are considered as several instances of the same service. Thereby, customers are interested in buying the best service implementation for their service composition wrt. to metrics, such as costs, energy, memory consumption, or execution time. One way to ensure the service quality is to employ certificates, which can come in different kinds: Technical certificates proving correctness can be automatically constructed by the service provider and again be automatically checked by the user. Digital certificates allow proof of the integrity of a product. Other certificates might be rolled out if service providers follow a good software construction principle, which is checked in annual audits. Whereas all of these certificates are handled differently in service markets, what they have in common is that they influence the buying decisions of customers. In this paper, we review state-of-the-art developments in certification with respect to service-oriented computing. We not only discuss how certificates are constructed and handled in service-oriented computing but also review the effects of certificates on the market from an economic perspective."}],"file":[{"content_type":"application/pdf","relation":"main_file","success":1,"creator":"florida","date_created":"2018-03-21T13:04:12Z","date_updated":"2018-03-21T13:04:12Z","file_id":"1564","file_name":"115-JakobsKraemerVanStraatenLettmann2017.pdf","access_level":"closed","file_size":133531}],"publication":"The Ninth International Conferences on Advanced Service Computing (SERVICE COMPUTATION)"},{"year":"2017","citation":{"apa":"Witschen, L. M. (2017). <i>A Framework for the Synthesis of Approximate Circuits</i>. Universität Paderborn.","short":"L.M. Witschen, A Framework for the Synthesis of Approximate Circuits, Universität Paderborn, 2017.","bibtex":"@book{Witschen_2017, title={A Framework for the Synthesis of Approximate Circuits}, publisher={Universität Paderborn}, author={Witschen, Linus Matthias}, year={2017} }","mla":"Witschen, Linus Matthias. <i>A Framework for the Synthesis of Approximate Circuits</i>. Universität Paderborn, 2017.","ama":"Witschen LM. <i>A Framework for the Synthesis of Approximate Circuits</i>. Universität Paderborn; 2017.","chicago":"Witschen, Linus Matthias. <i>A Framework for the Synthesis of Approximate Circuits</i>. Universität Paderborn, 2017.","ieee":"L. M. Witschen, <i>A Framework for the Synthesis of Approximate Circuits</i>. Universität Paderborn, 2017."},"title":"A Framework for the Synthesis of Approximate Circuits","publisher":"Universität Paderborn","date_updated":"2022-01-06T06:51:03Z","author":[{"first_name":"Linus Matthias","full_name":"Witschen, Linus Matthias","id":"49051","last_name":"Witschen"}],"supervisor":[{"last_name":"Platzner","id":"398","full_name":"Platzner, Marco","first_name":"Marco"},{"first_name":"Tobias","last_name":"Wiersema","id":"3118","full_name":"Wiersema, Tobias"}],"date_created":"2018-02-01T14:21:19Z","status":"public","type":"mastersthesis","language":[{"iso":"eng"}],"project":[{"name":"SFB 901","_id":"1"},{"_id":"3","name":"SFB 901 - Project Area B"},{"_id":"12","name":"SFB 901 - Subproject B4"},{"name":"Computing Resources Provided by the Paderborn Center for Parallel Computing","_id":"52"}],"_id":"1157","user_id":"477","department":[{"_id":"78"},{"_id":"7"}]},{"ddc":["040"],"file_date_updated":"2018-03-21T13:13:04Z","language":[{"iso":"eng"}],"project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"name":"SFB 901 - Project Area B","_id":"3"}],"_id":"90","user_id":"477","department":[{"_id":"77"}],"abstract":[{"text":"We propose and extend an approach for the verification of safety properties for parameterized timed systems modeled as networks of timed automata. For this task, we introduce an incremental workflow that is based on our algorithm IC3 with Zones. It proceeds in a cycle in which single models of the system are verified, and the verification results are employed for the reasoning about the entire system. Starting with the smallest instances, the verification of the safety property is carried out fast and efficient. On successful verification, the algorithm produces an inductive strengthening of the safety property. We reuse this result and try to reason about the entire parameterized timed system. To this end, we extrapolate the inductive strengthening into a candidate for the next-larger model. In case this candidate is a valid inductive strengthening for the next larger model, our main theorem reasons about all models of the parameterized timed system, stating that the safety property holds true for all models. Otherwise, the main cycle starts over with the verification of the next larger model. This workflow is iterated indefinitely, until able to reason about the entire parameterized timed system, until a counterexample trace is found, or until the single models become too large to be handled in the verification. We reuse the intermediate results in a Feedback-loop in order to accelerate the verification runs for the single models. Furthermore, we consider an extended formalism in comparison to our previous publications.","lang":"eng"}],"file":[{"content_type":"application/pdf","relation":"main_file","success":1,"date_created":"2018-03-21T13:13:04Z","creator":"florida","date_updated":"2018-03-21T13:13:04Z","access_level":"closed","file_name":"90-a47-isenberg.pdf","file_id":"1572","file_size":584870}],"status":"public","type":"journal_article","publication":"ACM Transactions on Embedded Computing Systems","title":"Incremental Inductive Verification of Parameterized Timed Systems","doi":"10.1145/2984640","date_updated":"2022-01-06T07:04:06Z","publisher":"ACM","author":[{"first_name":"Tobias","last_name":"Isenberg","full_name":"Isenberg, Tobias"}],"date_created":"2017-10-17T12:41:09Z","year":"2017","citation":{"ieee":"T. Isenberg, “Incremental Inductive Verification of Parameterized Timed Systems,” <i>ACM Transactions on Embedded Computing Systems</i>, no. 2, pp. 47:1-47:24, 2017.","chicago":"Isenberg, Tobias. “Incremental Inductive Verification of Parameterized Timed Systems.” <i>ACM Transactions on Embedded Computing Systems</i>, no. 2 (2017): 47:1-47:24. <a href=\"https://doi.org/10.1145/2984640\">https://doi.org/10.1145/2984640</a>.","ama":"Isenberg T. Incremental Inductive Verification of Parameterized Timed Systems. <i>ACM Transactions on Embedded Computing Systems</i>. 2017;(2):47:1-47:24. doi:<a href=\"https://doi.org/10.1145/2984640\">10.1145/2984640</a>","short":"T. Isenberg, ACM Transactions on Embedded Computing Systems (2017) 47:1-47:24.","mla":"Isenberg, Tobias. “Incremental Inductive Verification of Parameterized Timed Systems.” <i>ACM Transactions on Embedded Computing Systems</i>, no. 2, ACM, 2017, pp. 47:1-47:24, doi:<a href=\"https://doi.org/10.1145/2984640\">10.1145/2984640</a>.","bibtex":"@article{Isenberg_2017, title={Incremental Inductive Verification of Parameterized Timed Systems}, DOI={<a href=\"https://doi.org/10.1145/2984640\">10.1145/2984640</a>}, number={2}, journal={ACM Transactions on Embedded Computing Systems}, publisher={ACM}, author={Isenberg, Tobias}, year={2017}, pages={47:1-47:24} }","apa":"Isenberg, T. (2017). Incremental Inductive Verification of Parameterized Timed Systems. <i>ACM Transactions on Embedded Computing Systems</i>, (2), 47:1-47:24. <a href=\"https://doi.org/10.1145/2984640\">https://doi.org/10.1145/2984640</a>"},"page":"47:1-47:24","has_accepted_license":"1","issue":"2"},{"doi":"10.1007/978-3-319-68690-5_22","title":"Policy Dependent and Independent Information Flow Analyses","author":[{"first_name":"Manuel","last_name":"Töws","full_name":"Töws, Manuel","id":"11315"},{"id":"573","full_name":"Wehrheim, Heike","last_name":"Wehrheim","first_name":"Heike"}],"date_created":"2018-11-21T09:38:43Z","publisher":"Springer International Publishing","date_updated":"2022-01-06T07:02:39Z","page":"362-378","citation":{"bibtex":"@inproceedings{Töws_Wehrheim_2017, title={Policy Dependent and Independent Information Flow Analyses}, DOI={<a href=\"https://doi.org/10.1007/978-3-319-68690-5_22\">10.1007/978-3-319-68690-5_22</a>}, booktitle={Formal Methods and Software Engineering - 19th International Conference  on Formal Engineering Methods (ICFEM 2017)}, publisher={Springer International Publishing}, author={Töws, Manuel and Wehrheim, Heike}, year={2017}, pages={362–378} }","short":"M. Töws, H. Wehrheim, in: Formal Methods and Software Engineering - 19th International Conference  on Formal Engineering Methods (ICFEM 2017), Springer International Publishing, 2017, pp. 362–378.","mla":"Töws, Manuel, and Heike Wehrheim. “Policy Dependent and Independent Information Flow Analyses.” <i>Formal Methods and Software Engineering - 19th International Conference  on Formal Engineering Methods (ICFEM 2017)</i>, Springer International Publishing, 2017, pp. 362–78, doi:<a href=\"https://doi.org/10.1007/978-3-319-68690-5_22\">10.1007/978-3-319-68690-5_22</a>.","apa":"Töws, M., &#38; Wehrheim, H. (2017). Policy Dependent and Independent Information Flow Analyses. In <i>Formal Methods and Software Engineering - 19th International Conference  on Formal Engineering Methods (ICFEM 2017)</i> (pp. 362–378). Springer International Publishing. <a href=\"https://doi.org/10.1007/978-3-319-68690-5_22\">https://doi.org/10.1007/978-3-319-68690-5_22</a>","ama":"Töws M, Wehrheim H. Policy Dependent and Independent Information Flow Analyses. In: <i>Formal Methods and Software Engineering - 19th International Conference  on Formal Engineering Methods (ICFEM 2017)</i>. Springer International Publishing; 2017:362-378. doi:<a href=\"https://doi.org/10.1007/978-3-319-68690-5_22\">10.1007/978-3-319-68690-5_22</a>","chicago":"Töws, Manuel, and Heike Wehrheim. “Policy Dependent and Independent Information Flow Analyses.” In <i>Formal Methods and Software Engineering - 19th International Conference  on Formal Engineering Methods (ICFEM 2017)</i>, 362–78. Springer International Publishing, 2017. <a href=\"https://doi.org/10.1007/978-3-319-68690-5_22\">https://doi.org/10.1007/978-3-319-68690-5_22</a>.","ieee":"M. Töws and H. Wehrheim, “Policy Dependent and Independent Information Flow Analyses,” in <i>Formal Methods and Software Engineering - 19th International Conference  on Formal Engineering Methods (ICFEM 2017)</i>, 2017, pp. 362–378."},"year":"2017","has_accepted_license":"1","publication_identifier":{"isbn":["9783319686899","9783319686905"],"issn":["0302-9743","1611-3349"]},"publication_status":"published","file_date_updated":"2018-11-26T15:07:42Z","language":[{"iso":"eng"}],"ddc":["000"],"department":[{"_id":"77"}],"user_id":"477","_id":"5769","project":[{"name":"SFB 901 - Subproject B4","_id":"12"},{"name":"SFB 901 - Project Area B","_id":"3"},{"name":"SFB 901","_id":"1"}],"status":"public","file":[{"date_created":"2018-11-26T15:07:42Z","creator":"mtoews","date_updated":"2018-11-26T15:07:42Z","access_level":"closed","file_id":"5836","file_name":"Töws-Wehrheim2017_Chapter_PolicyDependentAndIndependentI.pdf","file_size":424031,"content_type":"application/pdf","relation":"main_file","success":1}],"abstract":[{"lang":"eng","text":"Information Flow Analysis (IFA) aims at detecting illegal flows of information between program entities. “Legality” is therein specified in terms of various security policies. For the analysis, this opens up two possibilities: building generic, policy independent and building specific, policy dependent IFAs. While the former needs to track all dependencies between program entities, the latter allows for a reduced and thus more efficient analysis.\r\n\r\nIn this paper, we start out by formally defining a policy independent information flow analysis. Next, we show how to specialize this IFA via policy specific variable tracking, and prove soundness of the specialization. We furthermore investigate refinement relationships between policies, allowing an IFA for one policy to be employed for its refinements. As policy refinement depends on concrete program entities, we additionally propose a precomputation of policy refinement conditions, enabling an efficient refinement check for concrete programs."}],"publication":"Formal Methods and Software Engineering - 19th International Conference  on Formal Engineering Methods (ICFEM 2017)","type":"conference"},{"publication":"Proceedings of the 3rd International Workshop on Software Analytics","type":"conference","abstract":[{"lang":"eng","text":"Today, software verification tools have reached the maturity to be used for large scale programs. Different tools perform differently well on varying code. A software developer is hence faced with the problem of choosing a tool appropriate for her program at hand. A ranking of tools on programs could facilitate the choice. Such rankings can, however, so far only be obtained by running all considered tools on the program.In this paper, we present a machine learning approach to predicting rankings of tools on programs. The method builds upon so-called label ranking algorithms, which we complement with appropriate kernels providing a similarity measure for programs. Our kernels employ a graph representation for software source code that mixes elements of control flow and program dependence graphs with abstract syntax trees. Using data sets from the software verification competition SV-COMP, we demonstrate our rank prediction technique to generalize well and achieve a rather high predictive accuracy (rank correlation > 0.6)."}],"status":"public","file":[{"content_type":"application/pdf","success":1,"relation":"main_file","date_updated":"2018-11-02T14:24:29Z","creator":"ups","date_created":"2018-11-02T14:24:29Z","file_size":822383,"file_name":"fsews17swan-swanmain1.pdf","access_level":"closed","file_id":"5271"}],"_id":"71","project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"name":"SFB 901 - Subproject B2","_id":"10"},{"_id":"3","name":"SFB 901 - Project Area B"},{"_id":"11","name":"SFB 901 - Subproject B3"}],"department":[{"_id":"355"},{"_id":"77"}],"user_id":"15504","series_title":"SWAN'17","ddc":["000"],"language":[{"iso":"eng"}],"file_date_updated":"2018-11-02T14:24:29Z","has_accepted_license":"1","year":"2017","page":"23-26","citation":{"apa":"Czech, M., Hüllermeier, E., Jakobs, M.-C., &#38; Wehrheim, H. (2017). Predicting Rankings of Software Verification Tools. In <i>Proceedings of the 3rd International Workshop on Software Analytics</i> (pp. 23–26). <a href=\"https://doi.org/10.1145/3121257.3121262\">https://doi.org/10.1145/3121257.3121262</a>","bibtex":"@inproceedings{Czech_Hüllermeier_Jakobs_Wehrheim_2017, series={SWAN’17}, title={Predicting Rankings of Software Verification Tools}, DOI={<a href=\"https://doi.org/10.1145/3121257.3121262\">10.1145/3121257.3121262</a>}, booktitle={Proceedings of the 3rd International Workshop on Software Analytics}, author={Czech, Mike and Hüllermeier, Eyke and Jakobs, Marie-Christine and Wehrheim, Heike}, year={2017}, pages={23–26}, collection={SWAN’17} }","short":"M. Czech, E. Hüllermeier, M.-C. Jakobs, H. Wehrheim, in: Proceedings of the 3rd International Workshop on Software Analytics, 2017, pp. 23–26.","mla":"Czech, Mike, et al. “Predicting Rankings of Software Verification Tools.” <i>Proceedings of the 3rd International Workshop on Software Analytics</i>, 2017, pp. 23–26, doi:<a href=\"https://doi.org/10.1145/3121257.3121262\">10.1145/3121257.3121262</a>.","ieee":"M. Czech, E. Hüllermeier, M.-C. Jakobs, and H. Wehrheim, “Predicting Rankings of Software Verification Tools,” in <i>Proceedings of the 3rd International Workshop on Software Analytics</i>, 2017, pp. 23–26.","chicago":"Czech, Mike, Eyke Hüllermeier, Marie-Christine Jakobs, and Heike Wehrheim. “Predicting Rankings of Software Verification Tools.” In <i>Proceedings of the 3rd International Workshop on Software Analytics</i>, 23–26. SWAN’17, 2017. <a href=\"https://doi.org/10.1145/3121257.3121262\">https://doi.org/10.1145/3121257.3121262</a>.","ama":"Czech M, Hüllermeier E, Jakobs M-C, Wehrheim H. Predicting Rankings of Software Verification Tools. In: <i>Proceedings of the 3rd International Workshop on Software Analytics</i>. SWAN’17. ; 2017:23-26. doi:<a href=\"https://doi.org/10.1145/3121257.3121262\">10.1145/3121257.3121262</a>"},"date_updated":"2022-01-06T07:03:28Z","author":[{"first_name":"Mike","last_name":"Czech","full_name":"Czech, Mike"},{"first_name":"Eyke","last_name":"Hüllermeier","full_name":"Hüllermeier, Eyke","id":"48129"},{"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:05Z","title":"Predicting Rankings of Software Verification Tools","doi":"10.1145/3121257.3121262"},{"ddc":["000"],"file_date_updated":"2018-11-21T10:50:11Z","language":[{"iso":"eng"}],"_id":"72","project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Subprojekt B3","_id":"11"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"department":[{"_id":"77"},{"_id":"355"}],"user_id":"15504","abstract":[{"lang":"eng","text":"Software verification competitions, such as the annual SV-COMP, evaluate software verification tools with respect to their effectivity and efficiency. Typically, the outcome of a competition is a (possibly category-specific) ranking of the tools. For many applications, such as building portfolio solvers, it would be desirable to have an idea of the (relative) performance of verification tools on a given verification task beforehand, i.e., prior to actually running all tools on the task.In this paper, we present a machine learning approach to predicting rankings of tools on verification tasks. The method builds upon so-called label ranking algorithms, which we complement with appropriate kernels providing a similarity measure for verification tasks. Our kernels employ a graph representation for software source code that mixes elements of control flow and program dependence graphs with abstract syntax trees. Using data sets from SV-COMP, we demonstrate our rank prediction technique to generalize well and achieve a rather high predictive accuracy. In particular, our method outperforms a recently proposed feature-based approach of Demyanova et al. (when applied to rank predictions). "}],"status":"public","file":[{"success":1,"relation":"main_file","content_type":"application/pdf","file_size":869984,"access_level":"closed","file_id":"5782","file_name":"Predicting Rankings of Soware Verification Competitions.pdf","date_updated":"2018-11-21T10:50:11Z","date_created":"2018-11-21T10:50:11Z","creator":"florida"}],"type":"report","title":"Predicting Rankings of Software Verification Competitions","date_updated":"2022-01-06T07:03:29Z","author":[{"last_name":"Czech","full_name":"Czech, Mike","first_name":"Mike"},{"first_name":"Eyke","last_name":"Hüllermeier","full_name":"Hüllermeier, Eyke","id":"48129"},{"first_name":"Marie-Christine","full_name":"Jakobs, Marie-Christine","last_name":"Jakobs"},{"last_name":"Wehrheim","full_name":"Wehrheim, Heike","id":"573","first_name":"Heike"}],"date_created":"2017-10-17T12:41:05Z","year":"2017","citation":{"apa":"Czech, M., Hüllermeier, E., Jakobs, M.-C., &#38; Wehrheim, H. (2017). <i>Predicting Rankings of Software Verification Competitions</i>.","mla":"Czech, Mike, et al. <i>Predicting Rankings of Software Verification Competitions</i>. 2017.","bibtex":"@book{Czech_Hüllermeier_Jakobs_Wehrheim_2017, title={Predicting Rankings of Software Verification Competitions}, author={Czech, Mike and Hüllermeier, Eyke and Jakobs, Marie-Christine and Wehrheim, Heike}, year={2017} }","short":"M. Czech, E. Hüllermeier, M.-C. Jakobs, H. Wehrheim, Predicting Rankings of Software Verification Competitions, 2017.","ieee":"M. Czech, E. Hüllermeier, M.-C. Jakobs, and H. Wehrheim, <i>Predicting Rankings of Software Verification Competitions</i>. 2017.","chicago":"Czech, Mike, Eyke Hüllermeier, Marie-Christine Jakobs, and Heike Wehrheim. <i>Predicting Rankings of Software Verification Competitions</i>, 2017.","ama":"Czech M, Hüllermeier E, Jakobs M-C, Wehrheim H. <i>Predicting Rankings of Software Verification Competitions</i>.; 2017."},"has_accepted_license":"1"},{"language":[{"iso":"eng"}],"file_date_updated":"2018-11-02T14:47:04Z","ddc":["000"],"series_title":"Lecture Notes in Computer Science","user_id":"477","_id":"73","project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"name":"SFB 901 - Project Area B","_id":"3"}],"status":"public","file":[{"date_created":"2018-11-02T14:47:04Z","creator":"ups","date_updated":"2018-11-02T14:47:04Z","file_id":"5283","access_level":"closed","file_name":"PARTMathrmPWFromPartialAnalysi.pdf","file_size":496965,"content_type":"application/pdf","relation":"main_file","success":1}],"abstract":[{"lang":"eng","text":"Today, verification tools do not only output yes or no, but also provide correctness arguments or counterexamples. While counterexamples help to fix bugs, correctness arguments are used to increase the trust in program correctness, e.g., in Proof-Carrying Code (PCC). Correctness arguments are well-studied for single analyses, but not when a set of analyses together verifies a program, each of the analyses checking only a particular part. Such a set of partial, complementary analyses is often used when a single analysis would fail or is inefficient on some program parts.We propose PART_PW, a technique which allows us to automatically construct a proof witness (correctness argument) from the analysis results obtained by a set of partial, complementary analyses. The constructed proof witnesses are proven to be valid correctness arguments and in our experiments we use them seamlessly and efficiently in existing PCC approaches."}],"editor":[{"first_name":"Alessandro","full_name":"Cimatti, Alessandro","last_name":"Cimatti"},{"first_name":"Marjan","full_name":"Sirjani, Marjan","last_name":"Sirjani"}],"publication":"Software Engineering and Formal Methods","type":"conference","doi":"10.1007/978-3-319-66197-1_8","title":"PART_PW: From Partial Analysis Results to a Proof Witness","author":[{"first_name":"Marie-Christine","full_name":"Jakobs, Marie-Christine","last_name":"Jakobs"}],"date_created":"2017-10-17T12:41:05Z","date_updated":"2022-01-06T07:03:32Z","page":"120-135","citation":{"ama":"Jakobs M-C. PART_PW: From Partial Analysis Results to a Proof Witness. In: Cimatti A, Sirjani M, eds. <i>Software Engineering and Formal Methods</i>. Lecture Notes in Computer Science. ; 2017:120-135. doi:<a href=\"https://doi.org/10.1007/978-3-319-66197-1_8\">10.1007/978-3-319-66197-1_8</a>","ieee":"M.-C. Jakobs, “PART_PW: From Partial Analysis Results to a Proof Witness,” in <i>Software Engineering and Formal Methods</i>, 2017, pp. 120–135.","chicago":"Jakobs, Marie-Christine. “PART_PW: From Partial Analysis Results to a Proof Witness.” In <i>Software Engineering and Formal Methods</i>, edited by Alessandro Cimatti and Marjan Sirjani, 120–35. Lecture Notes in Computer Science, 2017. <a href=\"https://doi.org/10.1007/978-3-319-66197-1_8\">https://doi.org/10.1007/978-3-319-66197-1_8</a>.","apa":"Jakobs, M.-C. (2017). PART_PW: From Partial Analysis Results to a Proof Witness. In A. Cimatti &#38; M. Sirjani (Eds.), <i>Software Engineering and Formal Methods</i> (pp. 120–135). <a href=\"https://doi.org/10.1007/978-3-319-66197-1_8\">https://doi.org/10.1007/978-3-319-66197-1_8</a>","bibtex":"@inproceedings{Jakobs_2017, series={Lecture Notes in Computer Science}, title={PART_PW: From Partial Analysis Results to a Proof Witness}, DOI={<a href=\"https://doi.org/10.1007/978-3-319-66197-1_8\">10.1007/978-3-319-66197-1_8</a>}, booktitle={Software Engineering and Formal Methods}, author={Jakobs, Marie-Christine}, editor={Cimatti, Alessandro and Sirjani, MarjanEditors}, year={2017}, pages={120–135}, collection={Lecture Notes in Computer Science} }","mla":"Jakobs, Marie-Christine. “PART_PW: From Partial Analysis Results to a Proof Witness.” <i>Software Engineering and Formal Methods</i>, edited by Alessandro Cimatti and Marjan Sirjani, 2017, pp. 120–35, doi:<a href=\"https://doi.org/10.1007/978-3-319-66197-1_8\">10.1007/978-3-319-66197-1_8</a>.","short":"M.-C. Jakobs, in: A. Cimatti, M. Sirjani (Eds.), Software Engineering and Formal Methods, 2017, pp. 120–135."},"year":"2017","has_accepted_license":"1"},{"author":[{"last_name":"Späth","full_name":"Späth, Johannes","first_name":"Johannes"},{"last_name":"Ali","full_name":"Ali, Karim","first_name":"Karim"},{"first_name":"Eric","last_name":"Bodden","orcid":"0000-0003-3470-3647","id":"59256","full_name":"Bodden, Eric"}],"date_created":"2018-10-31T12:46:50Z","date_updated":"2022-01-06T07:01:44Z","publisher":"ACM Press","main_file_link":[{"url":" http://bodden.de/pubs/sab17ideal.pdf"}],"title":"IDEal: Efficient and Precise Alias-aware Dataflow Analysis","has_accepted_license":"1","citation":{"apa":"Späth, J., Ali, K., &#38; Bodden, E. (2017). IDEal: Efficient and Precise Alias-aware Dataflow Analysis. In <i>2017 International Conference on Object-Oriented Programming, Languages and Applications (OOPSLA/SPLASH)</i>. ACM Press.","bibtex":"@inproceedings{Späth_Ali_Bodden_2017, title={IDEal: Efficient and Precise Alias-aware Dataflow Analysis}, booktitle={2017 International Conference on Object-Oriented Programming, Languages and Applications (OOPSLA/SPLASH)}, publisher={ACM Press}, author={Späth, Johannes and Ali, Karim and Bodden, Eric}, year={2017} }","mla":"Späth, Johannes, et al. “IDEal: Efficient and Precise Alias-Aware Dataflow Analysis.” <i>2017 International Conference on Object-Oriented Programming, Languages and Applications (OOPSLA/SPLASH)</i>, ACM Press, 2017.","short":"J. Späth, K. Ali, E. Bodden, in: 2017 International Conference on Object-Oriented Programming, Languages and Applications (OOPSLA/SPLASH), ACM Press, 2017.","ama":"Späth J, Ali K, Bodden E. IDEal: Efficient and Precise Alias-aware Dataflow Analysis. In: <i>2017 International Conference on Object-Oriented Programming, Languages and Applications (OOPSLA/SPLASH)</i>. ACM Press; 2017.","ieee":"J. Späth, K. Ali, and E. Bodden, “IDEal: Efficient and Precise Alias-aware Dataflow Analysis,” in <i>2017 International Conference on Object-Oriented Programming, Languages and Applications (OOPSLA/SPLASH)</i>, 2017.","chicago":"Späth, Johannes, Karim Ali, and Eric Bodden. “IDEal: Efficient and Precise Alias-Aware Dataflow Analysis.” In <i>2017 International Conference on Object-Oriented Programming, Languages and Applications (OOPSLA/SPLASH)</i>. ACM Press, 2017."},"year":"2017","user_id":"477","department":[{"_id":"76"}],"project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Project Area B","_id":"3"},{"name":"SFB 901 - Subproject B4","_id":"12"}],"_id":"5204","language":[{"iso":"eng"}],"file_date_updated":"2018-11-02T14:28:13Z","ddc":["000"],"keyword":["ATTRACT","ITSECWEBSITE","CROSSING"],"type":"conference","publication":"2017 International Conference on Object-Oriented Programming, Languages and Applications (OOPSLA/SPLASH)","file":[{"file_size":1021251,"file_id":"5273","access_level":"closed","file_name":"sab17ideal.pdf","date_updated":"2018-11-02T14:28:13Z","date_created":"2018-11-02T14:28:13Z","creator":"ups","success":1,"relation":"main_file","content_type":"application/pdf"}],"status":"public"},{"type":"journal_article","publication":"CoRR","file":[{"relation":"main_file","success":1,"content_type":"application/pdf","access_level":"closed","file_id":"5321","file_name":"1710.00390.pdf","file_size":2339380,"date_created":"2018-11-02T16:03:01Z","creator":"ups","date_updated":"2018-11-02T16:03:01Z"}],"status":"public","user_id":"477","department":[{"_id":"76"}],"project":[{"name":"SFB 901","_id":"1"},{"_id":"3","name":"SFB 901 - Project Area B"},{"name":"SFB 901 - Subproject B4","_id":"12"}],"_id":"5209","language":[{"iso":"eng"}],"file_date_updated":"2018-11-02T16:03:01Z","ddc":["000"],"has_accepted_license":"1","citation":{"chicago":"Fischer, Andreas, Benny Fuhry, Florian Kerschbaum, and Eric Bodden. “Computation on Encrypted Data Using Data Flow Authentication.” <i>CoRR</i> abs/1710.00390 (2017).","ieee":"A. Fischer, B. Fuhry, F. Kerschbaum, and E. Bodden, “Computation on Encrypted Data using Data Flow Authentication,” <i>CoRR</i>, vol. abs/1710.00390, 2017.","ama":"Fischer A, Fuhry B, Kerschbaum F, Bodden E. Computation on Encrypted Data using Data Flow Authentication. <i>CoRR</i>. 2017;abs/1710.00390.","mla":"Fischer, Andreas, et al. “Computation on Encrypted Data Using Data Flow Authentication.” <i>CoRR</i>, vol. abs/1710.00390, 2017.","bibtex":"@article{Fischer_Fuhry_Kerschbaum_Bodden_2017, title={Computation on Encrypted Data using Data Flow Authentication}, volume={abs/1710.00390}, journal={CoRR}, author={Fischer, Andreas and Fuhry, Benny and Kerschbaum, Florian and Bodden, Eric}, year={2017} }","short":"A. Fischer, B. Fuhry, F. Kerschbaum, E. Bodden, CoRR abs/1710.00390 (2017).","apa":"Fischer, A., Fuhry, B., Kerschbaum, F., &#38; Bodden, E. (2017). Computation on Encrypted Data using Data Flow Authentication. <i>CoRR</i>, <i>abs/1710.00390</i>."},"year":"2017","date_created":"2018-10-31T13:12:32Z","author":[{"last_name":"Fischer","full_name":"Fischer, Andreas","first_name":"Andreas"},{"first_name":"Benny","full_name":"Fuhry, Benny","last_name":"Fuhry"},{"full_name":"Kerschbaum, Florian","last_name":"Kerschbaum","first_name":"Florian"},{"orcid":"0000-0003-3470-3647","last_name":"Bodden","full_name":"Bodden, Eric","id":"59256","first_name":"Eric"}],"volume":"abs/1710.00390","date_updated":"2022-01-06T07:01:46Z","main_file_link":[{"url":"https://arxiv.org/pdf/1710.00390.pdf"}],"title":"Computation on Encrypted Data using Data Flow Authentication"},{"file_date_updated":"2018-11-02T16:08:17Z","language":[{"iso":"eng"}],"ddc":["000"],"department":[{"_id":"77"},{"_id":"78"}],"user_id":"3118","_id":"68","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"_id":"3","name":"SFB 901 - Project Area B"},{"_id":"52","name":"Computing Resources Provided by the Paderborn Center for Parallel Computing"}],"status":"public","file":[{"content_type":"application/pdf","success":1,"relation":"main_file","date_updated":"2018-11-02T16:08:17Z","date_created":"2018-11-02T16:08:17Z","creator":"ups","file_size":806356,"file_name":"a61-isenberg.pdf","access_level":"closed","file_id":"5324"}],"abstract":[{"lang":"eng","text":"Proof-carrying hardware (PCH) is a principle for achieving safety for dynamically reconfigurable hardware systems. The producer of a hardware module spends huge effort when creating a proof for a safety policy. The proof is then transferred as a certificate together with the configuration bitstream to the consumer of the hardware module, who can quickly verify the given proof. Previous work utilized SAT solvers and resolution traces to set up a PCH technology and corresponding tool flows. In this article, we present a novel technology for PCH based on inductive invariants. For sequential circuits, our approach is fundamentally stronger than the previous SAT-based one since we avoid the limitations of bounded unrolling. We contrast our technology to existing ones and show that it fits into previously proposed tool flows. We conduct experiments with four categories of benchmark circuits and report consumer and producer runtime and peak memory consumption, as well as the size of the certificates and the distribution of the workload between producer and consumer. Experiments clearly show that our new induction-based technology is superior for sequential circuits, whereas the previous SAT-based technology is the better choice for combinational circuits."}],"publication":"ACM Transactions on Design Automation of Electronic Systems","type":"journal_article","doi":"10.1145/3054743","title":"Proof-Carrying Hardware via Inductive Invariants","author":[{"last_name":"Isenberg","full_name":"Isenberg, Tobias","first_name":"Tobias"},{"last_name":"Platzner","full_name":"Platzner, Marco","id":"398","first_name":"Marco"},{"full_name":"Wehrheim, Heike","id":"573","last_name":"Wehrheim","first_name":"Heike"},{"last_name":"Wiersema","full_name":"Wiersema, Tobias","id":"3118","first_name":"Tobias"}],"date_created":"2017-10-17T12:41:04Z","publisher":"ACM","date_updated":"2022-01-06T07:03:20Z","page":"61:1--61:23","citation":{"bibtex":"@article{Isenberg_Platzner_Wehrheim_Wiersema_2017, title={Proof-Carrying Hardware via Inductive Invariants}, DOI={<a href=\"https://doi.org/10.1145/3054743\">10.1145/3054743</a>}, number={4}, journal={ACM Transactions on Design Automation of Electronic Systems}, publisher={ACM}, author={Isenberg, Tobias and Platzner, Marco and Wehrheim, Heike and Wiersema, Tobias}, year={2017}, pages={61:1--61:23} }","mla":"Isenberg, Tobias, et al. “Proof-Carrying Hardware via Inductive Invariants.” <i>ACM Transactions on Design Automation of Electronic Systems</i>, no. 4, ACM, 2017, pp. 61:1--61:23, doi:<a href=\"https://doi.org/10.1145/3054743\">10.1145/3054743</a>.","short":"T. Isenberg, M. Platzner, H. Wehrheim, T. Wiersema, ACM Transactions on Design Automation of Electronic Systems (2017) 61:1--61:23.","apa":"Isenberg, T., Platzner, M., Wehrheim, H., &#38; Wiersema, T. (2017). Proof-Carrying Hardware via Inductive Invariants. <i>ACM Transactions on Design Automation of Electronic Systems</i>, (4), 61:1--61:23. <a href=\"https://doi.org/10.1145/3054743\">https://doi.org/10.1145/3054743</a>","chicago":"Isenberg, Tobias, Marco Platzner, Heike Wehrheim, and Tobias Wiersema. “Proof-Carrying Hardware via Inductive Invariants.” <i>ACM Transactions on Design Automation of Electronic Systems</i>, no. 4 (2017): 61:1--61:23. <a href=\"https://doi.org/10.1145/3054743\">https://doi.org/10.1145/3054743</a>.","ieee":"T. Isenberg, M. Platzner, H. Wehrheim, and T. Wiersema, “Proof-Carrying Hardware via Inductive Invariants,” <i>ACM Transactions on Design Automation of Electronic Systems</i>, no. 4, pp. 61:1--61:23, 2017.","ama":"Isenberg T, Platzner M, Wehrheim H, Wiersema T. Proof-Carrying Hardware via Inductive Invariants. <i>ACM Transactions on Design Automation of Electronic Systems</i>. 2017;(4):61:1--61:23. doi:<a href=\"https://doi.org/10.1145/3054743\">10.1145/3054743</a>"},"year":"2017","issue":"4","has_accepted_license":"1"},{"publisher":"Universität Paderborn","date_updated":"2022-01-06T07:03:22Z","date_created":"2017-11-13T08:13:29Z","supervisor":[{"first_name":"Heike","last_name":"Wehrheim","full_name":"Wehrheim, Heike","id":"573"}],"author":[{"full_name":"Jakobs, Marie-Christine","last_name":"Jakobs","first_name":"Marie-Christine"}],"title":"On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring","doi":"10.17619/UNIPB/1-104","has_accepted_license":"1","year":"2017","citation":{"ama":"Jakobs M-C. <i>On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring</i>. Universität Paderborn; 2017. doi:<a href=\"https://doi.org/10.17619/UNIPB/1-104\">10.17619/UNIPB/1-104</a>","ieee":"M.-C. Jakobs, <i>On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring</i>. Universität Paderborn, 2017.","chicago":"Jakobs, Marie-Christine. <i>On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring</i>. Universität Paderborn, 2017. <a href=\"https://doi.org/10.17619/UNIPB/1-104\">https://doi.org/10.17619/UNIPB/1-104</a>.","apa":"Jakobs, M.-C. (2017). <i>On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring</i>. Universität Paderborn. <a href=\"https://doi.org/10.17619/UNIPB/1-104\">https://doi.org/10.17619/UNIPB/1-104</a>","mla":"Jakobs, Marie-Christine. <i>On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring</i>. Universität Paderborn, 2017, doi:<a href=\"https://doi.org/10.17619/UNIPB/1-104\">10.17619/UNIPB/1-104</a>.","short":"M.-C. Jakobs, On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring, Universität Paderborn, 2017.","bibtex":"@book{Jakobs_2017, title={On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring}, DOI={<a href=\"https://doi.org/10.17619/UNIPB/1-104\">10.17619/UNIPB/1-104</a>}, publisher={Universität Paderborn}, author={Jakobs, Marie-Christine}, year={2017} }"},"project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"_id":"685","user_id":"477","department":[{"_id":"77"}],"ddc":["040"],"file_date_updated":"2018-03-14T12:26:52Z","type":"dissertation","file":[{"content_type":"application/pdf","relation":"main_file","success":1,"creator":"florida","date_created":"2018-03-14T12:26:52Z","date_updated":"2018-03-14T12:26:52Z","file_id":"1211","access_level":"closed","file_name":"685-Dissertation-Jakobs.pdf","file_size":11828624}],"status":"public"},{"user_id":"477","department":[{"_id":"77"}],"project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"_id":"69","file_date_updated":"2018-03-21T13:15:09Z","language":[{"iso":"eng"}],"ddc":["040"],"type":"journal_article","publication":"ACM Transactions on Programming Languages and Systems","file":[{"success":1,"relation":"main_file","content_type":"application/pdf","file_size":1215139,"file_name":"69-a7-jakobs.pdf","access_level":"closed","file_id":"1575","date_updated":"2018-03-21T13:15:09Z","date_created":"2018-03-21T13:15:09Z","creator":"florida"}],"status":"public","abstract":[{"text":"Today, software is traded worldwide on global markets, with apps being downloaded to smartphones within minutes or seconds. This poses, more than ever, the challenge of ensuring safety of software in the face of (1) unknown or untrusted software providers together with (2) resource-limited software consumers. The concept of Proof-Carrying Code (PCC), years ago suggested by Necula, provides one framework for securing the execution of untrusted code. PCC techniques attach safety proofs, constructed by software producers, to code. Based on the assumption that checking proofs is usually much simpler than constructing proofs, software consumers should thus be able to quickly check the safety of software. However, PCC techniques often suffer from the size of certificates (i.e., the attached proofs), making PCC techniques inefficient in practice.In this article, we introduce a new framework for the safe execution of untrusted code called Programs from Proofs (PfP). The basic assumption underlying the PfP technique is the fact that the structure of programs significantly influences the complexity of checking a specific safety property. Instead of attaching proofs to program code, the PfP technique transforms the program into an efficiently checkable form, thus guaranteeing quick safety checks for software consumers. For this transformation, the technique also uses a producer-side automatic proof of safety. More specifically, safety proving for the software producer proceeds via the construction of an abstract reachability graph (ARG) unfolding the control-flow automaton (CFA) up to the degree necessary for simple checking. To this end, we combine different sorts of software analysis: expensive analyses incrementally determining the degree of unfolding, and cheap analyses responsible for safety checking. Out of the abstract reachability graph we generate the new program. In its CFA structure, it is isomorphic to the graph and hence another, this time consumer-side, cheap analysis can quickly determine its safety.Like PCC, Programs from Proofs is a general framework instantiable with different sorts of (expensive and cheap) analysis. Here, we present the general framework and exemplify it by some concrete examples. We have implemented different instantiations on top of the configurable program analysis tool CPAchecker and report on experiments, in particular on comparisons with PCC techniques.","lang":"eng"}],"date_created":"2017-10-17T12:41:04Z","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_updated":"2022-01-06T07:03:23Z","publisher":"ACM","doi":"10.1145/3014427","title":"Programs from Proofs: A Framework for the Safe Execution of Untrusted Software","issue":"2","has_accepted_license":"1","citation":{"ama":"Jakobs M-C, Wehrheim H. Programs from Proofs: A Framework for the Safe Execution of Untrusted Software. <i>ACM Transactions on Programming Languages and Systems</i>. 2017;(2):7:1-7:56. doi:<a href=\"https://doi.org/10.1145/3014427\">10.1145/3014427</a>","chicago":"Jakobs, Marie-Christine, and Heike Wehrheim. “Programs from Proofs: A Framework for the Safe Execution of Untrusted Software.” <i>ACM Transactions on Programming Languages and Systems</i>, no. 2 (2017): 7:1-7:56. <a href=\"https://doi.org/10.1145/3014427\">https://doi.org/10.1145/3014427</a>.","ieee":"M.-C. Jakobs and H. Wehrheim, “Programs from Proofs: A Framework for the Safe Execution of Untrusted Software,” <i>ACM Transactions on Programming Languages and Systems</i>, no. 2, pp. 7:1-7:56, 2017.","apa":"Jakobs, M.-C., &#38; Wehrheim, H. (2017). Programs from Proofs: A Framework for the Safe Execution of Untrusted Software. <i>ACM Transactions on Programming Languages and Systems</i>, (2), 7:1-7:56. <a href=\"https://doi.org/10.1145/3014427\">https://doi.org/10.1145/3014427</a>","short":"M.-C. Jakobs, H. Wehrheim, ACM Transactions on Programming Languages and Systems (2017) 7:1-7:56.","mla":"Jakobs, Marie-Christine, and Heike Wehrheim. “Programs from Proofs: A Framework for the Safe Execution of Untrusted Software.” <i>ACM Transactions on Programming Languages and Systems</i>, no. 2, ACM, 2017, pp. 7:1-7:56, doi:<a href=\"https://doi.org/10.1145/3014427\">10.1145/3014427</a>.","bibtex":"@article{Jakobs_Wehrheim_2017, title={Programs from Proofs: A Framework for the Safe Execution of Untrusted Software}, DOI={<a href=\"https://doi.org/10.1145/3014427\">10.1145/3014427</a>}, number={2}, journal={ACM Transactions on Programming Languages and Systems}, publisher={ACM}, author={Jakobs, Marie-Christine and Wehrheim, Heike}, year={2017}, pages={7:1-7:56} }"},"page":"7:1-7:56","year":"2017"},{"has_accepted_license":"1","year":"2017","citation":{"ama":"Pauck F. <i>Cooperative Static Analysis of Android Applications</i>. Universität Paderborn; 2017.","ieee":"F. Pauck, <i>Cooperative static analysis of Android applications</i>. Universität Paderborn, 2017.","chicago":"Pauck, Felix. <i>Cooperative Static Analysis of Android Applications</i>. Universität Paderborn, 2017.","apa":"Pauck, F. (2017). <i>Cooperative static analysis of Android applications</i>. Universität Paderborn.","mla":"Pauck, Felix. <i>Cooperative Static Analysis of Android Applications</i>. Universität Paderborn, 2017.","bibtex":"@book{Pauck_2017, title={Cooperative static analysis of Android applications}, publisher={Universität Paderborn}, author={Pauck, Felix}, year={2017} }","short":"F. Pauck, Cooperative Static Analysis of Android Applications, Universität Paderborn, 2017."},"oa":"1","date_updated":"2022-01-06T06:50:52Z","publisher":"Universität Paderborn","author":[{"last_name":"Pauck","full_name":"Pauck, Felix","id":"22398","first_name":"Felix"}],"date_created":"2017-10-17T12:41:12Z","supervisor":[{"first_name":"Heike","last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike"}],"title":"Cooperative static analysis of Android applications","type":"mastersthesis","status":"public","file":[{"date_updated":"2019-08-07T09:03:48Z","creator":"fpauck","date_created":"2019-08-07T08:55:58Z","title":"Master's Thesis","file_size":5093611,"file_id":"12905","access_level":"open_access","file_name":"fpauck_2017.pdf","content_type":"application/pdf","relation":"main_file"}],"_id":"109","project":[{"_id":"1","name":"SFB 901"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"name":"SFB 901 - Project Area B","_id":"3"}],"department":[{"_id":"77"}],"user_id":"22398","ddc":["000"],"language":[{"iso":"eng"}],"file_date_updated":"2019-08-07T09:03:48Z"},{"citation":{"bibtex":"@book{Bröcher_2016, title={Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer Softwarezertifizierung}, publisher={Universität Paderborn}, author={Bröcher, Henrik}, year={2016} }","short":"H. Bröcher, Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer Softwarezertifizierung, Universität Paderborn, 2016.","mla":"Bröcher, Henrik. <i>Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer Softwarezertifizierung</i>. Universität Paderborn, 2016.","apa":"Bröcher, H. (2016). <i>Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer Softwarezertifizierung</i>. Universität Paderborn.","ieee":"H. Bröcher, <i>Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer Softwarezertifizierung</i>. Universität Paderborn, 2016.","chicago":"Bröcher, Henrik. <i>Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer Softwarezertifizierung</i>. Universität Paderborn, 2016.","ama":"Bröcher H. <i>Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer Softwarezertifizierung</i>. Universität Paderborn; 2016."},"year":"2016","author":[{"last_name":"Bröcher","full_name":"Bröcher, Henrik","first_name":"Henrik"}],"supervisor":[{"last_name":"Wehrheim","full_name":"Wehrheim, Heike","first_name":"Heike"}],"date_created":"2017-10-17T12:41:31Z","publisher":"Universität Paderborn","date_updated":"2022-01-06T06:54:18Z","title":"Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer Softwarezertifizierung","type":"bachelorsthesis","status":"public","department":[{"_id":"77"}],"user_id":"15504","_id":"201","project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subprojekt B4"},{"name":"SFB 901 - Project Area B","_id":"3"}],"language":[{"iso":"ger"}]},{"ddc":["040"],"language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"Software verification is an established method to ensure software safety. Nevertheless, verification still often fails, either because it consumes too much resources, e.g., time or memory, or the technique is not mature enough to verify the property. Often then discarding the partial verification, the validation process proceeds with techniques like testing.To enable standard testing to profit from previous, partial verification, we use a summary of the verification effort to simplify the program for subsequent testing. Our techniques use this summary to construct a residual program which only contains program paths with unproven assertions. Afterwards, the residual program can be used with standard testing tools.Our first experiments show that testing profits from the partial verification.The test effort is reduced and combined verification and testing is faster than a complete verification."}],"file":[{"file_size":55775,"file_name":"186-SEsubmission8.pdf","access_level":"closed","file_id":"1532","date_updated":"2018-03-21T12:32:11Z","creator":"florida","date_created":"2018-03-21T12:32:11Z","success":1,"relation":"main_file","content_type":"application/pdf"}],"publication":"Software Engineering 2016","title":"Just test what you cannot verify!","date_created":"2017-10-17T12:41:28Z","year":"2016","file_date_updated":"2018-03-21T12:32:11Z","_id":"186","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"name":"SFB 901 - Project Area B","_id":"3"}],"department":[{"_id":"77"}],"user_id":"477","series_title":"Lecture Notes in Informatics","editor":[{"first_name":"Uwe Zdun","last_name":"Jens Knoop","full_name":"Jens Knoop, Uwe Zdun"}],"status":"public","type":"conference","date_updated":"2022-01-06T06:53:43Z","author":[{"first_name":"Mike","last_name":"Czech","full_name":"Czech, Mike"},{"last_name":"Jakobs","full_name":"Jakobs, Marie-Christine","first_name":"Marie-Christine"},{"last_name":"Wehrheim","full_name":"Wehrheim, Heike","id":"573","first_name":"Heike"}],"page":"17-18","citation":{"apa":"Czech, M., Jakobs, M.-C., &#38; Wehrheim, H. (2016). Just test what you cannot verify! In U. Z. Jens Knoop (Ed.), <i>Software Engineering 2016</i> (pp. 17–18).","bibtex":"@inproceedings{Czech_Jakobs_Wehrheim_2016, series={Lecture Notes in Informatics}, title={Just test what you cannot verify!}, booktitle={Software Engineering 2016}, author={Czech, Mike and Jakobs, Marie-Christine and Wehrheim, Heike}, editor={Jens Knoop, Uwe ZdunEditor}, year={2016}, pages={17–18}, collection={Lecture Notes in Informatics} }","short":"M. Czech, M.-C. Jakobs, H. Wehrheim, in: U.Z. Jens Knoop (Ed.), Software Engineering 2016, 2016, pp. 17–18.","mla":"Czech, Mike, et al. “Just Test What You Cannot Verify!” <i>Software Engineering 2016</i>, edited by Uwe Zdun Jens Knoop, 2016, pp. 17–18.","chicago":"Czech, Mike, Marie-Christine Jakobs, and Heike Wehrheim. “Just Test What You Cannot Verify!” In <i>Software Engineering 2016</i>, edited by Uwe Zdun Jens Knoop, 17–18. Lecture Notes in Informatics, 2016.","ieee":"M. Czech, M.-C. Jakobs, and H. Wehrheim, “Just test what you cannot verify!,” in <i>Software Engineering 2016</i>, 2016, pp. 17–18.","ama":"Czech M, Jakobs M-C, Wehrheim H. Just test what you cannot verify! In: Jens Knoop UZ, ed. <i>Software Engineering 2016</i>. Lecture Notes in Informatics. ; 2016:17-18."},"has_accepted_license":"1"},{"has_accepted_license":"1","page":"112--122","citation":{"ama":"Wiersema T, Bockhorn A, Platzner M. An Architecture and Design Tool Flow for Embedding a Virtual FPGA into a Reconfigurable System-on-Chip. <i>Computers &#38; Electrical Engineering</i>. 2016:112--122. doi:<a href=\"https://doi.org/10.1016/j.compeleceng.2016.04.005\">10.1016/j.compeleceng.2016.04.005</a>","chicago":"Wiersema, Tobias, Arne Bockhorn, and Marco Platzner. “An Architecture and Design Tool Flow for Embedding a Virtual FPGA into a Reconfigurable System-on-Chip.” <i>Computers &#38; Electrical Engineering</i>, 2016, 112--122. <a href=\"https://doi.org/10.1016/j.compeleceng.2016.04.005\">https://doi.org/10.1016/j.compeleceng.2016.04.005</a>.","ieee":"T. Wiersema, A. Bockhorn, and M. Platzner, “An Architecture and Design Tool Flow for Embedding a Virtual FPGA into a Reconfigurable System-on-Chip,” <i>Computers &#38; Electrical Engineering</i>, pp. 112--122, 2016.","bibtex":"@article{Wiersema_Bockhorn_Platzner_2016, title={An Architecture and Design Tool Flow for Embedding a Virtual FPGA into a Reconfigurable System-on-Chip}, DOI={<a href=\"https://doi.org/10.1016/j.compeleceng.2016.04.005\">10.1016/j.compeleceng.2016.04.005</a>}, journal={Computers &#38; Electrical Engineering}, publisher={Elsevier}, author={Wiersema, Tobias and Bockhorn, Arne and Platzner, Marco}, year={2016}, pages={112--122} }","short":"T. Wiersema, A. Bockhorn, M. Platzner, Computers &#38; Electrical Engineering (2016) 112--122.","mla":"Wiersema, Tobias, et al. “An Architecture and Design Tool Flow for Embedding a Virtual FPGA into a Reconfigurable System-on-Chip.” <i>Computers &#38; Electrical Engineering</i>, Elsevier, 2016, pp. 112--122, doi:<a href=\"https://doi.org/10.1016/j.compeleceng.2016.04.005\">10.1016/j.compeleceng.2016.04.005</a>.","apa":"Wiersema, T., Bockhorn, A., &#38; Platzner, M. (2016). An Architecture and Design Tool Flow for Embedding a Virtual FPGA into a Reconfigurable System-on-Chip. <i>Computers &#38; Electrical Engineering</i>, 112--122. <a href=\"https://doi.org/10.1016/j.compeleceng.2016.04.005\">https://doi.org/10.1016/j.compeleceng.2016.04.005</a>"},"year":"2016","date_created":"2017-10-17T12:41:35Z","author":[{"last_name":"Wiersema","full_name":"Wiersema, Tobias","id":"3118","first_name":"Tobias"},{"full_name":"Bockhorn, Arne","last_name":"Bockhorn","first_name":"Arne"},{"id":"398","full_name":"Platzner, Marco","last_name":"Platzner","first_name":"Marco"}],"date_updated":"2022-01-06T06:55:29Z","publisher":"Elsevier","doi":"10.1016/j.compeleceng.2016.04.005","title":"An Architecture and Design Tool Flow for Embedding a Virtual FPGA into a Reconfigurable System-on-Chip","publication":"Computers & Electrical Engineering","type":"journal_article","status":"public","file":[{"file_size":931048,"file_id":"1511","file_name":"222-1-s2.0-S0045790616300684-main.pdf","access_level":"closed","date_updated":"2018-03-21T10:36:08Z","date_created":"2018-03-21T10:36:08Z","creator":"florida","success":1,"relation":"main_file","content_type":"application/pdf"}],"abstract":[{"lang":"eng","text":"Virtual field programmable gate arrays (FPGA) 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, along with an analysis of the area and delay overheads involved."}],"department":[{"_id":"78"}],"user_id":"477","_id":"222","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-21T10:36:08Z","ddc":["040"]},{"_id":"227","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"name":"SFB 901 - Project Area B","_id":"3"}],"department":[{"_id":"77"}],"series_title":"LNCS","user_id":"477","file_date_updated":"2018-03-21T10:33:38Z","type":"conference","status":"public","date_updated":"2022-01-06T06:55:39Z","author":[{"first_name":"Manuel","id":"11315","full_name":"Töws, Manuel","last_name":"Töws"},{"first_name":"Heike","id":"573","full_name":"Wehrheim, Heike","last_name":"Wehrheim"}],"doi":"10.1007/978-3-319-47846-3_29","has_accepted_license":"1","page":"466--483","citation":{"ama":"Töws M, Wehrheim H. A CEGAR Scheme for Information Flow Analysis. In: <i>Proceedings of the 18th International Conference on Formal Engineering Methods (ICFEM 2016)</i>. LNCS. ; 2016:466--483. doi:<a href=\"https://doi.org/10.1007/978-3-319-47846-3_29\">10.1007/978-3-319-47846-3_29</a>","ieee":"M. Töws and H. Wehrheim, “A CEGAR Scheme for Information Flow Analysis,” in <i>Proceedings of the 18th International Conference on Formal Engineering Methods (ICFEM 2016)</i>, 2016, pp. 466--483.","chicago":"Töws, Manuel, and Heike Wehrheim. “A CEGAR Scheme for Information Flow Analysis.” In <i>Proceedings of the 18th International Conference on Formal Engineering Methods (ICFEM 2016)</i>, 466--483. LNCS, 2016. <a href=\"https://doi.org/10.1007/978-3-319-47846-3_29\">https://doi.org/10.1007/978-3-319-47846-3_29</a>.","apa":"Töws, M., &#38; Wehrheim, H. (2016). A CEGAR Scheme for Information Flow Analysis. In <i>Proceedings of the 18th International Conference on Formal Engineering Methods (ICFEM 2016)</i> (pp. 466--483). <a href=\"https://doi.org/10.1007/978-3-319-47846-3_29\">https://doi.org/10.1007/978-3-319-47846-3_29</a>","bibtex":"@inproceedings{Töws_Wehrheim_2016, series={LNCS}, title={A CEGAR Scheme for Information Flow Analysis}, DOI={<a href=\"https://doi.org/10.1007/978-3-319-47846-3_29\">10.1007/978-3-319-47846-3_29</a>}, booktitle={Proceedings of the 18th International Conference on Formal Engineering Methods (ICFEM 2016)}, author={Töws, Manuel and Wehrheim, Heike}, year={2016}, pages={466--483}, collection={LNCS} }","mla":"Töws, Manuel, and Heike Wehrheim. “A CEGAR Scheme for Information Flow Analysis.” <i>Proceedings of the 18th International Conference on Formal Engineering Methods (ICFEM 2016)</i>, 2016, pp. 466--483, doi:<a href=\"https://doi.org/10.1007/978-3-319-47846-3_29\">10.1007/978-3-319-47846-3_29</a>.","short":"M. Töws, H. Wehrheim, in: Proceedings of the 18th International Conference on Formal Engineering Methods (ICFEM 2016), 2016, pp. 466--483."},"ddc":["040"],"language":[{"iso":"eng"}],"publication":"Proceedings of the 18th International Conference on Formal Engineering Methods (ICFEM 2016)","abstract":[{"text":"Information flow analysis studies the flow of data between program entities (e.g. variables), where the allowed flow is specified via security policies. Typical information flow analyses compute a conservative (over-)approximation of the flows in a program. Such an analysis may thus signal non-existing violations of the security policy.In this paper, we propose a new technique for inspecting the reported violations (counterexamples) for spuriousity. Similar to counterexample-guided-abstraction-refinement (CEGAR) in software verification, we use the result of this inspection to improve the next round of the analysis. We prove soundness of this scheme.","lang":"eng"}],"file":[{"content_type":"application/pdf","success":1,"relation":"main_file","date_updated":"2018-03-21T10:33:38Z","date_created":"2018-03-21T10:33:38Z","creator":"florida","file_size":682849,"access_level":"closed","file_name":"227-chp_3A10.1007_2F978-3-319-47846-3_29.pdf","file_id":"1506"}],"date_created":"2017-10-17T12:41:36Z","title":"A CEGAR Scheme for Information Flow Analysis","year":"2016"},{"has_accepted_license":"1","year":"2016","citation":{"ieee":"J. Späth, L. Nguyen Quang Do, K. Ali, and E. Bodden, “Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java,” in <i>European Conference on Object-Oriented Programming (ECOOP)</i>, 2016.","chicago":"Späth, Johannes, Lisa Nguyen Quang Do, Karim Ali, and Eric Bodden. “Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java.” In <i>European Conference on Object-Oriented Programming (ECOOP)</i>, 2016.","ama":"Späth J, Nguyen Quang Do L, Ali K, Bodden E. Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java. In: <i>European Conference on Object-Oriented Programming (ECOOP)</i>. ; 2016.","apa":"Späth, J., Nguyen Quang Do, L., Ali, K., &#38; Bodden, E. (2016). Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java. In <i>European Conference on Object-Oriented Programming (ECOOP)</i>.","bibtex":"@inproceedings{Späth_Nguyen Quang Do_Ali_Bodden_2016, title={Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java}, booktitle={European Conference on Object-Oriented Programming (ECOOP)}, author={Späth, Johannes and Nguyen Quang Do, Lisa and Ali, Karim and Bodden, Eric}, year={2016} }","mla":"Späth, Johannes, et al. “Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java.” <i>European Conference on Object-Oriented Programming (ECOOP)</i>, 2016.","short":"J. Späth, L. Nguyen Quang Do, K. Ali, E. Bodden, in: European Conference on Object-Oriented Programming (ECOOP), 2016."},"date_updated":"2022-01-06T07:01:45Z","date_created":"2018-10-31T12:51:26Z","author":[{"last_name":"Späth","full_name":"Späth, Johannes","first_name":"Johannes"},{"full_name":"Nguyen Quang Do, Lisa","last_name":"Nguyen Quang Do","first_name":"Lisa"},{"last_name":"Ali","full_name":"Ali, Karim","first_name":"Karim"},{"first_name":"Eric","orcid":"0000-0003-3470-3647","last_name":"Bodden","id":"59256","full_name":"Bodden, Eric"}],"title":"Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java","main_file_link":[{"url":"http://www.bodden.de/pubs/sna+16boomerang.pdf"}],"publication":"European Conference on Object-Oriented Programming (ECOOP)","type":"conference","status":"public","file":[{"relation":"main_file","success":1,"content_type":"application/pdf","access_level":"closed","file_name":"sna+16boomerang.pdf","file_id":"5265","file_size":1921617,"date_created":"2018-11-02T14:13:19Z","creator":"ups","date_updated":"2018-11-02T14:13:19Z"}],"_id":"5205","project":[{"name":"SFB 901","_id":"1"},{"name":"SFB 901 - Project Area B","_id":"3"},{"_id":"12","name":"SFB 901 - Subproject B4"}],"department":[{"_id":"76"}],"user_id":"477","keyword":["ATTRACT","ITSECWEBSITE"],"ddc":["000"],"file_date_updated":"2018-11-02T14:13:19Z","language":[{"iso":"eng"}]},{"title":"PAndA 2 : Analyzing Permission Use and Interplay in Android Apps (Tool Paper)","author":[{"full_name":"Jakobs, Marie-Christine","last_name":"Jakobs","first_name":"Marie-Christine"},{"first_name":"Manuel","last_name":"Töws","id":"11315","full_name":"Töws, Manuel"},{"first_name":"Felix","id":"22398","full_name":"Pauck, Felix","last_name":"Pauck"}],"date_created":"2017-10-17T12:41:25Z","date_updated":"2022-01-06T06:53:01Z","citation":{"short":"M.-C. Jakobs, M. Töws, F. Pauck, in: T.E. Ishikawa F, Romanovsky A (Ed.), Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems, 2016.","bibtex":"@inproceedings{Jakobs_Töws_Pauck_2016, series={School of Computing Science Technical Report Series}, title={PAndA 2 : Analyzing Permission Use and Interplay in Android Apps (Tool Paper)}, booktitle={Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems}, author={Jakobs, Marie-Christine and Töws, Manuel and Pauck, Felix}, editor={Ishikawa F, Romanovsky A, Troubitsyna EEditor}, year={2016}, collection={School of Computing Science Technical Report Series} }","mla":"Jakobs, Marie-Christine, et al. “PAndA 2 : Analyzing Permission Use and Interplay in Android Apps (Tool Paper).” <i>Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems</i>, edited by Troubitsyna E Ishikawa F, Romanovsky A, 2016.","apa":"Jakobs, M.-C., Töws, M., &#38; Pauck, F. (2016). PAndA 2 : Analyzing Permission Use and Interplay in Android Apps (Tool Paper). In T. E. Ishikawa F, Romanovsky A (Ed.), <i>Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems</i>.","ieee":"M.-C. Jakobs, M. Töws, and F. Pauck, “PAndA 2 : Analyzing Permission Use and Interplay in Android Apps (Tool Paper),” in <i>Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems</i>, 2016.","chicago":"Jakobs, Marie-Christine, Manuel Töws, and Felix Pauck. “PAndA 2 : Analyzing Permission Use and Interplay in Android Apps (Tool Paper).” In <i>Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems</i>, edited by Troubitsyna E Ishikawa F, Romanovsky A. School of Computing Science Technical Report Series, 2016.","ama":"Jakobs M-C, Töws M, Pauck F. PAndA 2 : Analyzing Permission Use and Interplay in Android Apps (Tool Paper). In: Ishikawa F, Romanovsky A TE, ed. <i>Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems</i>. School of Computing Science Technical Report Series. ; 2016."},"year":"2016","related_material":{"link":[{"relation":"contains","url":"https://pdfs.semanticscholar.org/58cd/94c8b2335d16aa2558f711cf81b3f7746696.pdf"}]},"has_accepted_license":"1","file_date_updated":"2018-03-21T12:40:27Z","ddc":["040"],"department":[{"_id":"77"}],"series_title":"School of Computing Science Technical Report Series","user_id":"15504","_id":"170","project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Subprojekt B4","_id":"12"},{"_id":"3","name":"SFB 901 - Project Area B"}],"status":"public","file":[{"file_name":"170-main_04.pdf","file_id":"1539","access_level":"closed","file_size":285299,"creator":"florida","date_created":"2018-03-21T12:40:27Z","date_updated":"2018-03-21T12:40:27Z","relation":"main_file","success":1,"content_type":"application/pdf"}],"abstract":[{"text":"We present PAndA2, an extendable, static analysis tool for Android  apps  which  examines  permission  related security  threats  like overprivilege, existence of permission redelegation and permission flows. PAndA2 comes along with a textual and graphical visualization of the analysis result and even supports the comparison of analysis results for different android app versions.","lang":"eng"}],"editor":[{"first_name":"Troubitsyna E","full_name":"Ishikawa F, Romanovsky A, Troubitsyna E","last_name":"Ishikawa F, Romanovsky A"}],"publication":"Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems","type":"conference"},{"file_date_updated":"2018-03-08T09:14:11Z","ddc":["040"],"department":[{"_id":"77"}],"user_id":"477","_id":"1190","project":[{"name":"SFB 901","_id":"1"},{"_id":"12","name":"SFB 901 - Subproject B4"},{"_id":"3","name":"SFB 901 - Project Area B"}],"status":"public","file":[{"relation":"main_file","content_type":"application/pdf","file_name":"1190-thesis_abgabeversion.pdf","access_level":"closed","file_id":"1195","file_size":3354335,"creator":"florida","date_created":"2018-03-08T06:23:21Z","date_updated":"2018-03-08T09:14:11Z"}],"type":"dissertation","title":"Induction-based Verification of Timed Systems","supervisor":[{"first_name":"Heike","last_name":"Wehrheim","id":"573","full_name":"Wehrheim, Heike"}],"author":[{"full_name":"Isenberg, Tobias","last_name":"Isenberg","first_name":"Tobias"}],"date_created":"2018-03-05T10:11:48Z","date_updated":"2022-01-06T06:51:12Z","publisher":"Universität Paderborn","citation":{"short":"T. Isenberg, Induction-Based Verification of Timed Systems, Universität Paderborn, 2016.","bibtex":"@book{Isenberg_2016, title={Induction-based Verification of Timed Systems}, publisher={Universität Paderborn}, author={Isenberg, Tobias}, year={2016} }","mla":"Isenberg, Tobias. <i>Induction-Based Verification of Timed Systems</i>. Universität Paderborn, 2016.","apa":"Isenberg, T. (2016). <i>Induction-based Verification of Timed Systems</i>. Universität Paderborn.","chicago":"Isenberg, Tobias. <i>Induction-Based Verification of Timed Systems</i>. Universität Paderborn, 2016.","ieee":"T. Isenberg, <i>Induction-based Verification of Timed Systems</i>. Universität Paderborn, 2016.","ama":"Isenberg T. <i>Induction-Based Verification of Timed Systems</i>. Universität Paderborn; 2016."},"year":"2016","has_accepted_license":"1"}]