AFM17: Editor's Preface

The 2017 Automated Formal Methods Workshop (http://fm.csl.sri.com/AFM17/) took place in Menlo Park during May 19-20, 2017.  This workshop was originally initiated as a users' group meeting for the SRI formal verification tools, which now include PVS, SAL, HybridSAL, SALLY, Yices, NL-Yices, Joogie, Bixie, and SeaHorn, together with technologies under development, such as ARSENAL, Radler, PCE, and ETB.   However, topics were not restricted to these tools but were more generally scoped to cover all aspects of state-of-the-art automation in tool-supported formal methods.   Prior versions of the AFM workshop were held in 2006, 2007, 2008, 2009, and 2010. 

The program for the workshop included contributed papers as well as tool tutorials.   The tutorials include

1. Yices~2 by Bruno Dutertre (SRI Computer Science Laboratory)
2.  Sally by Dejan Jovanovic (SRI Computer Science Laboratory)
3. SeaHorn by Jorge Navas (SRI Computer Science Laboratory)
4.  PVS by Sam Owre (SRI Computer Science Laboratory)
5. Radler by Leonard Gerard (currently at Abundant Robotics)
6. Hybrid SAL by Ashish Tiwari (currently at Microsoft)
7. TeLeX runtime temporal verifier (SRI Computer Science Laboratory)
8. ARSENAL natural language requirements processor by Shalini Ghosh (SRI Computer Science Laboratory)

The contributed papers collected in this volume cover the presentations at the workshop.  Arun Chakrapani Rao (University of Warwick) in his paper More Automated Formal Methods?! If so, why, where & how? makes a case for viewing the role of automation in formal methods within the entire design process.   Automation, he argues, should be balanced with the need for connectivity between design layers as well as the usability of the tools.  He draws on his experience with different formal technologies, e.g., requirements analysis, model checking, property specification, static analysis,  and test generation, to illustrate this holistic and synergistic view of the use of automated formal methods.

In their paper entitled The MINERVA Software Development Process, Anthony Narkawicz, Cesar Munoz, and  AaronDutle (NASA Langley Research Center) outline a software process called MINERVA for Mirrored Implementation Numerically Evaluated against Rigorously Verified Algorithms.  In this process, the software routines are rigorously specified and developed using a theorem prover in parallel with the actual (unverified) software.  Test cases are then generated to ensure that the unverified software and its verified counterpart are in concordance. The power of the MINERVA approach, which has been applied in a number of NASA air-traffic management designs,  is illustrated with an extensive case study involving  geo-containment algorithms for an unmanned aircraft.  

Maria Paola Bonacina (Universita degli Studi di Verona), in her paper entitled On Conflict-Driven Reasoning, presents an overview of the conflict-driven paradigm for automated reasoning.  This approach to satisfiability and verification problems combines search and inference in an interesting way. Whenever the search process produces a conflict (a partial or complete solution that violates the search constraints), inference is used to explain the conflict and to learn new constraints that direct the search away from similarly conflicting search paths.  These techniques were first introduced in Boolean satisfiability solving (SAT) and have slowly made their way to Satisfiability Modulo Theories (SMT), first-order reasoning, as well as model checking.  

The paper, Salsa: An Automatic Tool to Improve the Numerical Accuracy of Programs by Nasrine Damouche and Matthieu Martel (Université de Perpignan Via Domitia),  describes the Salsa tool which transforms a program representing a floating-point computation to an equivalent one with a smaller floating-point error.  Transformations take place at the level of expressions, procedure, and procedure calls to modify and specialize the code in order to reduce the error.  This reduction is demonstrated on several benchmarks.  

Paolo Arcaini (Charles University), Angelo Gargantini (University of Bergamo), and Elvinia Riccobene (University of Milan) in their paper entitled SMT for state-based formal methods: the ASM case study define a translation from Abstract State Machines, a powerful and flexible model of computation, to the language of the Yices SMT solver.  This translation is used for symbolic execution, for verifying refinement relations between transition systems, and for runtime verification against Java executions.  

Ben Hocking and Anthony Aiello (Dependable Computing) describe two PVS libraries for encoding units of measurement in their paper entitled The Measurement Library: Representing Physical Types in PVS.  Errors involving mismatched units and dimensions are quite common in programming.  The first library employs a measurement template that, in addition to the value, maintains the scaling and dimensions (length, mass, time, etc.) of the reading.  Subtyping is used to ensure that operations are well-typed by matching dimensions and units.  This approach allows measurements that combine metric and imperial units.  The second library ensures that all the values in a computation are in a single system of measurements.  These PVS libraries have been used to support reasoning about Simulink operations.

The paper by Marek Baranowski, Ian Briggs, Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric and Alexey Solovyev (University of Utah) entitled Moving the Needle on Rigorous Floating-Point Precision Tuning surveys the work on optimization of floating point operations and describe their FPTuner optimization tool.  The FPTuner toolchain uses a number of other error analysis and optimization tools  to achieve mixed-precision tuning of the operands and operations in a floating-point computation.  

The paper A Brief Introduction to the PVS2C Code Generator by Natarajan Shankar (SRI) describes the generation of C code from executable functions in the PVS higher-order logic.  The code generator uses an intermediate language based on A-normal form to construct C code for a full functional fragmentof the higher-order logic with support for reference counting, memory management, fixed and multi-precision arithmetic, arrays, tuples, records, recursive datatypes,and closures.  

These papers demonstrate the range and power of modern automated formal methods and also capture the significant research challenges involved in facilitating the broader use of formal techniques.

Finally, we wish to thank the team at Easychair and Kalpa Publications for their excellent support.