Model checking is a verification technology that provides an algorithmic means of determining whether an abstract model—representing, for example, a hardware or software design—satisfies a formal specification expressed as a temporal logic formula. If the specification is not satisfied, the method identifies a counterexample execution that shows the source of the problem. Today, many major hardware and software companies use model checking in practice, for verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms. This book offers a comprehensive presentation of the theory and practice of model checking, covering the foundations of the key algorithms in depth.
The field of model checking has grown dramatically since the publication of the first edition in 1999, and this second edition reflects the advances in the field. Reorganized, expanded, and updated, the new edition retains the focus on the foundations of temporal logic model while offering new chapters that cover topics that did not exist in 1999: propositional satisfiability, SAT-based model checking, counterexample-guided abstraction refinement, and software model checking. The book serves as an introduction to the field suitable for classroom use and as an essential guide for researchers.
Model checking is a verification technology that provides an algorithmic means of determining whether an abstract model—representing, for example, a hardware or software design—satisfies a formal specification expressed as a temporal logic formula. If the specification is not satisfied, the method identifies a counterexample execution that shows the source of the problem. Today, many major hardware and software companies use model checking in practice, for verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms. This book offers a comprehensive presentation of the theory and practice of model checking, covering the foundations of the key algorithms in depth.
The field of model checking has grown dramatically since the publication of the first edition in 1999, and this second edition reflects the advances in the field. Reorganized, expanded, and updated, the new edition retains the focus on the foundations of temporal logic model while offering new chapters that cover topics that did not exist in 1999: propositional satisfiability, SAT-based model checking, counterexample-guided abstraction refinement, and software model checking. The book serves as an introduction to the field suitable for classroom use and as an essential guide for researchers.
For National Depression Education and Awareness Month in October, we are sharing a collection of titles that educates and informs on depression, including personal stories from those who have experienced depression and topics that range from causes and symptoms of depression to how to develop coping mechanisms to battle depression.
In celebration of the Halloween season, we are sharing horror books that are aligned with the themes of the holiday: the sometimes unknown and scary creatures and witches. From classic ghost stories and popular novels that are celebrated today, in literature courses and beyond, to contemporary stories about the monsters that hide in the dark, our list
For LGBTQIA+ History Month in October, we’re celebrating the shared history of individuals within the community and the importance of the activists who have fought for their rights and the rights of others. We acknowledge the varying and diverse experiences within the LGBTQIA+ community that have shaped history and have led the way for those
Penguin Random House Education is proud to celebrate Hispanic & Latine Heritage Month, which runs annually from September 15th through October 15th. We are highlighting the works of our authors from the Hispanic and Latine community. Find a full collection of titles here.
/
