@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}}, } @article{10096, author = {{Beyer, Dirk and Wehrheim, Heike}}, journal = {{CoRR}}, title = {{{Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework}}}, volume = {{abs/1905.08505}}, 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}}, } @inproceedings{3414, abstract = {{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.}}, author = {{Börding, Paul and Haltermann, Jan Frederik and Jakobs, Marie-Christine and Wehrheim, Heike}}, booktitle = {{Proceedings of the IFIP International Conference on Testing Software and Systems (ICTSS 2018)}}, location = {{Cádiz, Spain}}, pages = {{39----55}}, publisher = {{Springer}}, title = {{{JMCTest: Automatically Testing Inter-Method Contracts in Java}}}, volume = {{11146}}, year = {{2018}}, } @inbook{3536, author = {{Schellhorn, Gerhard and Wedel, Monika and Travkin, Oleg and König, Jürgen and Wehrheim, Heike}}, booktitle = {{Software Engineering and Formal Methods}}, isbn = {{9783319929699}}, issn = {{0302-9743}}, pages = {{105--120}}, publisher = {{Springer International Publishing}}, title = {{{FastLane Is Opaque – a Case Study in Mechanized Proofs of Opacity}}}, doi = {{10.1007/978-3-319-92970-5_7}}, year = {{2018}}, } @article{3153, author = {{Doherty, Simon and Derrick, John and Dongol, Brijesh and Wehrheim, Heike}}, journal = {{CoRR}}, title = {{{Causal Linearizability: Compositionality for Partially Ordered Executions}}}, year = {{2018}}, } @unpublished{2711, abstract = {{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.}}, author = {{Pauck, Felix and Bodden, Eric and Wehrheim, Heike}}, booktitle = {{arXiv:1804.02903}}, title = {{{Do Android Taint Analysis Tools Keep their Promises?}}}, year = {{2018}}, } @inproceedings{5774, abstract = {{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.}}, author = {{Töws, Manuel and Wehrheim, Heike}}, booktitle = {{Theoretical Aspects of Computing – ICTAC 2018}}, isbn = {{9783030025076}}, issn = {{0302-9743}}, pages = {{435--454}}, publisher = {{Springer International Publishing}}, title = {{{Information Flow Certificates}}}, doi = {{10.1007/978-3-030-02508-3_23}}, year = {{2018}}, } @inproceedings{4999, author = {{Pauck, Felix and Bodden, Eric and Wehrheim, Heike}}, booktitle = {{Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering - ESEC/FSE 2018}}, isbn = {{9781450355735}}, publisher = {{ACM Press}}, title = {{{Do Android taint analysis tools keep their promises?}}}, doi = {{10.1145/3236024.3236029}}, year = {{2018}}, } @article{6828, author = {{Derrick, John and Doherty, Simon and Dongol, Brijesh and Schellhorn, Gerhard and Travkin, Oleg and Wehrheim, Heike}}, journal = {{Formal Asp. Comput.}}, number = {{5}}, pages = {{597--625}}, title = {{{Mechanized proofs of opacity: a comparison of two techniques}}}, doi = {{10.1007/s00165-017-0433-3}}, volume = {{30}}, year = {{2018}}, } @inproceedings{6836, author = {{Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike and Derrick, John}}, booktitle = {{Integrated Formal Methods - 14th International Conference, {IFM} 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings}}, pages = {{110--129}}, title = {{{Making Linearizability Compositional for Partially Ordered Executions}}}, doi = {{10.1007/978-3-319-98938-9\_7}}, year = {{2018}}, } @inproceedings{6838, author = {{Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike and Derrick, John}}, booktitle = {{Integrated Formal Methods - 14th International Conference, {IFM} 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings}}, pages = {{110--129}}, title = {{{Making Linearizability Compositional for Partially Ordered Executions}}}, doi = {{10.1007/978-3-319-98938-9\_7}}, year = {{2018}}, } @inproceedings{6839, author = {{Doherty, Simon and Dongol, Brijesh and Wehrheim, Heike and Derrick, John}}, booktitle = {{32nd International Symposium on Distributed Computing, {DISC} 2018, New Orleans, LA, USA, October 15-19, 2018}}, pages = {{45:1--45:3}}, title = {{{Brief Announcement: Generalising Concurrent Correctness to Weak Memory}}}, doi = {{10.4230/LIPIcs.DISC.2018.45}}, year = {{2018}}, } @article{1043, abstract = {{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.}}, author = {{Isenberg, Tobias and Jakobs, Marie-Christine and Pauck, Felix and Wehrheim, Heike}}, issn = {{1943-0663}}, journal = {{IEEE Embedded Systems Letters}}, pages = {{22--25}}, publisher = {{Institute of Electrical and Electronics Engineers (IEEE)}}, title = {{{Validity of Software Verification Results on Approximate Hardware}}}, doi = {{10.1109/LES.2017.2758200}}, year = {{2018}}, } @inproceedings{1096, abstract = {{to appear}}, author = {{Beyer, Dirk and Jakobs, Marie-Christine and Lemberger, Thomas and Wehrheim, Heike}}, booktitle = {{Proceedings of the 40th International Conference on Software Engineering (ICSE)}}, location = {{Gothenburg, Sweden}}, pages = {{1182----1193}}, publisher = {{ACM}}, title = {{{Reducer-Based Construction of Conditional Verifiers}}}, year = {{2018}}, } @inproceedings{3155, author = {{Töws, Manuel and Wehrheim, Heike}}, booktitle = {{Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, {ICFEM} 2017, Xi'an, China, November 13-17, 2017, Proceedings}}, editor = {{Duan, Zhenhua and Ong, Luke}}, pages = {{362----378}}, title = {{{Policy Dependent and Independent Information Flow Analyses}}}, doi = {{10.1007/978-3-319-68690-5_22}}, year = {{2017}}, } @inproceedings{3156, author = {{König, Jürgen and Wehrheim, Heike}}, booktitle = {{Theoretical Aspects of Computing - {ICTAC} 2017 - 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings}}, editor = {{Van Hung, Dang and Kapur, Deepak}}, pages = {{118----135}}, title = {{{Value-Based or Conflict-Based? Opacity Definitions for STMs}}}, doi = {{10.1007/978-3-319-67729-3_8}}, year = {{2017}}, }