FM 2019 Invited Speakers

Erik Poll
Erik Poll is Associate Professor at the Digital Security group at Radboud University in Nijmegen. Here he has carried out applied security research into smartcards, payment systems, security protocols and smart grids, and investigated the use of formal methods to support such security analyses, especially to analyse the software implementing the protocols involved. Earlier he worked on the verification of object-oriented programs, especially for Java and using the specification language JML.
June Andronick
June Andronick leads the Trustworthy Systems group, world-leading in verified operating systems software, known worldwide for the formal verification of the seL4 microkernel. She is a Principal Research Scientist at Data61|CSIRO, and conjoint Associate Professor at UNSW Sydney, Australia. She was recognised in 2011 by MIT’s Technology Review as one of the world’s top young innovators (TR35). She previously worked in industry for the smart-card manufacturer Gemalto in Formal Methods research.
Shriram Krishnamurthi
Shriram Krishnamurthi is a Professor of Computer Science and an Associate Director of the Executive Master in Cybersecurity at Brown University. With collaborators and students, he has created several influential systems and written multiple widely-used books. He also co-directs the Bootstrap math-and-computing outreach program. For his work he has received SIGPLAN’s Robin Milner Young Researcher Award, SIGSOFT’s Influential Educator Award, SIGPLAN’s Software Award, and Brown’s Henry Merritt Wriston Fellowship for distinguished contribution to undergraduate education. He has authored over a dozen papers recognized for honors by program committees. He has an honorary doctorate from the Università della Svizzera Italiana.


DS 2019 Invited Speaker

Sung-Shik Jongmans
Sung-Shik Jongmans is assistant professor at Open University of the Netherlands and researcher in the Formal Methods group at Centrum Wiskunde & Informatica (CWI), Amsterdam. He has a PhD degree from Leiden University (2016) and was visiting researcher at Imperial College London (2017-2019). His research interests include concurrency and programming languages; at the intersection of theory and practice, he currently works on design and implementation of DSL techniques for code generation, optimization, and verification of synchronization and communication protocols.


iD 2019 Invited Speakers

Constance Heitmeyer
Constance Heitmeyer heads the Software Engineering Section of NRL’s Center for High Assurance Computer Systems. Her research focuses on techniques for modeling and analyzing critical software systems and on methods for assuring the safety and security of these systems. Chief designer of NRL’s Requirements Toolset, she has published 150+ papers on a wide range of software-related research topics and is a frequent invited speaker at conferences and universities. She has transferred the results of her research to many practical, safety-critical systems, including NASA’s International Space System and a Navy weapons system. Recently, she led the team that provided formal evidence, including a formal model, a set of security properties, mechanized proof that the model satisfies the properties, and a demonstration that the source code satisfies the model, for certifying the security of a software-based communications system. Currently, she leads the formal methods V&V team whose objective is to provide assurance that a space robot performs its autonomous operations safely and correctly.
Michael Leuschel
Michael Leuschel is full professor at the Institut für Informatik of Heinrich-Heine-Universität Düsseldorf, Germany, where he leads the Software Engineering and Programming Languages group. His research focusses on model-based problem solving using symbolic model checking. He has been one of the main developers of ProB, a successful animator, constraint solver and model checker for the B-Method. ProB is certified T2 SIL4 according to the Cenelec EN 50128 standard. Michael’s research is also behind the development of the ECCE system for partial deduction.


LOPSTR 2019 Invited Speakers

