Maude-NPA is a formal verification tool for analyzing cryptographic protocols in the Dolev-Yao strand space model modulo an equational theory defining the cryptographic primitives. It starts from an attack state to find counterexamples or conclude that the attack concerned cannot be conducted by performing a backward narrowing reachability analysis. Although Maude-NPA is a powerful analyzer, its running performance can be improved by taking advantage of parallel and/or distributed computing when dealing with complex protocols whose state space is huge. This paper describes a parallel version of Maude-NPA in which the backward narrowing and the transition subsumption at each layer in Maude-NPA are conducted in parallel. A tool supporting the parallel version has been implemented in Maude with a master-worker model using meta-interpreters. We report on some experiments of various kinds of protocols that demonstrate that the tool can increase the running performance of Maude-NPA by 52% on average for complex case studies in which the number of states located at each layer is considerably large.

Abstract State Machine Graphical Animation (called SMGA) is a visualization tool that assists formal methods experts in conjecturing characteristics of a protocol/system. The characteristics guessed by using the tool can be used as lemma candidates to theorem prove that the protocol/system satisfies its desired properties. Because previous work has shown that interaction in SMGA is one promising factor to foster assistance, in this paper, we revise SMGA equipping it with various interactive features in order to help human users in conjecturing lemmas. Moreover, we integrate SMGA and Maude, a declarative language and high-performance tool, so that the revised version of SMGA (called r-SMGA) can use some powerful features of Maude, such as parsing associative-commutative binary operators as well as context-free grammars, reachability analysis, and model checking. We conduct a case study with the Suzuki-Kasami protocol to demonstrate the usefulness of these new features. In the case study, some characteristics are conjectured and confirmed with these features. Based on the guessed characteristics and assistance of r-SMGA, we successfully prove that the protocol enjoys the mutual exclusion property. Finally, we propose guidelines that can help users to conjecture characteristics using r-SMGA. Our result shows that the graphical animation approach is useful for lemma conjecture in theorem proving. The formal verification is a part of the case study.

The Robot Operating System (ROS) is a framework for building robust software for complex robot systems in several domains. The Navigation Stack stands out among the different libraries available in ROS, providing a set of components that can be reused to build robots with autonomous navigation capabilities. This library is a critical component, as navigation failures could have catastrophic consequences for applications like self-driving cars where safety is crucial. Here we devise a general methodology for verifying this kind of complex systems by specifying them in different executable specification languages with verification support and validating the equivalence between the specifications and the original system using differential testing techniques. The complex system can then be indirectly analyzed using the verification tools of the specification languages like model checking, semi-automated functional verification based on Hoare logic, and other formal techniques. In this paper we apply this verification methodology to the NavFn planner, which is the main planner component of the Navigation Stack of ROS, using Maude and Dafny as specification languages. We have formally proved several desirable properties of this planner algorithm like the absence of obstacles in the planned path. Moreover, we have found counterexamples for other concerns like the optimality of the path cost.

We devised the L +1-layer divide & conquer approach to leads-to model checking ( L +1-DCA2L2MC) and its parallel version, and developed sequential and parallel tools for L +1-DCA2L2MC. In a temporal logic called UNITY , designed by Chandy and Misra, the leads-to temporal connective plays an important role and many case studies have been conducted in UNITY, demonstrating that many systems requirements can be expressed as leads-to properties. Hence, it is worth dedicating to these properties. Counterexample generation is one of the main tasks in the L +1-DCA2L2MC technique that can be optimized to improve its running performance. This article proposes a technique to find all counterexamples at once in model checking with a new model checker. Furthermore, layer configuration selection is essential to make the best use of the L +1-DCA2L2MC technique. This work also proposes an approach to finding a good layer configuration for the technique with an analysis tool. Some experiments are conducted to demonstrate the power and usefulness of the two optimization techniques, respectively. Moreover, our sequential and parallel tools are compared with SPIN and LTSmin model checkers, showing a promising way to mitigate the state space explosion and improve the running performance of model checking when dealing with large state spaces.

Databases are a key subject in several technical degrees.Because they have a strong practical nature, students require a large number of problems to master them.However, these problems are useful only if accurate and timely feedback is provided.In this paper, we present the learning improvements obtained by using LearnSQL, an automatic judge that has been designed to complement face-to-face lectures.We have measured the impact of this judge during the 2021/22 academic year and report promising results both in student engagement and final grades.

CafeOBJ is a language for specifying and verifying a wide variety of software and/or hardware systems. Traditionally, verification has been carried out via proof scores, which consist of reducing goal-related terms in user-defined modules. Although proof scores are semi-formal (the specifier is partially responsible for soundness), their flexibility makes them a useful approach to verification. For the last years, we have developed different formal tools around the CafeInMaude interpreter, a CafeOBJ interpreter implemented in Maude. Besides supporting proof scores, we implemented a theorem prover, a proof script generator from proof scores, and the first stages of a proof script generator and fixer-upper. In this paper, we present (i) an improved and detailed version of our proof script generator and fixer-upper and (ii) a reimplementation of the CafeInMaude interpreter, which supports, among others, parallel execution, an improved tool integration, and an interactive user interface. The benchmarks used to evaluate the tools confirm the usefulness of the approach.

Abstract Stream processing has reached the mainstream in the last years, as a new generation of open-source distributed stream processing systems, designed for scaling horizontally on commodity hardware, has brought the capability for processing high-volume and high-velocity data streams to companies of all sizes. In this work, we propose a combination of temporal logic and property-based testing (PBT) for dealing with the challenges of testing programs that employ this programming model. We formalize our approach in a discrete time temporal logic for finite words, with some additions to improve the expressiveness of properties, which includes timeouts for temporal operators and a binding operator for letters. In particular, we focus on testing Spark Streaming programs written with the Spark API for the functional language Scala, using the PBT library ScalaCheck. For that we add temporal logic operators to a set of new ScalaCheck generators and properties, as part of our testing library sscheck.

