2nd edition. — The MIT Press, 2018. — 424 p. — ISBN 9780262038836. An expanded and updated edition of a comprehensive presentation of the theory and practice of model checking, a technology that automates the analysis of complex systems. Model checking is a verification technology that provides an algorithmic means of determining whether an abstract model—representing, for...
MIT Press, 2013. — 440 p. — ISBN13: 978-0262026659. The technology of mechanized program verification can play a supporting role in many kinds of research projects in computer science, and related tools for formal proof-checking are seeing increasing adoption in mathematics and engineering. This book provides an introduction to the Coq software for writing and checking...
Springer, 2024. — 708 p. — (Computer Science Foundations and Applied Logic). — ISBN 978-3-031-55607-4. Frama-C is a popular open-source toolset for analysis and verification of C programs, largely used for teaching, experimental research, and industrial applications. With the growing complexity and ubiquity of modern software, there is increasing interest in code analysis tools...
Комментарии