Germán Vidal
German Vidal is a Professor of Computer Science at the Universitat Politecnica de Valencia, Spain. He leads a research group on Multi-paradigm Software Technology at the Valencian Research Institute for Artificial Intelligence (VRAIN). His research has mainly considered declarative programming languages and formalisms (e.g., term rewriting, functional and logic programming, the actor model) and research topics related to program semantics, integrated functional-logic languages, partial evaluation, software testing, program analysis, etc. Currently, his work mainly focuses on reversible computation and its application to program debugging in message-passing concurrent languages.
John Gallagher
John Gallagher received a Ph.D. in Computer Science from Trinity College Dublin, Ireland in 1983. After employment in research and development in a software company in Hamburg, Germany, and post-doc appointments at the Weizmann Institute of Science, Israel and Katholieke Universiteit Leuven, Belgium, he was employed at the University of Bristol, UK from 1990 to 2002. Since 2002 he has been a professor at the Roskilde University, Denmark and since 2008 he has also been a part-time research professor at IMDEA Software Institute, Madrid, Spain. His research interests focus on program transformation and generation, program analysis, constraint logic programming, rewrite systems, temporal logics, semantics-based emulation of languages and systems, and verification using abstraction.


MPC 2019 Invited Speakers

Annabelle McIver
Annabelle McIver is a Professor of Computer Science at Macquarie University in Sydney. Annabelle trained as a mathematician at Cambridge and Oxford Universities. Her research uses mathematics to prove quantitative properties of programs, and more recently to provide foundations for quantitative information flow for analysing security properties. She is co-author of the book Abstraction, Refinement and Proof for Probabilistic Systems, and of the forthcoming title The Science of Quantitative Information Flow.
Assia Mahboubi
Assia Mahboubi is a permanent researcher at Inria and an endowed Professor at the Department of Mathematics of the VU Amsterdam. Her research interests are the foundations and formalization of mathematics in type theory and the automated verification of mathematical proofs. She was previously a member of the Mathematical Components team at the Inria Microsoft Research joint centre, known for a machine-checked proof of the Odd Order theorem in finite group theory. She has been one of the main contributors to this collaborative effort. Her current projects are related to the formal verification of mathematical software.


PPDP 2019 Invited Speakers

Amal Ahmed
Amal Ahmed is an Associate Professor at the Khoury College of Computer Sciences at Northeastern University, where she leads the SILC group (Secure Interoperability, Languages, and Compilers). Her current research focuses on correct and secure compilation with support for safe inter-language linking of compiled code. Her group’s recent work also involves dependent-type-preserving compilation, new foundations for gradual typing, and formalizing the Rust type system. She is known for her work scaling the logical relations proof method, including “semantic” type soundness, to realistic languages. She received a PhD from Princeton, an MS from Stanford, and an AB from Brown, all in CS. Her awards include an NSF Career Award and a Google Faculty Research Award.
Naoki Kobayashi
Naoki Kobayashi is a professor at Department of Computer Science, Graduate School of Information Science and Technology, The University of Tokyo. He received his PhD from the University of Tokyo in 1996. His current major research interests are in principles of programming languages, especially type systems, higher-order model checking, and automated program verification.


RV 2019 Invited Speakers

Akshay Rajhans
Dr. Akshay Rajhans is a Principal Research Scientist at MathWorks. His work and research interests lie in multi-formalism model-based design of cyber-physical systems. He organizes the MathWorks Research Summits and other external research conferences, and has been an invited speaker and a panelist at various research gatherings for over a decade. Earlier, he worked on electronic control for diesel engine applications at Cummins and on non-intrusive load monitoring at Bosch Research. He has a Ph.D. from Carnegie Mellon University and an M.S. from University of Pennsylvania. (Akshay Rajhans is kindly sponsored by Runtime Verification Inc.)
David Basin
David Basin is professor of Computer Science at ETH Zurich and department head. He received his Ph.D. in Computer Science from Cornell University in 1989 and his Habilitation from the University of Saarbrucken in 1996. From 1997–2002 he held the chair of Software Engineering at the University of Freiburg. He is the founding director of the Zurich Information Security Center, which he led from 2003-2011. He is Editor-in-Chief of the ACM Transactions on Privacy and Security and an ACM fellow. (David Basin is kindly sponsored by Runtime Verification Inc.)
Sanjit A. Seshia
Sanjit A. Seshia is a Professor in the Dept. of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in CS from Carnegie Mellon University, and a B.Tech. in CS and Eng. from the Indian Institute of Technology, Bombay. His research interests are in formal methods for dependable and secure computing, with a current focus on the areas of cyber-physical systems, computer security, and robotics. He has made pioneering contributions to the areas of satisfiability modulo theories (SMT), SMT-based verification, and inductive program synthesis. He is co-author of a widely-used textbook on embedded, cyber-physical systems and has led the development of technologies for cyber-physical systems education based on formal methods. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, and the Frederick Emmons Terman Award for contributions to electrical engineering and computer science education. He is a Fellow of the IEEE. (Sanjit A. Seshia is kindly sponsored by Runtime Verification Inc.)