Transition systems provide a natural way to specify and reason about the behaviour of discrete systems, and in particular about the computations that they may perform. This paper advances a verification method for transition systems whose reachable states are described explicitly by membership axioms. The proof technique is implemented in the Constructor-based Inductive Theorem Prover (CITP), a proof management tool built on top of a variation of conditional equational logic enhanced with many modern features. This approach complements the so-called OTS method, a verification procedure for observational transition systems that is already implemented in CITP.

CafeOBJ is a language for writing formal specifications for a wide variety of software and hardware systems and for verifying their properties. CafeOBJ makes it possible to verify properties by using either proof scores, which consists of reducing goal-related terms in user-defined modules, or by using theorem proving. While the former is more flexible, it lacks the formal support to ensure that a property has been really proven. On the other hand, theorem proving might be too strict, since only a predefined set of commands can be applied to the current goal; hence, it hardens the verification of properties. In order to take advantage of the benefits of both techniques, we have extended CafeInMaude, a CafeOBJ interpreter implemented in Maude, with the CafeInMaude Proof Assistant (CiMPA) and the CafeInMaude Proof Generator (CiMPG). CiMPA is a proof assistant for proving inductive properties on CafeOBJ specifications that uses Maude metalevel features to allow programmers to create and manipulate CiMPA proofs. On the other hand, CiMPG provides a minimal set of annotations for identifying proof scores and generating CiMPA scripts for these proof scores. In this article, we present the CiMPA and CiMPG, detailing the behavior of the CiMPA and the algorithm underlying the CiMPG and illustrating the power of the approach by using the QLOCK protocol. Finally, we present some benchmarks that give us confidence in the matureness and usefulness of these tools.

Abstract We present in this paper an interpreter implemented in Maude for non-behavioral CafeOBJ specifications. This alternative implementation poses a number of advantages: (1) it allows Maude tools to be used with CafeOBJ specifications, (2) it improves the performance of some CafeOBJ commands, such as search, (3) it enriches CafeOBJ syntax with Maude syntax, and (4) it makes CafeOBJ easily extensible, since new commands and tools can be included and tested and, once they are sufficiently mature, can be considered for inclusion in the Lisp implementation of CafeOBJ. The current tool presents a number of improvements over the tool presented in previous papers: it supports principal sorts, all kinds of CafeOBJ views, and all the search predicates recently implemented in the system. These improvements have allowed us to run the most recent CafeOBJ specifications, hence proving the robustness of the tool. Moreover, we present case studies illustrating the power of the tool, focusing on the falsification and verification of the NSPK and QLOCK protocols, respectively.

Abstract Modern functional logic programming (FLP) languages use non-terminating and non-confluent constructor systems (CSs) as programs in order to define non-strict and non-deterministic functions. Two semantic alternatives have been usually considered for parameter passing with this kind of functions: call-time choice and run-time choice. While the former is the standard choice of modern FLP languages, the latter lacks some basic properties – mainly compositionality – that have prevented its use in practical FLP systems. Traditionally it has been considered that call-time choice induces a singular denotational semantics, while run-time choice induces a plural semantics. We have discovered that this latter identification is wrong when pattern matching is involved, and thus in this paper we propose two novel compositional plural semantics for CSs that are different from run-time choice. We investigate the basic properties of our plural semantics – compositionality, polarity, and monotonicity for substitutions, and a restricted form of the bubbling property for CSs – and the relation between them and to previous proposals, concluding that these semantics form a hierarchy in the sense of set inclusion of the set of values computed by them. Besides, we have identified a class of programs characterized by a simple syntactic criterion for which the proposed plural semantics behave the same, and a program transformation that can be used to simulate one of the proposed plural semantics by term rewriting. At the practical level, we study how to use the new expressive capabilities of these semantics for improving the declarative flavor of programs. As call-time choice is the standard semantics for FLP, it still remains the best option for many common programming patterns. Therefore, we propose a language that combines call-time choice and our plural semantics, which we have implemented in the Maude system. The resulting interpreter is then employed to develop and test several significant examples showing the capabilities of the combined semantics.

Non-strict non-deterministic functions are one of the most distinctive features of functional-logic languages. Traditionally, two semantic alternatives have been considered for this kind of functions: call-time choice and run-time choice. While the former is the standard choice of modern implementations of FLP, the latter lacks some basic properties--mainly compositionality--that have prevented its use in practical FLP implementations. Recently, a new compositional plural semantics for FLP has been proposed. Although this semantics allows an elegant encoding of some problems--in particular those with an implicit manipulation of sets of values--, call-time choice still remains the best option for many common programming patterns.

Declarative debugging is a semi-automatic technique that starts from an incorrect computation and locates a program fragment responsible for the error by building a tree representing this computation and guiding the user through it to find the error. Membership equational logic (MEL) is an equational logic that in addition to equations allows the statement of membership axioms characterizing the elements of a sort. Rewriting logic is a logic of change that extends MEL by adding rewrite rules, that correspond to transitions between states and can be nondeterministic. In this paper we propose a calculus that allows to infer normal forms and least sorts with the equational part, and sets of reachable terms through rules. We use an abbreviation of the proof trees computed with this calculus to build appropriate debugging trees for missing answers (results that are erroneous because they are incomplete), whose adequacy for debugging is proved. Using these trees we have implemented a declarative debugger for Maude, a high-performance system based on rewriting logic, whose use is illustrated with an example.