Testing Monotonicity of Machine Learning Models - Sharma, Arnab; Wehrheim, Heike (CoRR)

Owicki-Gries Reasoning for C11 RAR (Artifact) - Dalvandi, Sadegh; Doherty, Simon; Dongol, Brijesh; Wehrheim, Heike (Dagstuhl Artifacts Ser.)

Owicki-Gries Reasoning for C11 RAR - Dalvandi, Sadegh; Doherty, Simon; Dongol, Brijesh; Wehrheim, Heike (34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15-17, 2020, Berlin, Germany (Virtual Conference))

Attend and Represent: A Novel View on Algorithm Selection for Software Verification - Richter, Cedric; Wehrheim, Heike (35th {IEEE/ACM} International Conference on Automated Software Engineering, ASE 2020, Melbourne, Australia, September 21-25, 2020)

Tests and Proofs - 14th International Conference, TAP@STAF 2020, Bergen, Norway, June 22-23, 2020, Proceedings [postponed]

Cooperative Verification via Collective Invariant Generation - Haltermann, Jan Frederik; Wehrheim, Heike (arXiv:2008.04551)
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

Higher Income, Larger Loan? Monotonicity Testing of Machine Learning Models - Sharma, Arnab; Wehrheim, Heike (Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA).)

Algorithm Selection for Software Validation Based on Graph Kernels - Richter, Cedric; Hüllermeier, Eyke; Jakobs, Marie-Christine; Wehrheim, Heike (Journal of Automated Software Engineering)

A Case for a New IT Ecosystem: On-The-Fly Computing - Karl, Holger; Kundisch, Dennis; Meyer auf der Heide, Friedhelm; Wehrheim, Heike (Business & Information Systems Engineering)

Reproducing Taint-Analysis Results with ReproDroid - Pauck, Felix; Bodden, Eric; Wehrheim, Heike (Software Engineering 2020, Fachtagung des GI-Fachbereichs Softwaretechnik, 24.-28. Februar 2020, Innsbruck, Austria)

Specifying and Analyzing Virtual Network Services Using Queuing Petri Nets - Schneider, Stefan Balthasar; Sharma, Arnab; Karl, Holger; Wehrheim, Heike (2019 IFIP/IEEE International Symposium on Integrated Network Management (IM))
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.

Testing Balancedness of ML Algorithms - Sharma, Arnab; Wehrheim, Heike (Proceedings of the Software Engineering Conference (SE))

Combining Android Apps for Analysis Purposes - Zhang, Shikun

Testing Machine Learning Algorithms for Balanced Data Usage - Sharma, Arnab; Wehrheim, Heike (IEEE International Conference on Software Testing, Verification and Validation (ICST))

Analyzing Data Usage in Array Programs - Haltermann, Jan Frederik

Android App Merging for Benchmark Speed-Up and Analysis Lift-Up - Pauck, Felix; Zhang, Shikun (2019 34th IEEE/ACM International Conference on Automated Software Engineering Workshop (ASEW))
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.
Keywords: Program Analysis; Android App Analysis; Taint Analysis; App Merging; Benchmark

Verifying Correctness of Persistent Concurrent Data Structures - Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Wehrheim, Heike (Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings)

Editorial - Russo, Alessandra; Schürr, Andy; Wehrheim, Heike (Formal Asp. Comput.)

Editorial - Fränzle, Martin; Kapur, Deepak; Wehrheim, Heike; Zhan, Naijun (Formal Asp. Comput.)

CoVeriTest: Cooperative Verifier-Based Testing - Beyer, Dirk; Jakobs, Marie-Christine (Fundamental Approaches to Software Engineering)

Verifying Correctness of Persistent Concurrent Data Structures - Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Wehrheim, Heike (Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings)

Editorial - Fränzle, Martin; Kapur, Deepak; Wehrheim, Heike; Zhan, Naijun (Formal Asp. Comput.)

Data Independence for Software Transactional Memory - König, Jürgen; Wehrheim, Heike (NASA Formal Methods - 11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings)

Verifying C11 programs operationally - Doherty, Simon; Dongol, Brijesh; Wehrheim, Heike; Derrick, John (Proceedings of the 24th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2019, Washington, DC, USA, February 16-20, 2019)

