ACM, 2016, 283 pp, ISBN: 978-1-970001-27-3. https://dl.acm.org/doi/book/10.1145/2841316.
This book is a practical introduction to the dependently-typed functional programming language Agda. The main focus of the book is verified programming, where properties are expressed through a very expressive type system, based on dependent types. In this setting, code that type-checks is also an actual proof of the stated property.
The book Principles of Cyber-Physical Systems by Rajeev Alur introduces the principles of design, specification, modeling and analysis of cyber-physical systems with compositional modeling at its heart. This textbook – written with incredible care and attention to pedagogical detail – covers all the relevant fundamental notions. A host of carefully designed exercises should allow it to be used both as course material and for self-study.
Freely downloadable: https://functional-algorithms-verified.org/
The book Functional Algorithms, Verified! presents a number of classical functional data structures, accompanying each of them with formal specifications. These specifications describe both the functional correctness and the time complexity of every operation, emphasizing the notion of interface for an abstract data type. The book can be seen as a way to augment a course on functional data structures with an introduction to formal specifications.
Springer, 2016, 356 pages, ISBN 978-3-662-57065-4
https://www.springer.com/gp/book/9783662504963
This book, entitled Decision Procedures – An Algorithmic Point of View, successfully describes and explains algorithmic solutions to decision problems. It is well-suited for use as a textbook and as a developer reference. The book precisely describes a series of algorithms used by decision procedures and also includes many worked out examples accompanied by a library that includes implementations of the algorithms.
The Annual General Meeting of FME will take place as a hybrid meeting at the iFM Conference in Lugano, Switzerland, June 9 2022.
Springer, 2019, 160 pages, ISBN 978-3-030-05155-6
https://link.springer.com/book/10.1007/978-3-030-05156-3
Teaching and convincing practitioners to adopt formal methods in system engineering is admittedly still a challenge. This book aims at generating “appetite” in undergraduate students by introducing some classical formal methods trying to rely on intuition, simple examples, and a “metaformalism” rooted in graph theory which is better known than more sophisticated mathematics at the undergraduate level. The selected areas of application of formal methods are language semantics and program verification. The exposition is generally clear although the adopted notation is sometimes mathematically heavy.