Container-based virtualization is a popular technique, e.g., to realize microservice architectures. Recently, containers became popular in Industry 4.0 / IIoT systems, which typically consist of hundreds of (edge) devices and machines. In such ...

Over the last several decades, static and dynamic program analysis techniques have received widespread attention. Their application to mainstream programming languages always requires extending theories and finding practical solutions. This ...

The C programming language offers setjmp/ longjmp as a mechanism for nonlocal control flow. This mechanism has complicated semantics. As most developers do not encounter it day-to-day, they may be unfamiliar with all its intricacies – leading to ...

Running static analysis rules in the wild as part of a commercial service demands special consideration of time limits and scalability, given the large and diverse real-world workloads that the rules are evaluated on. Furthermore, these rules do ...

CodePeer is a static analysis tool based on compiler optimization techniques such as static single assignment and value numbering. CodePeer infers and reports on implicit preconditions for each function of the program, based on limitations it ...

In the context of abstract interpretation-based static analysis, we propose a new abstract operator modeling the split of control flow paths: the goal of the operator is to enable a more efficient analysis when using abstract domains that are ...

Software verification aims to prove that a program satisfies some given properties for all its possible executions. Software evolved incredibly fast during the last century, exposing several challenges to this scientific discipline. The goal of ...

The widespread use of advanced driver assistance systems in modern vehicles, together with their integration with the Internet and other road nodes, has made vehicle more vulnerable to cyber-attacks. To address these risks, the automotive industry ...

Formally verified compilers and formally verified static analyzers are a solution to the problem that certain industries face when they have to demonstrate to authorities that the object code they run truly corresponds to its source code and that ...

Blockchain technology has created a new software development context, with its own peculiarities, mainly due to the guarantees that the technology must satisfy, that is, immutability, distributability, and decentralization of data. Its rapid ...

We present a relational program logic for reasoning about information flow properties formalised in an assertion language based on partial equivalence relations. We define and prove the soundness of the logic, a proof technique for precise, logic-...

We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018–2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then we introduce new benchmark classes that have been added to the ...

An execution trace is a model of a single system behavior. Execution traces occur everywhere in the system’s lifecycle as they can typically be produced by executable models, by prototypes of (sub)systems, and by the system itself during its ...

Architecture-Driven Modernization (ADM) is a special kind of reengineering that employs models along the process. The main ADM metamodel is the Knowledge Discovery Metamodel (KDM), which is a platform-independent metamodel able to represent ...

An adaptive system is able to adapt at runtime to dynamically changing environments and to new requirements. Adaptive systems can be single adaptive entities or collective ones that consist of several collaborating entities. Rigorous engineering ...

There have been a number of approaches to employ neural networks in self-adaptive systems; in many cases, generic neural networks and deep learning are utilized for this purpose. When this approach is to be applied to improve an adaptation process ...

This paper advocates the use of compositional specifications based on formal languages as a means of modelling and analysing sophisticated collective behaviour in natural systems. With the use of appropriate linguistic constructs, models can be ...

We present an application of strategy synthesis to enforce spatial properties. This is achieved by implementing a toolchain that enables the tools CATLib and VoxLogicA to interact in a fully automated way. The Contract Automata Library (CATLib) is ...

Reconfigurable interacting systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interaction interfaces by forming collectives and ...

Non-functional properties of collective adaptive systems (CAS) are of paramount relevance practically in any application. This paper compares two recently proposed approaches to quantitative modelling that exploit different system abstractions: ...