Hardware and software systems will inevitably grow in scale and functionality. Because of
this increase in complexity, the likelihood of subtle errors is much greater. Moreover, some of …

A comprehensive introduction to the foundations of model checking, a fully automated
technique for finding flaws in hardware and software; with extensive examples and both …

Despite the automation, users of finite-state verification tools still must be able to specify the
system requirements in the specification language of the tool. This is more challenging than …

Verification by state-space exploration, also often referred to as" model checking", is an
effective method for analyzing the correctness of concurrent reactive systems (eg …

We present algorithms for computing similarity relations of labeled graphs. Similarity
relations have applications for the refinement and verification of reactive systems. For finite …

Finite-state verification(eg, model checking) provides a powerful means to detect errors that
are often subtle and difficult to reproduce. Nevertheless, the transition of this technology from …

This paper informally presents the theoretical and practical foundations of synchronous
programming of reactive systems, mostly focusing on the author's Esterel language …

Automated and semi-automated manipulation of so-called labelled transition systems has
become an important means in discovering flaws in software and hardware systems …

The CSP approach has been widely used in the specification, analysis and verification of
concurrent and real-time systems, and for understanding the particular issues that can arise …

MOCHA: Modularity in model checking Page 1 MOCHA: Modularity in Model Checking* R. Alur
l, TA Henzinger 2, EY.C. Mang 2, S. Qadeer 2, SK Rajamani z, and S. Tasiran 2 ! Computer & …