77th FME Meeting, 1st February 2024

The 77th Business Meeting of FME will take place in London (UK), February 1, 2024.

Read more

Share

Book Review: Program Proofs

K. Rustan M. Leino: Program Proofs

MIT Press, 2023, 496 pp, ISBN: 978-0-262546-23-2. https://mitpress.mit.edu/9780262546232/program-proofs/

Summary

The book Program Proofs by Rustan Leino teaches students how to write specifications for functional, imperative, and object-oriented program code and how to prove them correct. The book uses the language and proof tool Dafny. It comes with online code examples and, as teacher’s material, answers to the exercises.

Read more

Share

Call for Nominations: FME Fellowship Award 2024

FME Fellowship Award

FME is currently accepting nominations from FME members for the 2024 fellowship, which will be presented during FM 2024 (9th-13th September 2024). The nominations should be sent to info@fmeurope.org by 5th JANUARY 2024.

Established in 2015 and normally given every three years for technical achievements in advancing, applying, and promoting formal methods, the Formal Methods Europe (FME) Fellowship rewards scientific breakthroughs and pioneering work that have made a difference to the world through advances in formal methods.

Nominees are expected to have made significant contributions through solid theoretical work or practical impact in industry. The development of frameworks and tools, teaching formal methods, as well as publicising formal methods worldwide and attracting people to the community are additional criteria that can strengthen a nomination. All nominations have to be supported by concrete evidence.

Read more

Share

Book Review: Verified Functional Programming in Agda

Aaron Stump: Verified Functional Programming in Agda

ACM, 2016, 283 pp, ISBN: 978-1-970001-27-3. https://dl.acm.org/doi/book/10.1145/2841316.

Summary

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.

Read more

Share

FME Annual General Meeting 2023

The Annual General Meeting of FME will take place online, June 15, 2023.

Read more

Share

Book Review: Principles of Cyber-Physical Systems

Rajeev Alur: Principles of Cyber-Physical Systems

Summary

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.

Read more

Share

Book Review: Functional Algorithms, Verified!

Tobias Nipkow, Jasmin Blanchette, Manuel Eberl, Alejandro Gómez-Londoño, Peter Lammich, Christian Sternagel, Simon Wimmer, and Bohua Zhan: Functional Algorithms, Verified!

Freely downloadable: https://functional-algorithms-verified.org/

Summary

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.

Read more

Share

74th FME Meeting, 12 December 2022

The 74th Business Meeting of FME will take place December 12, 2022.

Read more

Share

CfP FormaliSE 2023

Call for Papers
FORMALISE 2023

11th International Conference on Formal Methods in Software Engineering
co-located with ICSE 2023

14-15 May 2023, Melbourne, Australia
http://www.formalise.org

Read more

Share

Book review: Decision Procedures – An Algorithmic Point of View

Daniel Kroening and Ofer Strichman: Decision Procedures – An Algorithmic Point of View

Springer, 2016, 356 pages, ISBN 978-3-662-57065-4
https://www.springer.com/gp/book/9783662504963

Summary

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.

Read more

Share