Skip to main content


Formal Methods in System Design

An International Journal

Formal Methods in System Design OnlineFirst articles


Exact quantitative probabilistic model checking through rational search

Model checking systems formalized using probabilistic models such as discrete time Markov chains (DTMCs) and Markov decision processes (MDPs) can be reduced to computing constrained reachability properties. Linear programming methods to compute …


Abstraction refinement and antichains for trace inclusion of infinite state systems

A generic register automaton is a finite automaton equipped with variables (which may be viewed as counters or, more generally, registers) ranging over infinite data domains. A trace of a generic register automaton is an alternating sequence of …

15.04.2020 Open Access

Model checking boot code from AWS data centers

This paper describes our experience with symbolic model checking in an industrial setting. We have proved that the initial boot code running in data centers at Amazon Web Services is memory safe, an essential step in establishing the security of …


Parameterized verification of algorithms for oblivious robots on a ring

We study verification problems for autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives. In particular, we focus in this paper on the model proposed by Suzuki and Yamashita of anonymous robots evolving in …

26.02.2019 Open Access

Incremental column-wise verification of arithmetic circuits using computer algebra

Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning over pseudo boolean …

Aktuelle Ausgaben

Über diese Zeitschrift

Formal Methods in System Design reports on the latest formal methods for designing, implementing, and validating the correctness of hardware (VLSI) and software systems. Readers will find high quality, original papers describing all aspects of research and development. Contributions to the journal serve its goal of developing an important and highly useful collection of commonly applicable formal methods that will strongly influence future design environments and design methods.

Weitere Informationen

Premium Partner