AFM17: Papers with Abstracts

Abstract. State-based transition systems can take advantage of a symbolic representation of the concepts of state and transition in order to automatically solve verification questions that could not be otherwise tackled in terms of explicit representation of the transition system. We report here our experience in developing solutions, approaches and supporting tools of verification problems regarding the Abstract State Machines (ASMs), a transition system which can be considered as an extension of Finite State Machines. We present the symbolic representation of an ASM and of its computational model in terms of the Yices SMT solver. We also discuss two scenarios of verification questions regarding the ASMs for which the symbolic representation helped us to formalize and solve the problem by satisfiability checking, namely automatic proof of correct ASM refinement and runtime verification.

Abstract. Virtually all real-valued computations are carried out using floating-point data types and operations. With increasing emphasis on overall computational efficiency, compilers are increasingly attempting to optimize floating-point expressions. Practical reasoning about the correctness of these optimizations requires error analysis procedures that are rigorous (ideally, they can generate proof certificates), can handle a wide variety of operators (e.g., transcendentals), and handle all normal programmatic constructs (e.g., conditionals and loops). Unfortunately, none of today’s approaches can achieve this combination. This position paper summarizes recent progress achieved in the community on this topic. It then showcases the component techniques present within our own rigorous floating-point precision tuning framework called FPTuner—essentially offering a collection of “grab and go” tools that others can benefit from. Finally, we present FPTuner’s limitations and describe how we can exploit contemporaneous research to improve it.

Abstract. Automated formal methods and automated reasoning are interconnected, as formal methods generate reasoning problems and incorporate reasoning techniques. For example, formal methods tools employ reasoning engines to find solutions of sets of constraints, or proofs of conjectures. From a reasoning perspective, the expressivity of the logical lan- guage is often directly proportional to the difficulty of the problem. In propositional logic, Conflict-Driven Clause Learning (CDCL) is one of the key features of state-of-the-art sat- isfiability solvers. The idea is to restrict inferences to those needed to explain conflicts, and use conflicts to prune a backtracking search. A current research direction in auto- mated reasoning is to generalize this notion of conflict-driven satisfiability to a paradigm of conflict-driven reasoning in first-order theories for satisfiability modulo theories and as- signments, and even in full first-order logic for generic automated theorem proving. While this is a promising and exciting lead, it also poses formidable challenges.

Abstract. Formal Methods (FM) have been around for decades and many have been improving all the time. Automated formal methods techniques and tools have been making a mark in real world applications across industry domains. So, why and where do we need more automation? How much automation is required? This paper attempts to cover an assessment on where I believe we are, based on my own not-so-limited but diverse enough experience in automated industry-strength formal methods and model based systems engineering area, where we might need to get to and possibly how. Key characteristics of future automation needed for success are outlined. No attempt is made to be exhaustive as the world of FMs is vast and the collective work of FM expert researchers, developers and users is needed for exploration – “to boldly meet future challenges which no FM has ever met before”!

Abstract. This article describes Salsa, an automatic tool to improve the accuracy of the floating- point computations done in numerical codes. Based on static analysis methods by abstract interpretation, our tool takes as input an original program, applies to it a set of transformations and then generates an optimized program which is more accurate than the initial one. The original and the transformed programs are written in the same imperative language. This article is a concise description of former work on the techniques implemented in Salsa, extended with a presentation of the main software architecture, the inputs and outputs of the tool as well as experimental results obtained by applying our tool on a set of sample programs coming from embedded systems and numerical analysis.

Abstract. Cyber-physical systems model physical phenomena, implicitly or explicitly, in order to interact with the real world. Representation of physical phenomena, including dimensionality and units, using the PVS type system provides users with the ability to create specifications that more accurately describe cyber-physical systems. This paper discusses two related libraries that each present a different approach to providing functionality for using units in PVS. Objectives in creating the libraries include: soundness, ease of use, ease of readability, and effect on provability.

Abstract. This paper presents a software development process for safety-critical software components of cyber-physical systems. The process is called MINERVA, which stands for Mirrored Implementation Numerically Evaluated against Rigorously Verified Algorithms. The process relies on formal methods for rigorously validating code against its requirements. The software development process uses: (1) a formal specification language for describing the algorithms and their functional requirements, (2) an interactive theorem prover for formally verifying the correctness of the algorithms, (3) test cases that stress the code, and (4) numerical evaluation on these test cases of both the algorithm specifications and their implementations in code. The MINERVA process is illustrated in this paper with an application to geo-containment algorithms for unmanned aircraft systems. These algorithms ensure that the position of an aircraft never leaves a predetermined polygon region and provide recovery maneuvers when the region is inadvertently exited.

Abstract. We present a brief tutorial on the PVS2C code generator for producing C code from an applicative fragment of the PVS specification language. This fragment roughly corresponds to a self-contained functional language. The tutorial covers the generation of C code for numeric data types and associated operations, arrays, recursive data types, and higher- order operations.