Zohar Manna Knihy

Once the province of philosophy, logic has found increasing application in computer science, especially in software engineering and artificial intelligence. Systems with the ability to perform logical deduction are being applied to the synthesis, verification, and transformation of computer programs, to the understanding of natural language, and to the formation of commonsense and robotic plans. Expert systems and logic-programming systems (such as Prolog) may all be regarded as rudimentary applications of a new deductive technology.

This volume is dedicated to the memory of the 1996 Turing Award winner Amir Pnueli. It contains articles written by leading scientists that span the breadth of Pnueli’s scientific work, with a focus on the development and the application of formal methods.

With the objective of making into a science the art of verifying computer programs (debugging), the author addresses both practical and theoretical aspects of the process. A classic of sequential program verification, this volume has been translated into almost a dozen other languages and is much in demand among graduate and advanced undergraduate computer science students.Subjects include computability (with discussions of finite automata and Turing machines); predicate calculus (basic notions, natural deduction, and the resolution method); verification of programs (both flowchart and algol-like programs); flowchart schemas (basic notions, decision problems, formalization in predicate calculus, and translation programs); and the fixpoint theory of programs (functions and functionals, recursive programs, and verification programs). The treamtent is self-contained, and each chapter concludes with bibliographic remarks, references, and problems.

Focusing on the complexities of programming interactive computing systems, this volume provides a comprehensive introduction to temporal logic as a specification tool for reactive systems. It presents a foundational understanding of the computational model for reactive programs, developed by renowned scholars Zohar Manna and Amir Pnueli. The text serves as an essential resource for those delving into the challenges of real-time, concurrent, and control systems, making it a valuable reference for both students and professionals in the field.

Focusing on computational logic, the textbook covers foundational concepts of first-order logic and advances to modern decision procedures for arithmetic and data structures. It emphasizes a logical methodology for developing correct software, making it a valuable resource for understanding both theoretical and practical aspects of computational logic in engineering.

This book focuses on the verification of reactive systems, which continuously interact with their environment rather than compute a final value upon termination. Such systems include concurrent programs, embedded and process control programs, and operating systems, all of which present unique challenges for reliable construction. Examples include air traffic control systems, train control programs, and processes like nuclear reactors. As computers are increasingly used in safety-critical applications where failures can have severe consequences, ensuring correctness becomes essential. This necessity has led to the development of formal verification techniques that enhance user and designer confidence in meeting specifications. The approach outlined in this book utilizes temporal logic to specify the properties of reactive systems and establishes a comprehensive verification methodology for demonstrating that a system adheres to its temporal specifications. Reactive programs must be defined by their ongoing behavior, and temporal logic serves as an expressive language for this purpose. The framework for specifying and verifying the temporal properties of reactive systems comprises four components, with the chosen computational model being a Fair Transition System (FTS) to effectively describe the behavior of these systems.