This book explores one of the most common approaches to program verification, known as the assertional approach. Case studies supplied throughout the book demonstrate the use of the proof systems and formally verify solutions to classical problems.
Value-Range Analysis of C Programs describes a static analysis for detecting buffer overflows. While the book focuses on a sound analysis of C, it will be useful to researchers and students interested in static analysis of real-world programming languages.
With a free, downloadable software package available to help solve the exercises, this book focuses on practical and relevant problems that arise in the field of binary logics, with its two main applications – digital circuit design, and propositional logics.
This book provides foundations for software specification and formal software development from the perspective of work on algebraic specification. It concentrates on developing basic concepts and studying their fundamental properties.
This book teaches readers how to better reason about software development. It teaches how to communicate reasoning, to distinguish between good and bad reasoning, and to read professional literature that presumes knowledge of elementary logic.