@inproceedings{14885, author = {{Potthast, Martin and Chen, Wei-Fan and Hagen, Matthias and Stein, Benno}}, booktitle = {{Proceedings of the Second International Workshop on Recent Trends in News Information Retrieval}}, pages = {{3--5}}, title = {{{A Plan for Ancillary Copyright: Original Snippets.}}}, year = {{2018}}, } @inproceedings{3325, author = {{Melnikov, Vitalik and Hüllermeier, Eyke}}, booktitle = {{Proceedings. 27. Workshop Computational Intelligence, Dortmund, 23. - 24. November 2017}}, publisher = {{KIT Scientific Publishing}}, title = {{{Optimizing the Structure of Nested Dichotomies: A Comparison of Two Heuristics}}}, doi = {{10.5445/KSP/1000074341}}, year = {{2017}}, } @misc{3512, author = {{Börding, Paul}}, publisher = {{Universität Paderborn}}, title = {{{Testing Java Method Contracts}}}, year = {{2017}}, } @misc{3580, author = {{Hansmeier, Tim}}, publisher = {{Universität Paderborn}}, title = {{{An FPGA Accelerator for Checking Resolution Proofs}}}, year = {{2017}}, } @inproceedings{114, abstract = {{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.}}, author = {{Jakobs, Marie-Christine and Wehrheim, Heike}}, booktitle = {{NASA Formal Methods: 9th International Symposium}}, editor = {{Barrett, Clark and Davies, Misty and Kahsai, Temesghen}}, pages = {{389--403}}, title = {{{Compact Proof Witnesses}}}, doi = {{10.1007/978-3-319-57288-8_28}}, year = {{2017}}, } @inproceedings{115, abstract = {{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.}}, author = {{Jakobs, Marie-Christine and Krämer, Julia and van Straaten, Dirk and Lettmann, Theodor}}, booktitle = {{The Ninth International Conferences on Advanced Service Computing (SERVICE COMPUTATION)}}, editor = {{Marcelo De Barros, Janusz Klink,Tadeus Uhl, Thomas Prinz}}, pages = {{7--12}}, title = {{{Certification Matters for Service Markets}}}, year = {{2017}}, } @misc{1157, author = {{Witschen, Linus Matthias}}, publisher = {{Universität Paderborn}}, title = {{{A Framework for the Synthesis of Approximate Circuits}}}, year = {{2017}}, } @article{90, abstract = {{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.}}, author = {{Isenberg, Tobias}}, journal = {{ACM Transactions on Embedded Computing Systems}}, number = {{2}}, pages = {{47:1--47:24}}, publisher = {{ACM}}, title = {{{Incremental Inductive Verification of Parameterized Timed Systems}}}, doi = {{10.1145/2984640}}, year = {{2017}}, } @inbook{93, abstract = {{In recent years, there has been a proliferation of technological developments that incorporate processing of human language. Hardware and software can be specialized for designated subject areas, and computational devices are designed for a widening variety of applications. At the same time, new areas and applications are emerging by demanding intelligent technology enhanced by the processing of human language. These new applications often perform tasks which handle information, and they have a capacity to reason, using both formal and human language. Many sub-areas of Artificial Intelligence demand integration of Natural Language Processing, at least to some degree. Furthermore, technologies require coverage of known as well as unknown agents, and tasks with potential variations. All of this takes place in environments with unknown factors. The book covers theoretical work, advanced applications, approaches, and techniques for computational models of information, reasoning systems, and presentation in language. The book promotes work on intelligent natural language processing and related models of information, thought, reasoning, and other cognitive processes. The topics covered by the chapters prompt further research and developments of advanced systems in the areas of logic, computability, computational linguistics, cognitive science, neuroscience of language, robotics, and artificial intelligence, among others.}}, author = {{Geierhos, Michaela and Bäumer, Frederik Simon}}, booktitle = {{Partiality and Underspecification in Information, Languages, and Knowledge}}, editor = {{Christiansen, Henning and Jiménez-López, M. Dolores and Loukanova, Roussanka and Moss, Lawrence S.}}, isbn = {{978-1- 4438-7947-7}}, pages = {{65--108}}, publisher = {{Cambridge Scholars Publishing}}, title = {{{Guesswork? Resolving Vagueness in User-Generated Software Requirements}}}, year = {{2017}}, } @misc{5694, author = {{Schnitker, Nino Noel}}, publisher = {{Universität Paderborn}}, title = {{{Genetischer Algorithmus zur Erstellung von Ensembles von Nested Dichotomies}}}, year = {{2017}}, } @inproceedings{57, abstract = {{Users prefer natural language software requirements because of their usability and accessibility. Many approaches exist to elaborate these requirements and to support the users during the elicitation process. But there is a lack of adequate resources, which are needed to train and evaluate approaches for requirement refinement. We are trying to close this gap by using online available software descriptions from SourceForge and app stores. Thus, we present two real-life requirements collections based on online-available software descriptions. Our goal is to show the domain-specific characteristics of content words describing functional requirements. On the one hand, we created a semantic role-labeled requirements set, which we use for requirements classification. On the other hand, we enriched software descriptions with linguistic features and dependencies to provide evidence for the context-awareness of software functionalities. }}, author = {{Bäumer, Frederik Simon and Dollmann, Markus and Geierhos, Michaela}}, booktitle = {{Proceedings of the 2nd ACM SIGSOFT International Workshop on App Market Analytics}}, editor = {{Sarro, Federica and Shihab, Emad and Nagappan, Meiyappan and Platenius, Marie Christin and Kaimann, Daniel}}, isbn = {{978-1-4503-5158-4}}, location = {{Paderborn, Germany}}, pages = {{19--25}}, publisher = {{ACM}}, title = {{{Studying Software Descriptions in SourceForge and App Stores for a better Understanding of real-life Requirements}}}, doi = {{10.1145/3121264.3121269}}, year = {{2017}}, } @misc{5724, author = {{Hetzer, Alexander and Tornede, Tanja}}, publisher = {{Universität Paderborn}}, title = {{{Solving the Container Pre-Marshalling Problem using Reinforcement Learning and Structured Output Prediction}}}, year = {{2017}}, } @inproceedings{5769, abstract = {{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.}}, author = {{Töws, Manuel and Wehrheim, Heike}}, booktitle = {{Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods (ICFEM 2017)}}, isbn = {{9783319686899}}, issn = {{0302-9743}}, pages = {{362--378}}, publisher = {{Springer International Publishing}}, title = {{{Policy Dependent and Independent Information Flow Analyses}}}, doi = {{10.1007/978-3-319-68690-5_22}}, year = {{2017}}, } @misc{46, author = {{Grobbel, Florian}}, publisher = {{Universität Paderborn}}, title = {{{Was kommt zuerst? Erkennung von zeitlichen Abläufen infunktionalen Softwareanforderungsbeschreibungen}}}, year = {{2017}}, } @misc{47, author = {{Theda, Mona}}, publisher = {{Universität Paderborn}}, title = {{{Was ist gemeint? Strukturell ambige Sätze als Herausforderung für Parsing-Ansätze}}}, year = {{2017}}, } @phdthesis{707, author = {{Walther, Sven}}, publisher = {{Universität Paderborn}}, title = {{{Knowledge-based Verification of Service Compositions}}}, doi = {{10.17619/UNIPB/1-307}}, year = {{2017}}, } @inproceedings{71, abstract = {{Today, software verification tools have reached the maturity to be used for large scale programs. Different tools perform differently well on varying code. A software developer is hence faced with the problem of choosing a tool appropriate for her program at hand. A ranking of tools on programs could facilitate the choice. Such rankings can, however, so far only be obtained by running all considered tools on the program.In this paper, we present a machine learning approach to predicting rankings of tools on programs. The method builds upon so-called label ranking algorithms, which we complement with appropriate kernels providing a similarity measure for programs. Our kernels employ a graph representation for software source code that mixes elements of control flow and program dependence graphs with abstract syntax trees. Using data sets from the software verification competition SV-COMP, we demonstrate our rank prediction technique to generalize well and achieve a rather high predictive accuracy (rank correlation > 0.6).}}, author = {{Czech, Mike and Hüllermeier, Eyke and Jakobs, Marie-Christine and Wehrheim, Heike}}, booktitle = {{Proceedings of the 3rd International Workshop on Software Analytics}}, pages = {{23--26}}, title = {{{Predicting Rankings of Software Verification Tools}}}, doi = {{10.1145/3121257.3121262}}, year = {{2017}}, } @techreport{72, abstract = {{Software verification competitions, such as the annual SV-COMP, evaluate software verification tools with respect to their effectivity and efficiency. Typically, the outcome of a competition is a (possibly category-specific) ranking of the tools. For many applications, such as building portfolio solvers, it would be desirable to have an idea of the (relative) performance of verification tools on a given verification task beforehand, i.e., prior to actually running all tools on the task.In this paper, we present a machine learning approach to predicting rankings of tools on verification tasks. The method builds upon so-called label ranking algorithms, which we complement with appropriate kernels providing a similarity measure for verification tasks. Our kernels employ a graph representation for software source code that mixes elements of control flow and program dependence graphs with abstract syntax trees. Using data sets from SV-COMP, we demonstrate our rank prediction technique to generalize well and achieve a rather high predictive accuracy. In particular, our method outperforms a recently proposed feature-based approach of Demyanova et al. (when applied to rank predictions). }}, author = {{Czech, Mike and Hüllermeier, Eyke and Jakobs, Marie-Christine and Wehrheim, Heike}}, title = {{{Predicting Rankings of Software Verification Competitions}}}, year = {{2017}}, } @inproceedings{73, abstract = {{Today, verification tools do not only output yes or no, but also provide correctness arguments or counterexamples. While counterexamples help to fix bugs, correctness arguments are used to increase the trust in program correctness, e.g., in Proof-Carrying Code (PCC). Correctness arguments are well-studied for single analyses, but not when a set of analyses together verifies a program, each of the analyses checking only a particular part. Such a set of partial, complementary analyses is often used when a single analysis would fail or is inefficient on some program parts.We propose PART_PW, a technique which allows us to automatically construct a proof witness (correctness argument) from the analysis results obtained by a set of partial, complementary analyses. The constructed proof witnesses are proven to be valid correctness arguments and in our experiments we use them seamlessly and efficiently in existing PCC approaches.}}, author = {{Jakobs, Marie-Christine}}, booktitle = {{Software Engineering and Formal Methods}}, editor = {{Cimatti, Alessandro and Sirjani, Marjan}}, pages = {{120--135}}, title = {{{PART_PW: From Partial Analysis Results to a Proof Witness}}}, doi = {{10.1007/978-3-319-66197-1_8}}, year = {{2017}}, } @inproceedings{84, abstract = {{The increasing popularity of paradigms like service-oriented computing and cloud com-puting is leading to a growing amount of service providers offering software componentsin the form of deployed, ready-to-use services (Software as a Service, SaaS) [14, 20].In order to discover and select software services, intermediaries apply service matchingapproaches for determining whether the specification of a provided service satisfies therequester’s requirements. There are already lots of different service matching approachesconsidering different service properties (structural, behavioral, and non-functional proper-ties). However, each of these approaches alone is not enough to provide a high matchingresult quality (e.g., accurate matching results) [BOR04].Thus, such approaches should be combined into a more holistic approach leading to moreaccurate matching results. However, this combination is a manual, error-prone procedurewhere many design decisions are made. Furthermore, this procedure has to be repeatedfrequently depending on the context, e.g., to consider different requesters or markets.}}, author = {{Platenius, Marie Christin and Arifulina, Svetlana and Schäfer, Wilhelm}}, booktitle = {{Tagungsband Software Engineering}}, pages = {{81----82}}, title = {{{MatchBox: A Framework for Dynamic Configuration of Service Matching Processes (Extended Abstract)}}}, year = {{2017}}, }