Formal Methods: Foundations and Applications

Machine learning is a popular tool for building state of the art software systems. It is more and more used also in safety critical areas. This demands for verification techniques ensuring the safety and security of machine learning based solutions. However, we argue that the popularity of machine learning comes from the fact that no formal specification exists which renders traditional verification inappropriate. Instead, validation is typically demanded, but formalization of so far informal requirements is necessary to give formal evidence that the right system is build. Moreover, we present a recent technique that allows to check certain properties for an underlying recurrent neural network and which may be uses as a tool to identify whether the system learned is right.

Modular combination of theory solvers is an integral theme in engineering modern SMT solvers. The CDCL(T) architecture provides an overall setting for how theory solvers may cooperate around a SAT solver based on conflict driven clause learning. The Nelson-Oppen framework provides the interface contracts between theory solvers for disjoint signatures. This paper provides an update on theories integrated in Z3. We briefly review principles of theory integration in CDCL(T) and then examine the theory solvers available in Z3, with special emphasis on two recent solvers: a new solver for arithmetic and a pluggable user solver that allows callbacks to invoke propagations and detect conflicts.

Refactoring is a widely used development practice, available in mainstream IDEs. A previous work conducted a survey with developers, and finds that most of them use their experience to define refactoring mechanics for each refactoring type. However, we do not know whether a similar scenario happens in the context of refactoring tool developers. In this work, we conduct a study to compare refactoring mechanics implemented by tool developers. We apply 10 types of refactorings to 157,339 programs using 27 refactoring implementations from three tools, and compare the outputs. The refactoring implementations of Eclipse, NetBeans, and JRRT have different mechanics in all refactoring types.

Due to the risk of discharge sparks and ignition, there are strict rules concerning the safety of high voltage electrostatic systems used in industrial painting robots. In order to assure that the system fulfils its safety requirements, formal verification is an important tool to supplement traditional testing and quality assurance procedures. The work in this paper presents formal verification of the most important safety functions of a high voltage controller. The controller has been modelled as a finite state machine, which was formally verified using two different model checking software tools; Simulink Design Verifier and RoboTool. Five safety critical properties were specified and formally verified using the two tools. Simulink was chosen as a low-threshold entry point since MathWorks products are well known to most practitioners. RoboTool serves as a software tool targeted towards model checking, thus providing more advanced options for the more experienced user. The comparative study and results show that all properties were successfully verified. The verification times in both tools were in the order of a few minutes, which was within the acceptable time limit for this particular application.

Dementia is a disease that is characterized by the gradual loss of memory and cognition of patients due to the death of neurons. The future perspective is that the number of patients will increase, due to the aging of the population, reaching up to one third of the world population over 65 years. Alzheimer’s disease is the most common form of dementia and there is no medication to prevent or cure the disease. In this sense, the discovery of an efficient treatment for the disease is a real need, and the repositioning of drugs and in silico techniques can contribute to this purpose. Computational methods, such as Statistical Model Checking, which is a formal verification technique, contribute to this field of research, aiding to analyze the evolution of the protein and drugs interactions at a lower cost than the laboratory experiments. In this work, we present a model of the PI3K/AKT/mTOR pathway and we connected it with Tau and A\(\beta \), which are two important proteins that contribute to the evolution of Alzheimer’s disease. We analyzed the effect of rapamycin, an immunosuppressive drug, on those proteins. Our results show that this medicine has the potential to slow down one of the biological processes that causes neuronal death. In addition, we could show the formal model verification technique can be an efficient tool to design pharmacological strategies reducing experimental cost.

We showcase a modular, graphical language—graphical linear algebra—and use it as high-level language to reason calculationally about linear algebra. We propose a minimal framework of six axioms that highlight the dualities and symmetries of linear algebra, and use the resulting diagrammatic calculus as a convenient tool to prove a number of diverse theorems. Our work develops a relational approach to linear algebra, closely connected to classical relational algebra.

We propose a new model for data processing programs. Our model generalizes the data flow programming style implemented by systems such as Apache Spark, DryadLINQ, Apache Beam and Apache Flink. The model uses directed acyclic graphs (DAGs) to represent the main aspects of data flow-based systems, namely, operations over data (filtering, aggregation, join) and program execution, defined by data dependence between operations. We use Monoid Algebra to model operations over distributed, partitioned datasets and Petri Nets to represent the data flow. This approach allows the data processing program specification to be agnostic of the target Big Data processing system. As a first application of the model, we used it to formalize mutation operators for the application of mutation testing in Big Data processing programs. The testing tool TRANSMUT-Spark implement these operators.