TAP 2019 Invited Speakers

Ana Cavalcanti
Ana Cavalcanti is Professor of Software Verification at York and Royal Academy of Engineering Chair in Emerging Technologies working on Software Engineering for Robotics: modelling, validation, simulation, and testing. She held a Royal Society-Wolfson Research Merit Award and a Royal Society Industry Fellowship to work with QinetiQ in avionics. She has chaired the PC of various well-established international conferences, is on the editorial board of four international journals, and is Chair of the board of the FME Association. She is, and has been, PI on several large research grants. Her current research is on theory and practice of verification and testing for robotics.
Heike Wehrheim
Heike Wehrheim is a full professor of Computer Science at Paderborn University, Germany. Before, she worked as a post-doc at the University of Oldenburg, obtained her PhD from Hildesheim University and studied at the University of Bonn. Her research interest are formal methods and software verification, in particular recently the combination of different verification techniques.


UTP 2019 Invited Speakers

C.A.R. Hoare
Tony Hoare’s highest official academic qualification is an MA in Classical Greats at Oxford (1952-1956). He earned professional qualifications as an Interpreter of Russian (1956-8) and as a Statistician (1958-9). He exercised his Russian as an intern at Moscow State University (1959-60), and on many subsequent visits to the Soviet Union (or Russia) and to Armenia. His first job was in the UK Computer Industry at a small computer manufacturer, where he held posts as Programmer, Chief Engineer, and Researcher (1960-68). He then applied for the Chair of Computing Science at the Queen’s University, Belfast, and to his surprise he was appointed (1968-77). He left Belfast with regret, to return to Oxford University as Professor of Computation back at Oxford (1977-99). His first retirement job was in Cambridge with Microsoft Research (1999-2017) where he stimulated an international Grand Challenge Initiative in Verified Software. Since his second retirement, he has been an unpaid Visitor at Microsoft Research and an Honorary Member of the Cambridge University Computing Laboratory.
He Jifeng
From 1965 to 1985, He Jifeng was an instructor at East China Normal University. During 1980–81, he was a visiting scholar at Stanford University and the University of San Francisco in California, USA. From 1984 to 1998, He Jifeng was a Senior Research Fellow at Oxford PRG. In particular, he worked with Prof. Sir Tony Hoare, latterly on Unifying Theories of Programming, resulting in a book of that name. Since 1986, He Jifeng has been Professor of Computer Science at East China Normal University in Shanghai. In 1996, he also became Professor of Computer Science at Shanghai Jiao Tong University. In 1998, he became a Senior Research Fellow at UNU-IIST, United Nations University, based in Macau. He moved back to Shanghai in 2005. He Jifeng’s research interests include sound methods for the specification of computer systems, communications, application and standards, and techniques for designing and implementing those specifications in software and/or hardware with high reliability. In 2005, he was elected to the Chinese Academy of Sciences. In 2013, his 70th birthday was celebrated at East China Normal University with an international three-day Festschrift in association with ICTAC.


VECoS 2019 Invited Speakers

