Abstract
This article presents Pardinus, an extension of the popular Kodkod relational model finder with linear temporal logic (including past operators), to simplify the analysis of dynamic systems. Pardinus includes a SAT-based bounded-model checking engine and an SMV-based complete model checking engine, both allowing iteration through the different instances (or counter-examples) of a specification. It also supports a decomposed parallel analysis strategy that improves the efficiency of both analysis engines on commodity multi-core machines.

Abstract
Robotic applications are often designed to be reusable and configurable. Sometimes, due to the different supported software and hardware components, as well as the different implemented robot capabilities, the total number of possible configurations for a single system can be extremely large. In these scenarios, understanding how different configurations coexist and which components and capabilities are compatible with each other is a significant time sink both for developers and end users alike. In this paper, we present a static analysis tool, specifically designed for robotic software developed for the Robot Operating System (ROS), that is capable of presenting a graphical and interactive overview of the system's runtime variability, with the goal of simplifying the deployment of the desired robot configuration.

Abstract
This paper describes a methodology for task model design and analysis using the Alloy Analyzer, a formal, declarative modeling tool. Our methodology leverages (1) a formalization of the HAMSTERS task modeling notation in Alloy and (2) a method for encoding a concrete task model and compose it with a model of the interactive system. The Analyzer then automatically verifies the overall model against desired properties, revealing counter-examples (if any) in terms of interaction scenarios between the operator and the system. In addition, we demonstrate how Alloy can be used to encode various types of operator errors (e.g., inserting or omitting an action) into the base HAMSTERS model and generate erroneous interaction scenarios. Our methodology is applied to a task model describing the interaction of a traffic air controller with a semi-autonomous Arrival MANager (AMAN) planning tool. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Abstract
This short paper summarizes an article published in the Journal of Automated Reasoning [7]. It presents, an extension of the popular [12] relational model finder with linear temporal logic (including past operators) to simplify the analysis of dynamic systems. includes a SAT-based bounded model checking engine and an SMV-based complete model checking engine, both allowing iteration through the different instances (or counterexamples) of a specification. It also supports a decomposed parallel analysis strategy that improves the efficiency of both analysis engines on commodity multi-core machines. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Abstract

Abstract
Existing bidirectional languages are either state-based or operation-based, depending on whether they represent updates as mere states or as sequences of edit operations. In-between both worlds are delta-based frameworks, where updates are represented using alignment relationships between states. In this paper, we formalize delta lenses over inductive types using dependent type theory and develop a point-free delta lens language with an explicit separation of shape and data. In contrast with the already known issue of data alignment, we identify the new problem of shape alignment and solve it by lifting standard recursion patterns such as folds and unfolds to delta lenses that use alignment to infer meaningful shape updates. © Bidirectional Transformations 2012.