@inbook{45888, author = {{Wehrheim, Heike and Platzner, Marco and Bodden, Eric and Schubert, Philipp and Pauck, Felix and Jakobs, Marie-Christine}}, booktitle = {{On-The-Fly Computing -- Individualized IT-services in dynamic markets}}, editor = {{Haake, Claus-Jochen and Meyer auf der Heide, Friedhelm and Platzner, Marco and Wachsmuth, Henning and Wehrheim, Heike}}, pages = {{125--144}}, publisher = {{Heinz Nixdorf Institut, Universität Paderborn}}, title = {{{Verifying Software and Reconfigurable Hardware Services}}}, doi = {{10.5281/zenodo.8068583}}, volume = {{412}}, year = {{2023}}, } @book{45863, abstract = {{In the proposal for our CRC in 2011, we formulated a vision of markets for IT services that describes an approach to the provision of such services that was novel at that time and, to a large extent, remains so today: „Our vision of on-the-fly computing is that of IT services individually and automatically configured and brought to execution from flexibly combinable services traded on markets. At the same time, we aim at organizing markets whose participants maintain a lively market of services through appropriate entrepreneurial actions.“ Over the last 12 years, we have developed methods and techniques to address problems critical to the convenient, efficient, and secure use of on-the-fly computing. Among other things, we have made the description of services more convenient by allowing natural language input, increased the quality of configured services through (natural language) interaction and more efficient configuration processes and analysis procedures, made the quality of (the products of) providers in the marketplace transparent through reputation systems, and increased the resource efficiency of execution through reconfigurable heterogeneous computing nodes and an integrated treatment of service description and configuration. We have also developed network infrastructures that have a high degree of adaptivity, scalability, efficiency, and reliability, and provide cryptographic guarantees of anonymity and security for market participants and their products and services. To demonstrate the pervasiveness of the OTF computing approach, we have implemented a proof-of-concept for OTF computing that can run typical scenarios of an OTF market. We illustrated the approach using a cutting-edge application scenario – automated machine learning (AutoML). Finally, we have been pushing our work for the perpetuation of On-The-Fly Computing beyond the SFB and sharing the expertise gained in the SFB in events with industry partners as well as transfer projects. This work required a broad spectrum of expertise. Computer scientists and economists with research interests such as computer networks and distributed algorithms, security and cryptography, software engineering and verification, configuration and machine learning, computer engineering and HPC, microeconomics and game theory, business informatics and management have successfully collaborated here.}}, author = {{Haake, Claus-Jochen and Meyer auf der Heide, Friedhelm and Platzner, Marco and Wachsmuth, Henning and Wehrheim, Heike}}, pages = {{247}}, publisher = {{Heinz Nixdorf Institut, Universität Paderborn}}, title = {{{On-The-Fly Computing -- Individualized IT-services in dynamic markets}}}, doi = {{10.17619/UNIPB/1-1797}}, volume = {{412}}, year = {{2023}}, } @inproceedings{35426, author = {{Richter, Cedric and Haltermann, Jan Frederik and Jakobs, Marie-Christine and Pauck, Felix and Schott, Stefan and Wehrheim, Heike}}, booktitle = {{37th IEEE/ACM International Conference on Automated Software Engineering}}, publisher = {{ACM}}, title = {{{Are Neural Bug Detectors Comparable to Software Developers on Variable Misuse Bugs?}}}, doi = {{10.1145/3551349.3561156}}, year = {{2023}}, } @inbook{45886, author = {{Wehrheim, Heike and Hüllermeier, Eyke and Becker, Steffen and Becker, Matthias and Richter, Cedric and Sharma, Arnab}}, booktitle = {{On-The-Fly Computing -- Individualized IT-services in dynamic markets}}, editor = {{Haake, Claus-Jochen and Meyer auf der Heide, Friedhelm and Platzner, Marco and Wachsmuth, Henning and Wehrheim, Heike}}, pages = {{105--123}}, publisher = {{Heinz Nixdorf Institut, Universität Paderborn}}, title = {{{Composition Analysis in Unknown Contexts}}}, doi = {{10.5281/zenodo.8068510}}, volume = {{412}}, year = {{2023}}, } @inproceedings{32311, abstract = {{Testing is one of the most frequent means of quality assurance for software. Property-based testing aims at generating test suites for checking code against user-defined properties. Test input generation is, however, most often independent of the property to be checked, and is instead based on random or user-defined data generation.In this paper, we present property-driven unit testing of functions with numerical inputs and outputs. Alike property-based testing, it allows users to define the properties to be tested for. Contrary to property-based testing, it also uses the property for a targeted generation of test inputs. Our approach is a form of learning-based testing where we first of all learn a model of a given black-box function using standard machine learning algorithms, and in a second step use model and property for test input generation. This allows us to test both predefined functions as well as machine learned regression models. Our experimental evaluation shows that our property-driven approach is more effective than standard property-based testing techniques.}}, author = {{Sharma, Arnab and Melnikov, Vitaly and Hüllermeier, Eyke and Wehrheim, Heike}}, booktitle = {{Proceedings of the 10th IEEE/ACM International Conference on Formal Methods in Software Engineering (FormaliSE)}}, pages = {{113--123}}, publisher = {{IEEE}}, title = {{{Property-Driven Testing of Black-Box Functions}}}, year = {{2022}}, } @inproceedings{32590, author = {{Richter, Cedric and Wehrheim, Heike}}, booktitle = {{2022 IEEE Conference on Software Testing, Verification and Validation (ICST)}}, pages = {{162--173}}, title = {{{Learning Realistic Mutations: Bug Creation for Neural Bug Detectors}}}, doi = {{10.1109/ICST53961.2022.00027}}, year = {{2022}}, } @inproceedings{32591, author = {{Richter, Cedric and Wehrheim, Heike}}, booktitle = {{2022 IEEE/ACM 19th International Conference on Mining Software Repositories (MSR)}}, pages = {{418--422}}, title = {{{TSSB-3M: Mining single statement bugs at massive scale}}}, doi = {{10.1145/3524842.3528505}}, year = {{2022}}, } @inproceedings{45248, author = {{Dongol, Brijesh and Schellhorn, Gerhard and Wehrheim, Heike}}, booktitle = {{33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland}}, editor = {{Klin, Bartek and Lasota, Slawomir and Muscholl, Anca}}, pages = {{31:1–31:23}}, publisher = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}}, title = {{{Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement}}}, doi = {{10.4230/LIPIcs.CONCUR.2022.31}}, volume = {{243}}, year = {{2022}}, } @article{25213, author = {{Sharma, Arnab and Demir, Caglar and Ngonga Ngomo, Axel-Cyrille and Wehrheim, Heike}}, journal = {{CoRR}}, title = {{{MLCheck- Property-Driven Testing of Machine Learning Models}}}, volume = {{abs/2105.00741}}, year = {{2021}}, } @inproceedings{28350, abstract = {{In recent years, we observe an increasing amount of software with machine learning components being deployed. This poses the question of quality assurance for such components: how can we validate whether specified requirements are fulfilled by a machine learned software? Current testing and verification approaches either focus on a single requirement (e.g., fairness) or specialize on a single type of machine learning model (e.g., neural networks). In this paper, we propose property-driven testing of machine learning models. Our approach MLCheck encompasses (1) a language for property specification, and (2) a technique for systematic test case generation. The specification language is comparable to property-based testing languages. Test case generation employs advanced verification technology for a systematic, property dependent construction of test suites, without additional user supplied generator functions. We evaluate MLCheck using requirements and data sets from three different application areas (software discrimination, learning on knowledge graphs and security). Our evaluation shows that despite its generality MLCheck can even outperform specialised testing approaches while having a comparable runtime}}, author = {{Sharma, Arnab and Demir, Caglar and Ngonga Ngomo, Axel-Cyrille and Wehrheim, Heike}}, booktitle = {{Proceedings of the 20th IEEE International Conference on Machine Learning and Applications (ICMLA)}}, publisher = {{IEEE}}, title = {{{MLCHECK–Property-Driven Testing of Machine Learning Classifiers}}}, year = {{2021}}, } @inproceedings{22927, author = {{Derrick, John and Doherty, Simon and Dongol, Brijesh and Schellhorn, Gerhard and Wehrheim, Heike}}, booktitle = {{Proceedings of the 35th International Symposium on Distributed Computing (DISC)}}, publisher = {{Schloß Dagstuhl}}, title = {{{On Strong Observational Refinement and Forward Simulation}}}, year = {{2021}}, } @inproceedings{28199, author = {{Pauck, Felix and Wehrheim, Heike}}, booktitle = {{2021 IEEE 21st International Working Conference on Source Code Analysis and Manipulation (SCAM)}}, title = {{{Jicer: Simplifying Cooperative Android App Analysis Tasks}}}, doi = {{10.1109/scam52516.2021.00031}}, year = {{2021}}, } @article{27841, abstract = {{Verification of software and processor hardware usually proceeds separately, software analysis relying on the correctness of processors executing machine instructions. This assumption is valid as long as the software runs on standard CPUs that have been extensively validated and are in wide use. However, for processors exploiting custom instruction set extensions to meet performance and energy constraints the validation might be less extensive, challenging the correctness assumption. In this paper we present a novel formal approach for hardware/software co-verification targeting processors with custom instruction set extensions. We detail two different approaches for checking whether the hardware fulfills the requirements expected by the software analysis. The approaches are designed to explore a trade-off between generality of the verification and computational effort. Then, we describe the integration of software and hardware analyses for both techniques and describe a fully automated tool chain implementing the approaches. Finally, we demonstrate and compare the two approaches on example source code with custom instructions, using state-of-the-art software analysis and hardware verification techniques.}}, author = {{Jakobs, Marie-Christine and Pauck, Felix and Platzner, Marco and Wehrheim, Heike and Wiersema, Tobias}}, journal = {{IEEE Access}}, keywords = {{Software Analysis, Abstract Interpretation, Custom Instruction, Hardware Verification}}, publisher = {{IEEE}}, title = {{{Software/Hardware Co-Verification for Custom Instruction Set Processors}}}, doi = {{10.1109/ACCESS.2021.3131213}}, year = {{2021}}, } @inproceedings{21238, author = {{Pauck, Felix and Wehrheim, Heike}}, booktitle = {{Software Engineering 2021}}, editor = {{Koziolek, Anne and Schaefer, Ina and Seidl, Christoph}}, pages = {{ 83--84 }}, publisher = {{Gesellschaft für Informatik e.V.}}, title = {{{Cooperative Android App Analysis with CoDiDroid}}}, doi = {{10.18420/SE2021_30 }}, year = {{2021}}, } @inproceedings{19656, author = {{Sharma, Arnab and Wehrheim, Heike}}, booktitle = {{Proceedings of the 32th IFIP International Conference on Testing Software and Systems (ICTSS)}}, publisher = {{Springer}}, title = {{{Automatic Fairness Testing of Machine Learning Models}}}, year = {{2020}}, } @inproceedings{20274, author = {{Bila, Eleni and Doherty, Simon and Dongol, Brijesh and Derrick, John and Schellhorn, Gerhard and Wehrheim, Heike}}, booktitle = {{Formal Techniques for Distributed Objects, Components, and Systems - 40th {IFIP} {WG} 6.1 International Conference, {FORTE} 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings}}, editor = {{Gotsman, Alexey and Sokolova, Ana}}, pages = {{39--58}}, publisher = {{Springer}}, title = {{{Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory}}}, doi = {{10.1007/978-3-030-50086-3\_3}}, volume = {{12136}}, year = {{2020}}, } @inproceedings{20275, author = {{Beringer, Steffen and Wehrheim, Heike}}, booktitle = {{Proceedings of the 15th International Conference on Software Technologies, {ICSOFT} 2020, Lieusaint, Paris, France, July 7-9, 2020}}, editor = {{van Sinderen, Marten and Fill, Hans{-}Georg and A. Maciaszek, Leszek}}, pages = {{15--26}}, publisher = {{ScitePress}}, title = {{{Consistency Analysis of AUTOSAR Timing Requirements}}}, doi = {{10.5220/0009766600150026}}, year = {{2020}}, } @inproceedings{20276, author = {{Beyer, Dirk and Wehrheim, Heike}}, booktitle = {{Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part {I}}}, editor = {{Margaria, Tiziana and Steffen, Bernhard}}, pages = {{143--167}}, publisher = {{Springer}}, title = {{{Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework}}}, doi = {{10.1007/978-3-030-61362-4\_8}}, volume = {{12476}}, year = {{2020}}, } @proceedings{20277, editor = {{Wehrheim, Heike and Cabot, Jordi}}, isbn = {{978-3-030-45233-9}}, publisher = {{Springer}}, title = {{{Fundamental Approaches to Software Engineering - 23rd International Conference, FASE 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings}}}, doi = {{10.1007/978-3-030-45234-6}}, volume = {{12076}}, year = {{2020}}, } @proceedings{20278, 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}}, }