Browse Books

The complexity class PSPACE is one of the most robust concepts in contemporary computer science. Aside from the fact that space is invariant (for reasonable models at least) up to a constant factor, the class can be characterized in many alternative ...

In this discursive paper we discuss compositionality of (i) simple entities, (ii) operations, (iii) events, and (iv) behaviours. These four concepts, (i)–(iv), together define a concept of entities. We view entities as “things” characterised by ...

Computer science is largely about computation. Many kinds of computing devices have been described, some abstract and some very concrete. Among them are:

Automata, including Turing machines, Moore machines, Mealy machines, pushdown automata, and ...

For many programming languages, the only formal semantics published is an SOS big-step semantics. Such a semantics is not suited for investigations that observe intermediate states, such as invariant techniques. In this paper, a construction is proposed ...

Trojan horses of Thompson-Goerigk-type are intended software errors very hidden in machine level compiler implementations although the latter have successfully passed Wirth's strong compiler bootstrapping test and there have been done rigorous ...

In explicit fair schedulers, auxiliary integer-valued scheduling variables with non-deterministic assignments and with decrements keep track of each processor's relative urgency. Every scheduled execution is fair and yet, the scheduler is sufficiently ...

To find congruence relations proved more difficult for synchronous message passing than for asynchronous message passing. As well-known, trace equivalence of state-machines, which represents to a congruence relation for asynchronous computations, is not ...

In this paper an assertional proof method is introduced which captures concurrent systems consisting of dynamically created recursive processes which interact via shared-variables. The main contribution is a generalization of the Owicki & Gries proof ...

To support model-based development and analysis of embedded systems, the specification language VDM++ has been extended with asynchronous communication and improved timing primitives. In addition, we have defined an interface for the co-simulation of a ...

Due to advances in hardware architectures such as multi-core/multi-threaded architectures, various refinements of the parallel programming models such as distributed shared space, global address space and partitioned global address space (PGAS) etc., ...

Services are autonomous, self-describing, technology-neutral software units that can be described, published, discovered, and composed into software applications at run-time. Designing software services and composing services in order to form ...

We investigate the power of play-out, the execution mechanism associated with scenario-based programming, which was defined as the operational semantics of live sequence charts (LSC). We compare some of the play-out strategies and mechanisms suggested ...

The paper presents an automatic method to derive a deductive proof of response properties from symbolic model checking. The method is based on a new proof rule for response properties that deals directly with compassion (strong fairness). The method can ...

Model checking was introduced in the early 1980's to provide a practical automated method for verifying concurrent systems. Model checking has had substantive impact on program verification. For the first time industrial strength systems are being ...

The success of applying model-checking to large systems depends crucially on the choice of good abstractions. In this work we present an approach for constructing abstractions when checking Next-free universal CTL* properties. It is known that ...

This paper reports spreadsheet calculations intended to verify the timing of 6-4 GasP asynchronous Network on Chip (NoC) control circuits. The Logical Effort model used in the spreadsheet estimates the delays of each logic gate in the GasP control. The ...

Starting from the perspective of safety-critical systems development in avionics, railways and the automotive domain, we advocate an integrated verification approach for C/C++ modules combining abstract interpretation, formal verification and ...

Chosen-ciphertext security is by now a standard security property for asymmetric encryption. Many generic constructions for building secure cryptosystems from primitives with lower level of security have been proposed. Providing security proofs has also ...

In this work we introduce counterexample guided path reduction based on interval constraint solving for static program analysis. The aim of this technique is to reduce the number of false positives by reducing the number of feasible paths in the ...