Ahmed Bouajjani
Ahmed Bouajjani got his PhD and Habilitation in CS from U.Grenoble (1990, 1999). He is Professor at Paris Diderot University since 1999 and head of the “Automata, Structures, and Verification” of the IRIF lab. He is senior member of the “Inst. Univ. de France” since 2013. He has been visiting professor at TU Munich, U. Uppsala, Microsoft Research, etc. His main research interests are formal methods, program verification, concurrency, infinite-state model-checking algorithms, automata and logics. He got a “Humboldt Research Award” in 2018.
Ali Mili
Ali Mili holds a PhD in CS from the University of Illinois and a Doctorat es-Sciences d’Etat from the University of Grenoble. He served as chairperson of the Computer Science Department at the University of Tunis and currently serves as Professor and Associate Dean in the Ying Wu College of Computing at NJIT, Newark, NJ.


DALI 2019 Invited Speaker

Dexter Kozen
Dexter Kozen is the Joseph Newton Pew, Jr. Professor in Engineering, at Cornell University. One of the fathers of dynamic logic and the Mu-calculus, he is also credited for a number of major contributions in logic, theory of computation, automata theory and computational complexity. Along is career Dexter received several awards, including an Outstanding Innovation Award from IBM Corporation and the honor of a professorship at The Radboud Excellence Initiative, Radboud University Nijmegen in the Netherlands.


DataMod 2019 Invited Speakers

Ana Cavalcanti
Ana Cavalcanti is Professor of Software Verification at York and Royal Academy of Engineering Chair in Emerging Technologies working on Software Engineering for Robotics: modelling, validation, simulation, and testing. She held a Royal Society-Wolfson Research Merit Award and a Royal Society Industry Fellowship to work with QinetiQ in avionics. She has chaired the PC of various well-established international conferences, is on the editorial board of four international journals, and is Chair of the board of the FME Association. She is, and has been, PI on several large research grants. Her current research is on theory and practice of verification and testing for robotics.
Mieke Massink
Mieke Massink received her master’s degree in CS from the University of Nijmegen (NL), in 1988; she received her Laurea in CS from the University of Pisa in 1995 and her PhD degree in CS from the U. Nijmegen in 1996. In 1992 she received the “Dr. I.B.M. Frye Stipend” of the U. Nijmegen for the most promising female PhD researcher. She is currently a researcher in the Formal Methods and Tools lab at CNR-ISTI A. Faedo, Italy. Prior to this she held positions at the U. Nijmegen and U. Twente, both in the Netherlands, and in the context of several European projects, the CNR-CNUCE institute, Italy, and the University of York (UK). She has been lecturing at the U. Pisa from 1996 to 1998 and from 2006 to 2009 and at the University of Florence from 2005 to 2017. She is lecturing in the Tuscan PhD program in Smart Computing from 2015; in Feb. 2011 she was Visiting Professor at the MT-Lab, DTU, Copenhagen, DK. Her research interests include the development and application of formal languages for specification and verification of concurrent, safety critical and software intensive systems, including collective adaptive systems which may exhibit emergent behaviour, and HCI related aspects of such systems.


F-IDE 2019 Invited Speaker

Wolfgang Ahrendt
Wolfgang Ahrendt is professor at Chalmers University of Technology in Gothenburg, Sweden. He obtained his Ph.D. in Computer Science at the University of Karlsruhe in 2001. His work focuses on topics related to deductive software verification. He is one of the people behind the source code level verification approach and tool called KeY, and co-published the recent ‘KeY book’. Among others, he also worked on compositional verification of distributed objects, on combining static and runtime verification, and lately on smart contract verification. He is PC co-chair of the iFM conference, December 2019.


FMAS 2019 Invited Speaker

Claudio Menghi
Claudio Menghi received his BSc and MSc degrees in computer science from the Politecnico di Milano where he later obtained his Ph.D. degree in 2015. From 2017 to 2018, he was a Postdoctoral researcher at the University of Gothenburg and Chalmers. He is now a Research Associate at the University of Luxembourg. His research interests are in the field of formal methods and software engineering, with specific interests in cyber-physical systems, robotics, and formal verification.


FMBC 2019 Invited Speaker

