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.


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.


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 Speaker

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.


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


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.