Combining Verifiers in Conditional Model Checking via Reducers - Beyer, Dirk; Jakobs, Marie-Christine; Lemberger, Thomas; Wehrheim, Heike (Software Engineering and Software Management (SE/SWM 2019), Stuttgart, Germany, February 18-22, 2019)

Testing Balancedness of ML Algorithms - Sharma, Arnab; Wehrheim, Heike (Software Engineering and Software Management, {SE/SWM} 2019, Stuttgart, Germany, February 18-22, 2019)

PeSCo: Predicting Sequential Combinations of Verifiers - (Competition Contribution) - Richter, Cedric; Wehrheim, Heike (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)

Analyzing Data Usage in Array Programs - Haltermann, Jan

Together Strong: Cooperative Android App Analysis - Pauck, Felix; Wehrheim, Heike (Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering)
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.
Keywords: Android Taint Analysis; Cooperation; Precision; Tools

When Are Software Verification Results Valid for Approximate Hardware? - Isenberg, Tobias; Jakobs, Marie-Christine; Pauck, Felix; Wehrheim, Heike (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)

Korrektheitsbeweise für Muster von Servicekompositionen - Rautenberg, Kai

JMCTest: Automatically Testing Inter-Method Contracts in Java - Börding, Paul; Haltermann, Jan Frederik; Jakobs, Marie-Christine; Wehrheim, Heike (Proceedings of the IFIP International Conference on Testing Software and Systems (ICTSS 2018))
Over the years, Design by Contract (DbC) has evolved as a powerful concept for program documentation, testing, and verification. Contracts formally specify assertions on (mostly) object-oriented programs: pre- and postconditions of methods, class invariants, allowed call orders, etc. Missing in the long list of properties specifiable by contracts are, however, method correlations: DbC languages fall short on stating assertions relating methods. In this paper, we propose the novel concept of inter-method contract, allowing precisely for expressing method correlations.We present JMC as a language for specifying and JMCTest as a tool for dynamically checking inter-method contracts on Java programs. JMCTest fully automatically generates objects on which the contracted methods are called and the validity of the contract is checked. Using JMCTest, we detected that large Java code bases (e.g. JBoss, Java RT) frequently violate standard inter-method contracts. In comparison to other verification tools inspecting (some) inter-method contracts, JMCTest can find bugs that remain undetected by those tools.

FastLane Is Opaque – a Case Study in Mechanized Proofs of Opacity - Schellhorn, Gerhard; Wedel, Monika; Travkin, Oleg; König, Jürgen; Wehrheim, Heike (Software Engineering and Formal Methods)

Causal Linearizability: Compositionality for Partially Ordered Executions - Doherty, Simon; Derrick, John; Dongol, Brijesh; Wehrheim, Heike (CoRR)

Do Android Taint Analysis Tools Keep their Promises? - Pauck, Felix; Bodden, Eric; Wehrheim, Heike (arXiv:1804.02903)
In recent years, researchers have developed a number of tools to conduct taint analysis of Android applications. While all the respective papers aim at providing a thorough empirical evaluation, comparability is hindered by varying or unclear evaluation targets. Sometimes, the apps used for evaluation are not precisely described. In other cases, authors use an established benchmark but cover it only partially. In yet other cases, the evaluations differ in terms of the data leaks searched for, or lack a ground truth to compare against. All those limitations make it impossible to truly compare the tools based on those published evaluations. We thus present ReproDroid, a framework allowing the accurate comparison of Android taint analysis tools. ReproDroid supports researchers in inferring the ground truth for data leaks in apps, in automatically applying tools to benchmarks, and in evaluating the obtained results. We use ReproDroid to comparatively evaluate on equal grounds the six prominent taint analysis tools Amandroid, DIALDroid, DidFail, DroidSafe, FlowDroid and IccTA. The results are largely positive although four tools violate some promises concerning features and accuracy. Finally, we contribute to the area of unbiased benchmarking with a new and improved version of the open test suite DroidBench.

Information Flow Certificates - Töws, Manuel; Wehrheim, Heike (Theoretical Aspects of Computing – ICTAC 2018)
Information flow analysis investigates the flow of data in applications, checking in particular for flows from private sources to public sinks. Flow- and path-sensitive analyses are, however, often too costly to be performed every time a security-critical application is run. In this paper, we propose a variant of proof carrying code for information flow security. To this end, we develop information flow (IF) certificates which get attached to programs as well as a method for IF certificate validation. We prove soundness of our technique, i.e., show it to be tamper-free. The technique is implemented within the program analysis tool CPAchecker. Our experiments confirm that the use of certificates pays off for costly analysis runs.