Ilya Sergey
Ilya Sergey is a tenure-track Associate Professor at Yale-NUS College (Singapore), holding a joint appointment with NUS School of Computing. From 2015 to 2018 he was with the CS Dept. of UCL. Prior to joining UCL he was a postdoc at IMDEA Software Institute (2012-2015). From 2008 to 2012 he was RA at the CS Dept. of KU Leuven, where he obtained his PhD. During his doctoral studies he was a visiting PhD fellow at the CS Dept. of Aarhus University and a research intern at the PPT group at MSR Cambridge. He got a MSc degree in Mathematics and CS in 2008 from Dept. of Mathematics and Mechanics of St. Petersburg State University. Before joining academia he worked as a software developer at JetBrains.


FMTea 2019 Invited Speaker

Carroll Morgan
Carroll Morgan was at the University of Oxford in the 1980-90’s; since 2000 he has been at the University of New South Wales and in the Trustworthy Systems Group of CSIRO’s Data61 in Sydney. He is the author of Programming from Specifications (Prentice-Hall 1990,4,8), of Abstraction, Refinement and Proof for Probabilistic Systems (Springer 2005, with Annabelle McIver), and of The Science of Quantitative Information Flow (Springer 2019 to appear, one of six authors). His current interest is refinement-based techniques for security-respecting program development, with a particular emphasis on source-level reasoning.


HFM 2019 Invited Speaker

Mark Priestley
After a career as a programmer and lecturer in software engineering, Mark Priestley is now an independent scholar of the history and philosophy of computing with a particular interest in the early history of programming. His publications include the books A Science of Operations and ENIAC in Action (coauthored with Thomas Haigh and Crispin Rope). His most recent book, Routines of Substitution (Springer, 2018), is a study of John von Neumann’s work in software development in the mid-1940s. Read more at


OVT 2019 Invited Speaker

Ana Paiva
Ana Paiva is Assistant Professor with Habilitation in the Dept. of Informatics Engineering of the Faculty of Engineering of the University of Porto (FEUP). Also a researcher at INESC TEC in the area of Software Engineering, she obtained her PhD (2007) with her thesis Automated Testing of Graphical User Interface Specification, in the context of which she visited Microsoft Research and gave talks on automated GUI testing with Spec Explorer. Ana has researched and published in the area of implementing and automating model-based testing. She is a member of PSTQB (Software Testing Qualification Board) and also a member of several ISTQB (International Software Testing Qualification Board) working groups.


OpenCERT 2019 Invited Speaker

Andreas Meiszner
Dr Andreas Meiszner is a seasoned portfolio worker who worked across a number of sectors and functions. In two of his most recent portfolios he has tutored, mentored and coached beyond 500 professional doctoral students (mid to seniors, aged 35 to 70), first with the University of Liverpool (UK), and since 2016 also with the DoctorateHub. 500+ students imply 500+ workplace-based problems from 500+ organizations from across the globe. This allowed Andreas to understand how to tackle problems at scale, be it the tame, the complex, or the wicked.


REFINE 2019 Invited Speaker

Régine Laleau
Régine Laleau is professor at Université Paris-Est Créteil (UPEC) and member of the team Specification and Verification of Systems of the LACL (Laboratory of Algorithmic, Complexity and Logic) laboratory. She was head of the LACL from June 2008 to December 2016. She is also associate professor at Université de Sherbrooke (Québec). Her research is in the field of formal methods, software engineering and information systems. It includes the coupling of formal methods and semi-formal ones, combination of formal methods for the specification of systems and requirements engineering.


RPLA 2019 Invited Speaker

Robert Glück
Robert Glück is a Professor of Computer Science at the University of Copenhagen. His main research interests are programming languages and software systems. His current research focus is on reversible computing, program generation, and metaprogramming. He has chaired and edited the proceedings of several conferences and workshops in North America, Europe and Asia. Robert Glück has been the principle investigator of a number of research awards and projects. (Robert Glück is kindly sponsored by CMUP/FCT.)