13h30 : Hélène Kirchner - Informal prospects in formal methods

Organized by: 
L'équipe des Keynote Speeches : Sihem Amer-Yahia, Jérôme David, Renaud Lachaize
Hélène Kirchner (INRIA)

Detailed information: 


H. Kirchner is emeritus research director at Inria. She graduated first in mathematics in Paris, then in computer science in Strasbourg and Nancy. Her research is concerned with the foundation, design and development of safe software: formal specifications, logic and automated deduction, program verification, with a special emphasis on deduction and computation by rewriting rules and strategies. Since 2005, she applies these techniques to the design and verification of security policies, and to the modeling of bio-chemical processes and social networks with graph transformations. 
She entered CNRS in 1982 after her PhD in Computer Science, did a post-doc at Stanford and SRI after her Habilitation (These d'Etat) in 1985, and later moved to Inria in 2007. She has been Director of UMR LORIA and Inria Lorraine research center (2001-2007), Deputy Scientific Director at Inria (2007-2010),  Director of European and International Partnerships of Inria (2010-2015), then Scientific Affairs Officer at Direction of European and International Partnerships of Inria (2015-2018). 
In 2012, she was selected as Grand Professor in the TU Dresden Cluster of Excellence CfAED - Center for Advancing Electronics Dresden. Since 2015, she is member of the Board of Informatics Europe and member of the Board of the French High Council for Evaluation of Research and Higher Education. She is member of the IFIP WG 1.6 (Term Rewriting), co-editor of Annals of Mathematics and Artificial Intelligence, member of the editorial board of Computing and Informatics (until 2017) and of Logical Methods in Computer Science (LMCS).


[The talk will be in English]


Formal methods, rooted  in  logic and reasoning, traditionally aim to provide guarantees that systems behave correctly, thanks to verification technologies (based on concepts of model, computation, deduction, constraint solving). They strongly contribute to ensure safety, security and accountability of software and hardware systems. These guarantees must be addressed in the context of actual and future cyber systems where  machine learning techniques and autonomous decisions are expanding. 
Prospects in formal methods will be examined and challenges will be proposed, focusing on cybersecurity issues.