Do Android taint analysis tools keep their promises? - Pauck, Felix; Bodden, Eric; Wehrheim, Heike (Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering - ESEC/FSE 2018)

Mechanized proofs of opacity: a comparison of two techniques - Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike (Formal Asp. Comput.)

Making Linearizability Compositional for Partially Ordered Executions - Doherty, Simon; Dongol, Brijesh; Wehrheim, Heike; Derrick, John (Integrated Formal Methods - 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings)

Making Linearizability Compositional for Partially Ordered Executions - Doherty, Simon; Dongol, Brijesh; Wehrheim, Heike; Derrick, John (Integrated Formal Methods - 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings)

Brief Announcement: Generalising Concurrent Correctness to Weak Memory - Doherty, Simon; Dongol, Brijesh; Wehrheim, Heike; Derrick, John (32nd International Symposium on Distributed Computing, DISC 2018, New Orleans, LA, USA, October 15-19, 2018)

Validity of Software Verification Results on Approximate Hardware - Isenberg, Tobias; Jakobs, Marie-Christine; Pauck, Felix; Wehrheim, Heike (IEEE Embedded Systems Letters)
Approximate computing (AC) is an emerging paradigm for energy-efficient computation. The basic idea of AC is to sacrifice high precision for low energy by allowing hardware to carry out “approximately correct” calculations. This provides a major challenge for software quality assurance: programs successfully verified to be correct might be erroneous on approximate hardware. In this letter, we present a novel approach for determining under what conditions a software verification result is valid for approximate hardware. To this end, we compute the allowed tolerances for AC hardware from successful verification runs. More precisely, we derive a set of constraints which—when met by the AC hardware—guarantees the verification result to carry over to AC. On the practical side, we furthermore: 1) show how to extract tolerances from verification runs employing predicate abstraction as verification technology and 2) show how to check such constraints on hardware designs. We have implemented all techniques, and exemplify them on example C programs and a number of recently proposed approximate adders.

Reducer-Based Construction of Conditional Verifiers - Beyer, Dirk; Jakobs, Marie-Christine; Lemberger, Thomas; Wehrheim, Heike (Proceedings of the 40th International Conference on Software Engineering (ICSE))
to appear

Testing Java Method Contracts - Börding, Paul

Policy Dependent and Independent Information Flow Analyses - Töws, Manuel; Wehrheim, Heike (Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an, China, November 13-17, 2017, Proceedings)

Value-Based or Conflict-Based? Opacity Definitions for STMs - König, Jürgen; Wehrheim, Heike (Theoretical Aspects of Computing - ICTAC 2017 - 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings)

Compact Proof Witnesses - Jakobs, Marie-Christine; Wehrheim, Heike (NASA Formal Methods: 9th International Symposium)
Proof witnesses are proof artifacts showing correctness of programs wrt. safety properties. The recent past has seen a rising interest in witnesses as (a) proofs in a proof-carrying-code context, (b) certificates for the correct functioning of verification tools, or simply (c) exchange formats for (partial) verification results. As witnesses in all theses scenarios need to be stored and processed, witnesses are required to be as small as possible. However, software verification tools – the prime suppliers of witnesses – do not necessarily construct small witnesses. In this paper, we present a formal account of proof witnesses. We introduce the concept of weakenings, reducing the complexity of proof witnesses while preserving the ability of witnessing safety. We develop aweakening technique for a specific class of program analyses, and prove it to be sound. Finally, we experimentally demonstrate our weakening technique to indeed achieve a size reduction of proof witnesses.

Certiﬁcation Matters for Service Markets - Jakobs, Marie-Christine; Krämer, Julia; van Straaten, Dirk; Lettmann, Theodor (The Ninth International Conferences on Advanced Service Computing (SERVICE COMPUTATION))
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.

Incremental Inductive Verification of Parameterized Timed Systems - Isenberg, Tobias (ACM Transactions on Embedded Computing Systems)
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.

Policy Dependent and Independent Information Flow Analyses - Töws, Manuel; Wehrheim, Heike (Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods (ICFEM 2017))
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. In 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.