Given a consistent timed scenario, we use its stable distance table, which is a canonical representation for the entire class of equivalent scenarios, to optimise a scenario. We present a general algorithm that can be combined with different heuristics in order to achieve different optimisation goals. In the limited setting of scenarios this algorithm is stronger than the DBM reduction technique.

Fuzzy Switch Graphs (FSG) generalize the notion of Fuzzy Graphs by adding high-order arrows and aggregation functions which update the fuzzy values of arrows whenever a zero-order arrow is crossed. In this paper, we propose a more general structure called Reversal Fuzzy Switch Graph (RFSG), which promotes other actions in addition to updating the fuzzy values of the arrows, namely: activation and deactivation of the arrows. RFSGs are able to model dynamical aspects of some systems which generally appear in engineering, computer science and some other fields. The paper also provides a logic to verify properties of the modelled system and closes with an application.

Filesystems have held the interest of the formal verification community for a while, with several high-performance filesystems constructed with accompanying proofs of correctness. However, the question of verifying an existing filesystem and incorporating filesystem-specific guarantees remains unexplored, leaving those application developers underserved who need to work with a specific filesystem known to be fit for their purpose. In this work, we present an implementation of a verified filesystem which matches the specification of an existing filesystem, and with our new model AbsFAT tie it to the reasoning framework of separation logic in order to verify properties of programs which use the filesystem. This work is intended to match the target filesystem, FAT32, at a binary level and return the same data and error codes returned by mature FAT32 implementations, considered canonical. We provide a logical framework for reasoning about program behavior when filesystem calls are involved in terms of separation logic, and adapt it to simplify and automate the proof process in ACL2. By providing this framework, we encourage and facilitate greater adoption of software verification by application developers.

Likewise to code, clone-and-own is a common way to create variants of a model, to explore the impact of different features while exploring the design of a software system. Previously, we have introduced Colorful Alloy, an extension of the popular Alloy language and toolkit to support feature-oriented design, where model elements can be annotated with feature expressions and further highlighted with different colors to ease understanding. In this paper we propose a catalog of refactorings for Colorful Alloy models, and show how they can be used to iteratively merge cloned Alloy models into a single feature-annotated colorful model, where the commonalities and differences between the different clones are easily perceived, and more efficient aggregated analyses can be performed.

Software product lines are an engineering approach to systematically build similar software products from a common asset base. When evolving such systems, it is important to have assurance that we are not introducing errors or changing the behavior of existing products. The product line refinement theory establishes the necessary conditions for such assurance. This theory has been specified and proved using the PVS proof assistant. However, the Coq proof assistant is increasingly popular among researchers and practitioners, and, given that some programming languages are already formalized into such tool, the refinement theory might benefit from the potential integration. Therefore, in this work we present a case study on porting the PVS specification of the refinement theory to Coq. We compare the proof assistants based on the noted differences between the specifications and proofs of this theory, providing some reflections on the tactics and strategies used to compose the proofs. According to our study, PVS provided more succinct definitions than Coq, in several cases, as well as a greater number of successful automatic commands that resulted in shorter proofs. Despite that, Coq also brought facilities in definitions such as enumerated and recursive types, and features that support developers in their proofs.

When evolving a software product line, it is often important to ensure that we do it in a safe way, ensuring that the resulting product line remains well-formed and that the behavior of existing products is not affected. To ensure this, one usually has to analyze the different artifacts that constitute a product line, like feature models, configuration knowledge and assets. Manually analyzing these artifacts can be time-consuming and error prone, since a product line might consist of thousands of products. Existing works show that a non-negligible number of changes performed in commits deal only with the configuration knowledge, that is, the mapping between features and assets. This way, in this paper, we propose a set of algebraic laws, which correspond to bi-directional transformations for configuration knowledge models, that we can use to justify safe evolution of product lines, when only the configuration knowledge model changes. Using a theorem prover, we proved all laws sound with respect to a formal semantics. We also present a case study, where we use these laws to justify safe evolution scenarios of a non trivial industrial software product line.