The 70th Business Meeting of FME will take place December 10, 2020.
| About FME | Formal Methods | Events | FME Awards |
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.
now Publishers Inc., 2018, 296 pages, ISBN 978-1-68083-402-4
https://www.nowpublishers.com/article/Details/EDA-053
While a number of theoretical contract frameworks have been proposed in the literature, missing has been a formal statement of what is required in defining a contract theory. This book addresses that gap, presenting a thorough mathematical treatment of contracts with the development of a new meta-theory for contracts as the foundation. That meta-theory is used to provide an understanding of several contract frameworks, allowing the reader to see how each framework fits into the meta-theory and to assess similarities and differences between the individual frameworks.
MIT Press, 2014, ISBN 978-0-262-02771-7,
https://mitpress.mit.edu/books/modeling-and-analysis-communicating-systems
The book Modeling and Analysis of Communicating Systems by Jan Friso Groote and Mohammad Reza Mousavi introduces the foundations for modeling concurrent systems as transition systems, the key notions of equivalence and of bi-simulation between transition systems, and their use in the specification and verification system mCRL2. Though rooted in the mCRL2 technique, the book presents general principles that should be of interest not only for readers who want to learn about mCRL2, but also for readers interested in general in modeling and verification of complex systems.
FormaliSE 2020 was organised as a 1-day virtual conference co-located with ICSE on July 13, 2020. The main objective of FormaliSE is to foster the integration between the formal methods and the software engineering communities, to strengthen the – still too weak – links between them, and to stimulate researchers to share ideas, techniques, and results, with the ultimate goal to propose novel solutions to the fraught problem of improving the quality of software systems. We here bring you a keynote from Formalise 2020, given by Corina Pasareanu: On the Probabilistic Analysis of Neural Networks.
FormaliSE 2020 was organised as a 1-day virtual conference co-located with ICSE on July 13, 2020. The main objective of FormaliSE is to foster the integration between the formal methods and the software engineering communities, to strengthen the – still too weak – links between them, and to stimulate researchers to share ideas, techniques, and results, with the ultimate goal to propose novel solutions to the fraught problem of improving the quality of software systems. We here bring you a keynote from Formalise 2020, given by Shahar Maoz: SYNTECH: Synthesis Technologies for Reactive Systems Software Engineers