Fundamental algorithms, set theory, logic, and discrete mathematics are essential for computing students aiming for success. This textbook provides clear and precise explanations of key algorithms while offering necessary background material for deeper understanding. The author emphasizes that clarity comes from proper use of formalism, ensuring students grasp complex concepts effectively. The book serves as a foundational resource for programming students, equipping them with the tools needed to analyze algorithm correctness and complexity.
This book covers a range of topics in embedded systems design and formal verification. It includes discussions on interactive verification techniques, such as machine-checked proofs for electronic payment systems and the validation of medical guidelines. The text explores the certification of airport security regulations and the safety properties of aircraft landing protocols using theorem proving. It also addresses the validation of hypervisors and formal modeling of systems, including properties of behavioral model merging and the automatic translation of Circus to Java.
The book delves into real-time systems, focusing on the modeling and validation of distributed embedded systems and modularized verification approaches. It shares industrial experiences in adopting formal methods, including case studies from railway signaling manufacturers and object-oriented development.
Additionally, the text discusses specification refinement, programming languages, and formal reasoning about Java methods. It presents concepts like dynamic frames, type-safe data transformation, and feature algebra. The educational aspect emphasizes using domain-independent problems to introduce formal methods and formal modeling of communication protocols.
Lastly, it covers model checking techniques, including strategies for symmetry reduction and monitoring distributed controllers, alongside insights into formal methods for security and their applicat
In this book, a programming model is developed that addresses the fundamental issues of 'large-scale programming'. The approach unifies several concepts from database theory, object-oriented programming and designs of reactive systems. The model and the associated theory has been christened "Seuss." The major goal of Seuss is to simplify multiprogramming. To this end, the concern of concurrent implementation is separated from the core program design problem. A program execution is understood as a single thread of control - sequential executions of actions that are chosen according to some scheduling policy. As a consequence, it is possible to reason about the properties of a program from its single execution thread.
