Berard, B., Ecole Normale Superieure de Cachan, France et al.

Systems and Software Verification
Model-Checking Techniques and Tools

2001. XII, 196 pp. Hardcover
3-540-41523-8

Model checking is a powerful approach for the formal verification of software. When applicable, it automatically provides complete proofs of correctness, or explains, via counter-examples, why a system is not correct.
This book provides a basic introduction to this new technique. The first part describes in simple terms the theoretical basis of model checking: transition systems as a formal model of systems, temporal logic as a formal language for behavioral properties, and model-checking algorithms. The second part explains how to write rich and structured temporal logic specifications in practice, while the third part surveys some of the major model checkers available.

Keywords: Software Verification, Model Checking, Transition Systems, Temporal Logics, Tools

Contents: Part I : Principles and Techniques: Introduction; 1. Automata; 2. Temporal Logic; 3. Model Checking; 4. Symbolic Model Checking; 5. Timed Automata; Conclusion. Part II: Specifying with Temporal Logic: Introduction; 6. Reachability Properties; 7. Safety Properties; 8. Liveness Properties; 9. Deadlock-freeness; 10. Fairness Properties; 11. Abstraction Methods; Conclusion. Part III : Some Tools: Introduction; 12. SMV - Symbolic Model Checking; 13. Spin - Communication Automata; 14. Design/CPN - Coloured Petri Nets; 15. Uppaal - Timed Systems; 16. Kronos - Model Checking of Real-time Systems; 17. HyTech - Linear Hybrid Systems; Main Bibliography; Index.

Derrick, J., University of Kent at Canterbury, UK
Boiten, E.A., University of Kent at Canterbury, UK

Refinement in Z and Object-Z
Foundations and Advanced Applications

2001. XVIII, 466 pp. Softcover
1-85233-245-X

Refinement is one of the cornerstones of the formal approach to software engineering, and its use in various domains has led to research on new applications and generalisation. This book brings together this important research in one volume, with the addition of examples drawn from different application areas. It covers four main themes:
- data refinement and its application to Z;
- generalisations of refinement that change the interface and atomicity of operations;
- refinement in Object-Z;
- and modelling state and behaviour by combining Object-Z with CSP.
Refinement in Z and Object-Z: Foundations and Advanced Applications provides an invaluable overview of recent research for academic and industrial researchers, lecturers teaching formal specification and development, industrial practitioners using formal methods in their work, and postgraduate and advanced undergraduate students.

Series: Formal Approaches to Computing and Information Technology (FACIT).

Lomax, H. / Pulliam, T.H., NASA Ames Research Center, Moffett Field, CA, USA
Zingg, D.W., University of Toronto, Ont., Canada

Fundamentals of Computational Fluid Dynamics

2001. XIV, 249 pp. 25 figs., 11 tabs. Hardcover
3-540-41607-2

This book is intended as a textbook for a first course in computational fluid dynamics and will be of interest to researchers and practitioners as well. It emphasizes fundamental concepts in developing, analyzing, and understanding numerical methods for the partial differential equations governing the physics of fluid flow. The linear convection and diffusion equations are used to illustrate concepts throughout. The chosen approach, in which the partial differential equations are reduced to ordinary differential equations, and finally to difference equations, gives the book its distinctiveness and provides a sound basis for a deep understanding of the fundamental concepts in computational fluid dynamics.

Keywords: Numerical Methods .

Series: Scientific Computation.

Seed, G.M., Heriot-Watt University, Edinburgh, UK

An Introduction to Object-Oriented Programming in C++
with applications in Computer Graphics

2nd extended and rev.ed. 2001. XL, 972 pp. Softcover
1-85233-450-9

