Program logics for certified compilers. (English) Zbl 1298.68009
Cambridge: Cambridge University Press (ISBN 978-1-107-04801-0/hbk; 978-1-107-25655-2/ebook). x, 458 p. (2014).
Formal verification has the potential to radically change the landscape of software engineering. Will it become integrated into the software engineering process, or will it remain a fringe science? The adoption of the techniques presented in this book is likely to influence the answer to this question. This book describes, in full detail, the cutting edge of software verification, viz., the complete verification of a compiler for almost all of C90. It is not an easy or casual read, but still a profitable investment for the serious student of computer science.
Reviewer: Johan Georg Granström (Zürich)
MSC:
68-02 | Research exposition (monographs, survey articles) pertaining to computer science |
68N20 | Theory of compilers and interpreters |
68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
68Q60 | Specification and verification (program logics, model checking, etc.) |