This special issue of the Journal on Formal Methods in System Design features extended and revised versions of select contributions presented at the 2017 Conference on Formal Methods in Computer-Aided Design (FMCAD 2017) [9]. The FMCAD conference focuses on theoretical results and tools in the field of automated verification and formal methods, and provides a leading forum that brings together researchers in academia and industry.

FMCAD 2017 was held from October 2 to October 6, 2017, in Vienna, Austria. In addition to the invited and contributed talks, the conference included a tutorial day, a student forum providing a platform for graduate students to present their research [6], and a symposium in memoriam Helmut Veith [3].

This special issue contains the following six contributions, all of which were reviewed by at least two experts in at least two rounds of peer review:

  • Incremental Column-Wise Verification of Arithmetic Circuits Using Computer Algebra is an extended version of [7], the publication which won the Best Paper Award at FMCAD 2017. The authors present an incremental technique that uses Gröbner bases to verify that a gate-level representation adheres to its specification.

  • Parameterized Verification of Algorithms for Oblivious Robots on a Ring (which extends [8]) studies the verification of autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives, and is the first work that focuses on the parameterized case of this setting.

  • First-Order Temporal Logic Monitoring with BDDs, based on [5], deploys Binary Decision Diagrams to representing data observed during program executions, which leads to substantial performance improvements.

  • Exact Quantitative Probabilistic Model Checking Through Rational Search, based on [1], presents a new automated model checking algorithm that improves approximate verification results for probabilistic models by using scalable iterative techniques to compute exact reachability probabilities.

  • Automated Repair By Example for Firewalls is based on [4] and describes FireMason, a tool that uses automated decision procedures to automatically repair firewalls, where the correct behavior is specified in terms of examples.

  • Learning Inductive Invariants by Sampling from Frequency Distributions, an extended version of [2], presents a probabilistic, syntax-guided method to discover inductive invariants.

We thank the authors for their excellent work, all reviewers for their time and valuable suggestions for improving the manuscripts, and Daniel Kroening, the FMSD Editor in Chief, for his support.