@inproceedings{3287, abstract = {{For optimal placement and orchestration of network services, it is crucial that their structure and semantics are specified clearly and comprehensively and are available to an orchestrator. Existing specification approaches are either ambiguous or miss important aspects regarding the behavior of virtual network functions (VNFs) forming a service. We propose to formally and unambiguously specify the behavior of these functions and services using Queuing Petri Nets (QPNs). QPNs are an established method that allows to express queuing, synchronization, stochastically distributed processing delays, and changing traffic volume and characteristics at each VNF. With QPNs, multiple VNFs can be connected to complete network services in any structure, even specifying bidirectional network services containing loops. We discuss how management and orchestration systems can benefit from our clear and comprehensive specification approach, leading to better placement of VNFs and improved Quality of Service. Another benefit of formally specifying network services with QPNs are diverse analysis options, which allow valuable insights such as the distribution of end-to-end delay. We propose a tool-based workflow that supports the specification of network services and the automatic generation of corresponding simulation code to enable an in-depth analysis of their behavior and performance.}}, author = {{Schneider, Stefan Balthasar and Sharma, Arnab and Karl, Holger and Wehrheim, Heike}}, booktitle = {{2019 IFIP/IEEE International Symposium on Integrated Network Management (IM)}}, location = {{Washington, DC, USA}}, pages = {{116----124}}, publisher = {{IFIP}}, title = {{{Specifying and Analyzing Virtual Network Services Using Queuing Petri Nets}}}, year = {{2019}}, } @inproceedings{7752, author = {{Sharma, Arnab and Wehrheim, Heike}}, booktitle = {{Proceedings of the Software Engineering Conference (SE)}}, isbn = {{978-3-88579-686-2}}, location = {{Stuttgart}}, pages = {{157 -- 158}}, publisher = {{Gesellschaft für Informatik e.V. (GI)}}, title = {{{Testing Balancedness of ML Algorithms}}}, volume = {{P-292}}, year = {{2019}}, } @misc{7623, author = {{Zhang, Shikun}}, pages = {{64}}, publisher = {{Universität Paderborn}}, title = {{{Combining Android Apps for Analysis Purposes}}}, year = {{2019}}, } @inproceedings{7635, author = {{Sharma, Arnab and Wehrheim, Heike}}, booktitle = {{IEEE International Conference on Software Testing, Verification and Validation (ICST)}}, location = {{Xi'an, China, April, 2019}}, pages = {{125----135}}, publisher = {{IEEE}}, title = {{{Testing Machine Learning Algorithms for Balanced Data Usage}}}, year = {{2019}}, } @misc{12885, author = {{Haltermann, Jan Frederik}}, title = {{{Analyzing Data Usage in Array Programs}}}, year = {{2019}}, } @inproceedings{15838, abstract = {{In the field of software analysis a trade-off between scalability and accuracy always exists. In this respect, Android app analysis is no exception, in particular, analyzing large or many apps can be challenging. Dealing with many small apps is a typical challenge when facing micro-benchmarks such as DROIDBENCH or ICC-BENCH. These particular benchmarks are not only used for the evaluation of novel tools but also in continuous integration pipelines of existing mature tools to maintain and guarantee a certain quality-level. Considering this latter usage it becomes very important to be able to achieve benchmark results as fast as possible. Hence, benchmarks have to be optimized for this purpose. One approach to do so is app merging. We implemented the Android Merge Tool (AMT) following this approach and show that its novel aspects can be used to produce scaled up and accurate benchmarks. For such benchmarks Android app analysis tools do not suffer from the scalability-accuracy trade-off anymore. We show this throughout detailed experiments on DROIDBENCH employing three different analysis tools (AMANDROID, ICCTA, FLOWDROID). Benchmark execution times are largely reduced without losing benchmark accuracy. Moreover, we argue why AMT is an advantageous successor of the state-of-the-art app merging tool (APKCOMBINER) in analysis lift-up scenarios.}}, author = {{Pauck, Felix and Zhang, Shikun}}, booktitle = {{2019 34th IEEE/ACM International Conference on Automated Software Engineering Workshop (ASEW)}}, isbn = {{9781728141367}}, keywords = {{Program Analysis, Android App Analysis, Taint Analysis, App Merging, Benchmark}}, title = {{{Android App Merging for Benchmark Speed-Up and Analysis Lift-Up}}}, doi = {{10.1109/asew.2019.00019}}, year = {{2019}}, } @inproceedings{16215, author = {{Derrick, John and Doherty, Simon and Dongol, Brijesh and Schellhorn, Gerhard and Wehrheim, Heike}}, booktitle = {{Formal Methods - The Next 30 Years - Third World Congress, {FM} 2019, Porto, Portugal, October 7-11, 2019, Proceedings}}, editor = {{H. ter Beek, Maurice and McIver, Annabelle and N. Oliveira, Jos{\'{e}}}}, pages = {{179--195}}, publisher = {{Springer}}, title = {{{Verifying Correctness of Persistent Concurrent Data Structures}}}, doi = {{10.1007/978-3-030-30942-8\_12}}, volume = {{11800}}, year = {{2019}}, } @article{16216, author = {{Russo, Alessandra and Schürr, Andy and Wehrheim, Heike}}, journal = {{Formal Asp. Comput.}}, number = {{5}}, pages = {{457--458}}, title = {{{Editorial}}}, doi = {{10.1007/s00165-019-00495-y}}, volume = {{31}}, year = {{2019}}, } @article{16217, author = {{Fränzle, Martin and Kapur, Deepak and Wehrheim, Heike and Zhan, Naijun}}, journal = {{Formal Asp. Comput.}}, number = {{1}}, pages = {{1}}, title = {{{Editorial}}}, doi = {{10.1007/s00165-018-00477-6}}, volume = {{31}}, year = {{2019}}, } @inbook{13872, author = {{Beyer, Dirk and Jakobs, Marie-Christine}}, booktitle = {{Fundamental Approaches to Software Engineering}}, isbn = {{9783030167219}}, issn = {{0302-9743}}, title = {{{CoVeriTest: Cooperative Verifier-Based Testing}}}, doi = {{10.1007/978-3-030-16722-6_23}}, year = {{2019}}, } @inproceedings{13993, author = {{Derrick, John and Doherty, Simon and Dongol, Brijesh and Schellhorn, Gerhard and Wehrheim, Heike}}, booktitle = {{Formal Methods - The Next 30 Years - Third World Congress, {FM} 2019, Porto, Portugal, October 7-11, 2019, Proceedings}}, pages = {{179--195}}, title = {{{Verifying Correctness of Persistent Concurrent Data Structures}}}, doi = {{10.1007/978-3-030-30942-8\_12}}, year = {{2019}}, } @article{10011, author = {{Fränzle, Martin and Kapur, Deepak and Wehrheim, Heike and Zhan, Naijun}}, journal = {{Formal Asp. Comput.}}, number = {{1}}, pages = {{1}}, title = {{{Editorial}}}, doi = {{10.1007/s00165-018-00477-6}}, volume = {{31}}, year = {{2019}}, } @inproceedings{10091, author = {{König, Jürgen and Wehrheim, Heike}}, booktitle = {{{NASA} Formal Methods - 11th International Symposium, {NFM} 2019, Houston, TX, USA, May 7-9, 2019, Proceedings}}, editor = {{M. Badger, Julia and Yvonne Rozier, Kristin}}, pages = {{263--279}}, publisher = {{Springer}}, title = {{{Data Independence for Software Transactional Memory}}}, doi = {{10.1007/978-3-030-20652-9\_18}}, volume = {{11460}}, year = {{2019}}, } @inproceedings{10092, author = {{Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike and Derrick, John}}, booktitle = {{Proceedings of the 24th {ACM} {SIGPLAN} Symposium on Principles and Practice of Parallel Programming, PPoPP 2019, Washington, DC, USA, February 16-20, 2019}}, editor = {{K. Hollingsworth, Jeffrey and Keidar, Idit}}, pages = {{355--365}}, publisher = {{{ACM}}}, title = {{{Verifying C11 programs operationally}}}, doi = {{10.1145/3293883.3295702}}, year = {{2019}}, } @inproceedings{10093, author = {{Beyer, Dirk and Jakobs, Marie-Christine and Lemberger, Thomas and Wehrheim, Heike}}, booktitle = {{Software Engineering and Software Management (SE/SWM 2019), Stuttgart, Germany, February 18-22, 2019}}, editor = {{Becker, Steffen and Bogicevic, Ivan and Herzwurm, Georg and Wagner, Stefan}}, pages = {{151----152}}, publisher = {{GI}}, title = {{{Combining Verifiers in Conditional Model Checking via Reducers}}}, doi = {{10.18420/se2019-46}}, volume = {{P-292}}, year = {{2019}}, } @inproceedings{10094, author = {{Sharma, Arnab and Wehrheim, Heike}}, booktitle = {{Software Engineering and Software Management, {SE/SWM} 2019, Stuttgart, Germany, February 18-22, 2019}}, editor = {{Becker, Steffen and Bogicevic, Ivan and Herzwurm, Georg and Wagner, Stefan}}, pages = {{157--158}}, publisher = {{{GI}}}, title = {{{Testing Balancedness of ML Algorithms}}}, doi = {{10.18420/se2019-48}}, volume = {{{P-292}}}, year = {{2019}}, } @inproceedings{10095, author = {{Richter, Cedric and Wehrheim, Heike}}, booktitle = {{Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {III}}}, editor = {{Beyer, Dirk and Huisman, Marieke and Kordon, Fabrice and Steffen, Bernhard}}, pages = {{229--233}}, publisher = {{Springer}}, title = {{{PeSCo: Predicting Sequential Combinations of Verifiers - (Competition Contribution)}}}, doi = {{10.1007/978-3-030-17502-3_19}}, volume = {{11429}}, year = {{2019}}, } @misc{10105, author = {{Haltermann, Jan}}, publisher = {{Universität Paderborn}}, title = {{{Analyzing Data Usage in Array Programs}}}, year = {{2019}}, } @inproceedings{10108, abstract = {{Recent years have seen the development of numerous tools for the analysis of taint flows in Android apps. Taint analyses aim at detecting data leaks, accidentally or by purpose programmed into apps. Often, such tools specialize in the treatment of specific features impeding precise taint analysis (like reflection or inter-app communication). This multitude of tools, their specific applicability and their various combination options complicate the selection of a tool (or multiple tools) when faced with an analysis instance, even for knowledgeable users, and hence hinders the successful adoption of taint analyses. In this work, we thus present CoDiDroid, a framework for cooperative Android app analysis. CoDiDroid (1) allows users to ask questions about flows in apps in varying degrees of detail, (2) automatically generates subtasks for answering such questions, (3) distributes tasks onto analysis tools (currently DroidRA, FlowDroid, HornDroid, IC3 and two novel tools) and (4) at the end merges tool answers on subtasks into an overall answer. Thereby, users are freed from having to learn about the use and functionality of all these tools while still being able to leverage their capabilities. Moreover, we experimentally show that cooperation among tools pays off with respect to effectiveness, precision and scalability.}}, author = {{Pauck, Felix and Wehrheim, Heike}}, booktitle = {{Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering}}, isbn = {{978-1-4503-5572-8}}, keywords = {{Android Taint Analysis, Cooperation, Precision, Tools}}, pages = {{374--384}}, title = {{{Together Strong: Cooperative Android App Analysis}}}, doi = {{10.1145/3338906.3338915}}, year = {{2019}}, } @inproceedings{13874, author = {{Isenberg, Tobias and Jakobs, Marie-Christine and Pauck, Felix and Wehrheim, Heike}}, booktitle = {{Tests and Proofs - 13th International Conference, {TAP} 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings}}, pages = {{3--20}}, title = {{{When Are Software Verification Results Valid for Approximate Hardware?}}}, doi = {{10.1007/978-3-030-31157-5_1}}, year = {{2019}}, }