Springer, 2018, 133 pages, ISBN 978-3-319-67106-2
https://www.springer.com/gp/book/9783319671062
Exams are an important aspect in assessing people’s skills and as such play a key role to establish meritocracy in modern societies. To be effective, however, exams need to be fair and secure against tampering, which is where Rosario Giustolisi’s book “Modelling and Verification of Secure Exams’’ [5] comes to the rescue. Over 133 pages, the book describes the different aspects of exams in detail and identifies various security-related requirements for them. Moreover, the book describes how to formally model an exam using the applied pi-calculus and how to verify security requirements for it using the ProVerif verifier. Finally, the book presents the outcome of modelling and analysing three popular example protocols. This book might be of interest to everyone who wants to learn more about the nature of exams in general, and in particular about how to model and verify them. To fully appreciate the book, however, some familiarity with the applied pi-calculus and in particular the ProVerif verifier is necessary.
FME’s Teaching Committee is launching a new tutorial series, planned to be held monthly. We aim to increase the awareness and sharing of tools and techniques used for teaching formal methods. The tutorial will be held online via zoom.
CAVlinks is a platform for students and researchers interested in computer-aided verification. The website aims to be an entry point for new students by presenting links to introductory and advanced study material in the areas relevant to CAV (e.g. logics, theoretical CS, and formal methods), by pointing to interesting events (e.g. workshops, student forums, conferences maintained in a public calendar), and by advertising mentoring possibilities.
Springer, 2010, 426 pages, ISBN 978-3-642-14508-7
https://link.springer.com/book/10.1007%2F978-3-642-14509-4
This is an extensive book on deductive methods for hybrid systems’ verification, rooted in dynamic logic. The author develops both formal specification languages for hybrid systems and automated verification techniques based on them. The main focus is on the theoretical aspects of the approach, but implementation issues are also widely addressed, and a functioning tool is presented at the end of the book. It presents a powerful formalism for the specification and verification of hybrid systems, with a strong practical impact.
Two new survey papers offer complementary perspectives on the state of formal methods in 2020.
The nominations should be sent to info@fmeurope.org by 31st JANUARY 2021.
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.