An Introduction to Object-Oriented Programming in C++ with applications in Computer Graphics introduces the reader to programming in C++ step by step from the simplest of C++ programs, through features such as classes and templates to namespaces. Emphasis is placed on developing a good programming technique and demonstrating when and how to use the more advanced features of C++ through the development of realistic programming tools and classes.
This revised and extended 2nd edition includes:
- the Standard Template Library (STL), a major addition to the ANSI C++ standard
- full coverage of all the major topics of C++, such as Templates; exception handling; RTTI
- practical tools developed for object-oriented computer graphics programming
All code program files and exercises are ANSI C++ compatible and have been compiled on both Borland C++ v5.5 and GNU/Linux g++ v2.91 compilers, and are available from the author's web site:
http://www.hw.ac.uk/mecWWW/research/staff/gms.htm

Contents: Overview.- The Development Environment.- Getting Started.- Fundamental Data Types, Declarations, Definitions and Expressions.- Making Decisions and Repetition.- Functions.- Arrays.- Structures, Unions, Enumerations and Typedefs.- The C++ Class.- Operators and Overloading.- Friends.- Pointers.- Templates.- Exception Handling.- Inheritance.- Run-Time Type Information and Casting.- Input and Output, Files and Streams.- The Preprocessor.- Namespaces.- The Standard Template Library.- Conclusion.- Appendices.- References.- Index.

Monod, N., ETH Zurich, Switzerland

Continuous Bounded Cohomology of Locally Compact Groups

2001. IX, 214 pp. Softcover
3-540-42054-1

Recent research has repeatedly led to connections between important rigidity questions and bounded cohomology. However, the latter has remained by and large intractable. This monograph introduces the functorial study of the continuous bounded cohomology for topological groups, with coefficients in Banach modules. The powerful techniques of this more general theory have successfully solved a number of the original problems in bounded cohomology. As applications, one obtains, in particular, rigidity results for actions on the circle, for representations on complex hyperbolic spaces and on Teichmu"ller spaces. A special effort has been made to provide detailed proofs or references in quite some generality.

Keywords: Bounded cohomology, continuous cohomology, lattices in Lie groups, rigidity theory . MSC ( 2000 ): 22E41, 55N35, 20J05, 20J06, 22E40

Contents: Introduction Chapter I Banach modules, $L^/infty$ spaces 1 Banach modules 2 $L^/infty$ spaces 3 Integration Chapter II Relative injectivity and amenable actions 4 Relative injectivity 5 Amenability and amenable actions Chapter III Definition and characterization of continuous bounded cohomology 6 A naive definition 7 The functorial characterization 8 Functoriality 9 Continuous cohomology and the comparison map Chapter IV Cohomological techniques 10 General techniques 11 Double ergodicity 12 Hochschild-Serre spectral sequence Chapter V Towards applications 13 Interpretations of $(^2 /rm EH)rm cb)$ 14 General irreducible lattices Bibliography Index

Abe, Y., University of Tonanama, Japan
Kopfermann, K., University of Hannover, Germany

Toroidal Groups
Line Bundles, Cohomology and Quasi-Abelian Varieties

2001. VIII, 133 pp. Softcover
3-540-41989-6

Toroidal groups are the connecting link between torus groups and any complex Lie groups. Many properties of complex Lie groups such as the pseudoconvexity and cohomology are determined by their maximal toroidal subgroups. Quasi-Abelian varieties are meromorphically separable toroidal groups. They are the natural generalisation of the Abelian varieties. Nevertheless, their behavior can be completely different as the wild groups show.

Keywords: Toroidal groups, theta factors, quasi-Abelian varieties, automorphic foms, pseudoconvexity MSC 2000 : 22E10, 22E99

Contents: The concept of toroidal groups: Irrationality and toroidal coordinates; Toroidal subgroups and pseudoconvexity. Line bundles and cohomology: Line bundles on toroidal groups; Comohology of toroidal groups. Quasi-Abelian Varieties: Ample Riemann forms; Characterisation of quasi-Abelian varieties. Reduction and extension: Automorphic forms; Extendable line bundles.

Series: Lecture Notes in Mathematics.VOL. 1759