@article{20279, author = {{Sharma, Arnab and Wehrheim, Heike}}, journal = {{CoRR}}, title = {{{Testing Monotonicity of Machine Learning Models}}}, volume = {{abs/2002.12278}}, year = {{2020}}, } @article{21016, author = {{Dalvandi, Sadegh and Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike}}, journal = {{Dagstuhl Artifacts Ser.}}, number = {{2}}, pages = {{15:1--15:2}}, title = {{{Owicki-Gries Reasoning for C11 RAR (Artifact)}}}, doi = {{10.4230/DARTS.6.2.15}}, volume = {{6}}, year = {{2020}}, } @inproceedings{21017, author = {{Dalvandi, Sadegh and Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike}}, booktitle = {{34th European Conference on Object-Oriented Programming, {ECOOP} 2020, November 15-17, 2020, Berlin, Germany (Virtual Conference)}}, editor = {{Hirschfeld, Robert and Pape, Tobias}}, pages = {{11:1--11:26}}, publisher = {{Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}}, title = {{{Owicki-Gries Reasoning for C11 RAR}}}, doi = {{10.4230/LIPIcs.ECOOP.2020.11}}, volume = {{166}}, year = {{2020}}, } @inproceedings{21018, author = {{Richter, Cedric and Wehrheim, Heike}}, booktitle = {{35th {IEEE/ACM} International Conference on Automated Software Engineering, {ASE} 2020, Melbourne, Australia, September 21-25, 2020}}, pages = {{1016--1028}}, publisher = {{{IEEE}}}, title = {{{Attend and Represent: A Novel View on Algorithm Selection for Software Verification}}}, year = {{2020}}, } @proceedings{21019, editor = {{Ahrendt, Wolfgang and Wehrheim, Heike}}, isbn = {{978-3-030-50994-1}}, publisher = {{Springer}}, title = {{{Tests and Proofs - 14th International Conference, TAP@STAF 2020, Bergen, Norway, June 22-23, 2020, Proceedings [postponed]}}}, doi = {{10.1007/978-3-030-50995-8}}, volume = {{12165}}, year = {{2020}}, } @unpublished{17825, abstract = {{Software verification has recently made enormous progress due to the development of novel verification methods and the speed-up of supporting technologies like SMT solving. To keep software verification tools up to date with these advances, tool developers keep on integrating newly designed methods into their tools, almost exclusively by re-implementing the method within their own framework. While this allows for a conceptual re-use of methods, it requires novel implementations for every new technique. In this paper, we employ cooperative verification in order to avoid reimplementation and enable usage of novel tools as black-box components in verification. Specifically, cooperation is employed for the core ingredient of software verification which is invariant generation. Finding an adequate loop invariant is key to the success of a verification run. Our framework named CoVerCIG allows a master verification tool to delegate the task of invariant generation to one or several specialized helper invariant generators. Their results are then utilized within the verification run of the master verifier, allowing in particular for crosschecking the validity of the invariant. We experimentally evaluate our framework on an instance with two masters and three different invariant generators using a number of benchmarks from SV-COMP 2020. The experiments show that the use of CoVerCIG can increase the number of correctly verified tasks without increasing the used resources}}, author = {{Haltermann, Jan Frederik and Wehrheim, Heike}}, booktitle = {{arXiv:2008.04551}}, title = {{{Cooperative Verification via Collective Invariant Generation}}}, year = {{2020}}, } @inproceedings{16724, author = {{Sharma, Arnab and Wehrheim, Heike}}, booktitle = {{Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA).}}, publisher = {{ACM}}, title = {{{Higher Income, Larger Loan? Monotonicity Testing of Machine Learning Models}}}, year = {{2020}}, } @article{16725, author = {{Richter, Cedric and Hüllermeier, Eyke and Jakobs, Marie-Christine and Wehrheim, Heike}}, journal = {{Journal of Automated Software Engineering}}, publisher = {{Springer}}, title = {{{Algorithm Selection for Software Validation Based on Graph Kernels}}}, year = {{2020}}, } @article{13770, author = {{Karl, Holger and Kundisch, Dennis and Meyer auf der Heide, Friedhelm and Wehrheim, Heike}}, journal = {{Business & Information Systems Engineering}}, number = {{6}}, pages = {{467--481}}, publisher = {{Springer}}, title = {{{A Case for a New IT Ecosystem: On-The-Fly Computing}}}, doi = {{10.1007/s12599-019-00627-x}}, volume = {{62}}, year = {{2020}}, } @inproceedings{16214, author = {{Pauck, Felix and Bodden, Eric and Wehrheim, Heike}}, booktitle = {{Software Engineering 2020, Fachtagung des GI-Fachbereichs Softwaretechnik, 24.-28. Februar 2020, Innsbruck, Austria}}, editor = {{Felderer, Michael and Hasselbring, Wilhelm and Rabiser, Rick and Jung, Reiner}}, pages = {{123--124}}, publisher = {{Gesellschaft f{\"{u}}r Informatik e.V.}}, title = {{{Reproducing Taint-Analysis Results with ReproDroid}}}, doi = {{10.18420/SE2020_36}}, year = {{2020}}, } @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}}, }