Software model checking Page 1 21 Software Model Checking RANJIT JHALA University of
California, San Diego and RUPAK MAJUMDAR University of California, Los Angeles We survey …

This paper presents a general theory of system composition for" possibilistic" security
properties. We see that these properties fall outside of the Alpern-Schneider safety/liveness …

Abstract Synchronous programming [20, 14] is a useful approach to design reactive systems.
A synchronous program is supposed to instantly and deterministically react to events coming …

This is a tutorial introduction to assertional reasoning based on temporal logic. The objective
is to provide a working familiarity with the technique. We use a simple system model and a …

Yet, the structure of mathematical proofs has not changed in 300 years. The proofs in
Newton's Principia differ in style from those of a modern textbook only by being written in …

Formally defines a wide variety of separation-of-duty (SoD) properties, including the best
known to date, and establishes their relationships within a formal model of role-based …

Traditional methods for specifying and reasoning about concurrent systems work for real-
time systems. However, two problems arise: the real-time programming version of Zeno's …

We present a general theory of possibilistic security properties. We show that we can
express a security property as a predicate that is true of every set containing all the traces …

Since the initial work of Daryl McCullough (1987) on the subject, the security community has
struggled with the problem of composing" possibilistic" information-flow properties. Such …

The distinction of safety and liveness properties is often adopted in speci cation and design
methods for distributed systems. We present a short survey on the\history" of these concepts …