ABSTRACT. Software plays a fundamental role in modern research: it is used in all disciplines as a tool, but it is also a result of research, providing proof of the existence of a solution, and an object of study, as an artefact. And software source code, as a special form of knowledge, designed by humans to be read by humans and executed by machines, is a noble product of the ingenuity of mankind, and embodies a growing part of our technical, scientific and cultural heritage. We believe the time has come to make software source code a first class citizen in the scholarly world: it must be properly archived, referenced, described and cited in order to build a stable and long lasting corpus of scientific knowledge, support reproducibility of research results, and give the due credit to the people that design, develop, maintain, test and evolve it. We show how the Software Heritage universal source code archive provides a means to fully address the first two concerns, by archiving seamlessly all publicly available software source code, and by providing intrinsic persistent identifiers that allow to reference it at various granularities in a way that is at the same time convenient and effective. Support for citing software, leveraging these identifiers, is now also available.  We now call upon the research community to adopt these best practices, and help give software the status it deserves.

ABSTRACT. Enabling Hoare-style reasoning for low-level code is attractive since it opens the way to regain structure and modularity in a domain where structure is essentially absent. The field, however, has not yet arrived at a fully satisfactory solution, in the sense of avoiding restrictions on control flow (important for compiler optimization), controlling access to intermediate program points (important for modularity), and supporting total correctness. Proposals in the literature support some of these properties, but a solution that meets them all is yet to be found. We introduce a novel Hoare-style program logic which interprets postconditions relative to program points when these are first encountered. The logic can support both partial and total correctness, derive contracts for arbitrary control flow, and allows to freely choose decomposition strategy during verification while avoiding step-indexed approximations and global invariants. The logic can be instantiated for a variety of concrete instruction set architectures and intermediate languages. The rules have been verified in the interactive theorem prover HOL4 and integrated with the toolbox HolBA for semi-automated program verification, making it applicable to the ARMv6 and ARMv8 instruction sets.

ABSTRACT. Modern software systems operate in complex and changing environments and are exposed to multiple sources of uncertainty. Considering uncertainty as a first-class concern in software testing is currently on an uptrend. This paper introduces a novel methodology to deal with testing under uncertainty. Our proposal combines the usage of parametric model checking at design-time and online model-based testing algorithms to gather runtime evidence and detect requirement violations. As modeling formalism, we adopt parametric Markov Decision Processes where transition probabilities are not fixed, but are possibly given as a set of uncertain parameters. The design-time phase aims at analyzing the parameter space to identify the constraints for requirements satisfaction. Then, the testing activity applies a Bayesian inference process to identify violations of pre-computed constraints. An extensive empirical evaluation shows that the proposed technique is effective in discovering violations and is cheaper than existing testing under uncertainty methods.

ABSTRACT. Modern software-verification tools need to support development processes that involve frequent changes. Existing approaches for incremental verification hard-code specific verification techniques, and most of them must be integrated in the development process before the software system grows too large to be analyzed as a whole. To solve this open problem, we present the concept of difference verification with conditions. Difference verification with conditions is independent from any specific verification technique and can be integrated in software projects at any time. It first applies a change analysis that detects which parts of a software have changed between revisions and encodes that information in a condition. Based on this condition, an off-the-shelf verifier is used to verify only those parts of the software that are influenced by the changes. As a proof of concept, we propose a simple, syntax-based change analysis and use difference verification with conditions to make three existing verifiers capable of incremental verification. An extensive evaluation shows the competitiveness of difference verification with conditions.

ABSTRACT. Consumption of REST services has become a popular means of invoking code provided by third parties, particularly in web applications. Nowadays programmers of web applications can choose TypeScript over JavaScript to benefit from static type checking that enables validating calls to local functions or to those provided by libraries. Errors in calls to REST services, however, can only be found at run-time. In this paper, we present SafeRESTScript (SRS), a language that extends the support of static analysis to calls to REST services, with the ability to statically find common errors such as missing or invalid data in REST calls and misuse of the results from such calls. SRS features a syntax similar to JavaScript and is equipped with a rich collection of types and primitives to natively support REST calls that are statically validated against specifications of the corresponding APIs written in the HeadREST language.

ABSTRACT. Reconfigurable systems are emerging in many application domains as reconfiguration can be used to cope with unpredictable system environments and adapt by delivering new functionality. The Dynamic Reconfigurable BIP (DR-BIP) framework is an extension of the BIP component framework enriched with dynamic exogenous reconfiguration primitives, intended to support rigorous modeling of reconfigurable systems. We present a new two-layered implementation of DR-BIP clearly separating between execution of reconfiguration operations and execution of a fixed system configuration. Such a separation of concerns offers the advantage of using the mature and efficient BIP engine as well as existing associated analysis and verification tools. Another direct benefit of the new implementation is the possibility to monitor a holistic view of a system’s behavior captured as a set of traces involving information about both the state of the system components and the dynamically changing architecture. Monitoring and analyzing such traces, poses interesting questions regarding the formalization and runtime verification of properties of reconfigurable systems.

ABSTRACT. We formalise mathematical components for solving affine and linear systems of ordinary differential equations in Isabelle/HOL. The formalisation integrates the theory stacks of linear algebra and analysis and substantially adds content to both of them. It also serves to improve extant verification components for hybrid systems by increasing proof automation, removing certification procedures, and decreasing the number of proof obligations. We showcase these advantages through examples.

ABSTRACT. There are many hard verification problems that are currently only solvable by applying several verifiers that are based on complementing technologies. Conditional model checking (CMC) is a successful solution for cooperation between verification tools. In CMC, the first verifier outputs a condition describing the state space that it successfully verified. The second verifier uses the condition to focus its verification on the unverified state space. To use arbitrary second verifiers, a reducer-based approach was recently proposed. The reducer-based approach can be used to construct a conditional verifier from a reducer and a (non-conditional) verifier: the reducer translates the condition into a residual program that describes the unverified state space and the verifier can be any off-theshelf verifier (that does not need to understand conditions). Until now, only one reducer was available. But for a systematic investigation of the reducer concept, we need several reducers. To fill this gap, we developed FRed, a Framework for exploring different REDucers. Given an existing reducer, FRed allows us to derive various new reducers, which differ in their trade-off between size and precision of the residual program. For our experiments, we derived seven different reducers. Our evaluation on the largest and most diverse public collection of verification problems shows that we need all seven reducers to solve hard verification tasks that were not solvable before with the considered verifiers.

ABSTRACT. The recent active development of Internet of Things (IoT) solutions in various domains has led to an increased demand for security, safety, and reliability of these systems. Security and data privacy are currently the most frequently discussed topics; however, other reliability aspects also need to be focused on to maintain smooth and safe operation of IoT systems. Until now, there has been no systematic mapping study dedicated to the topic of interoperability and integration testing of IoT systems specifically; therefore, we present such an overview in this study. We analyze 803 papers from four major primary databases and perform detailed assessment and quality check to find 115 relevant papers. In addition, recently published testing techniques and approaches are analyzed and classified; the challenges and limitations in the field are also identified and discussed. Research trends related to publication time, active researchers, and publication media are presented in this study. The results suggest that studies mainly focus only on general testing methods, which can be applied to integration and interoperability testing of IoT systems; thus, there are research opportunities to develop additional testing methods focused specifically on IoT systems, so that they are more effective in the IoT context.