Abstract Small round-off errors in safety-critical systems can lead to catastrophic consequences. In this context, determining if the result computed by a floating-point program is accurate enough with respect to its ideal real-number counterpart is essential. This paper presents PRECiSA 4.0, a tool that rigorously estimates the accumulated round-off error of a floating-point program. PRECiSA 4.0 combines static analysis, optimization techniques, and theorem proving to provide a modular approach for computing a provably correct round-off error estimation. PRECiSA 4.0 adds several features to previous versions of the tool that enhance its applicability and performance. These features include support for data collections such as lists, records, and tuples; support for recursion schemas; an updated floating-point formalization that closely characterizes the IEEE-754 standard; an efficient and modular analysis of function calls that improves the performances for large programs; and a new user interface integrated into Visual Studio Code.

The Integrated and Configurable Algorithms for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture being developed for the robust integration of mission-specific software modules and highly assured core software modules. This paper reports on the use of automatic reachability analysis during the development of ICAROUS, as a first step towards a broader formal verification effort of the software architecture. It explains how simulation based on state-space exploration and LTL model checking has been performed on a formal executable specification of the system in rewriting logic. Overall, this effort has unveiled issues such as deadlocks and undesired behavior, and has helped improve the ICAROUS design and source code.

Formal specifications can be used for various software engineering activities ranging from finding errors to documenting software and automatic test-case generation. Automatically discovering specifications for heap-manipulating programs is a challenging task. In this paper, we propose a technique for automatically inferring formal specifications from C code which is based on the symbolic execution and automated reasoning tandem "Matching Logic/K framework". We implemented our technique for a fragment of C called KernelC, in the automated tool KingSpec, which generates axioms that describe the precise input/output behavior of C routines that handle pointer-based structures, i.e., result values and state change. These specifications can be written either in Matching Logic itself, which is useful for further automated analysis within the K formal environment, or in sugared axiomatic form, which favors better human inspection. Since we rely on rewriting logic K semantics specification of programming languages, our approach can be easily extended to any language for which %that a formal semantics in K is given.

This paper presents a technique to automatically infer algebraic property-oriented specifications from first-order Curry programs. Curry is a lazy functional logic language and the interaction between laziness and logical variables raises some additional difficulties with respect to other proposals for functional languages. Our technique statically infers from the source code of a Curry program a specification which consists of a set of equations relating (nested) operation calls that have the same behavior. We propose a (glass-box) semantic-based inference method which relies on a fully-abstract (condensed) semantics for achieving, to some extent, the correctness of the inferred specification, differently from other (black-box) approaches based on testing techniques.