Bøger i Atlantis Studies in Computing serien

In this monograph we introduce and examine four new temporal logic formalisms that can be used as specification languages for the automated verification of the reliability of hardware and software designs with respect to a desired behavior.

The subjects from the area of computer architecture, to wit instruction sequence performance, instruction set architectures and remote instruction processing, are usually not investigated in a rigorous way at all.

Templates are a tool for programmers, and implementations of template engines are most times based on practical experience rather than based on a theoretical background. This book reveals the mathematical background of templates and shows interesting findings for improving the practical use of templates.

In this book we develop powerful techniques based on formal methods for the verification of correctness, consistency and safety properties related to dynamic reconfiguration and communication in complex distributed systems. In particular, static analysis techniques based on types and type systems are an adequate methodology considering their success in guaranteeing not only basic safety properties, but also more sophisticated ones like deadlock or lock freedom in concurrent settings.The main contributions of this book are twofold.i) We design a type system for a concurrent object-oriented calculus to statically ensure consistency of dynamic reconfigurations.ii) We define an encoding of the session pi-calculus, which models communication in distributed systems, into the standard typed pi-calculus. We use this encoding to derive properties like type safety and progress in the session pi-calculus by exploiting the corresponding properties in the standard typed pi-calculus.

This book describes the benefits that emerge when the fields of constraint programming and concurrency meet. On the one hand, constraints can be used in concurrency theory to increase the conciseness and the expressive power of concurrent languages from a pragmatic point of view.

Data compression is mandatory to manage massive datasets, indexing is fundamental to query them.