The 79th Business Meeting of FME will take place in Milan (Italy), September 12, 2024.
FormaliSE 2024 took place on 14-15 April 2024, in Lisbon, Portugal, as a co-hosted conference of the International Conference on Software Engineering (ICSE2024). Carlo A. Furia (Università della Svizzera italiana, Switzerland) and Antónia Lopes (University of Lisbon, Portugal) were this year’s PC Co-chairs. 41 papers were submitted, which is amongst the highest level in recent years, of which 14 were accepted (11 full research papers, 1 case study and 2 research ideas).
MIT Press, 2023, 496 pp, ISBN: 978-0-262546-23-2. https://mitpress.mit.edu/9780262546232/program-proofs/
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.
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.
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.