Irina Mariuca Asavoae & Markus Roggenbach – Software Model Checking for Mobile Security – Collusion Detection in K
Abstract: Cyber-security witnesses an ongoing expansion in various fields of research. This is due to the booming of cyber-physical systems and the necessity of evaluating and certifying their
Irina Mariuca Asavoae is a guest researcher at Swansea University where, in 2015, she started working on Android security in the ACID project. She received her PhD in 2012 from A.I. Cuza University in Romania for the thesis “K Semantics for Abstractions”–part of a project in collaboration with Grigore Rosu’s group in University of Illinois Urbana-Champaign. Her work evolves from formal methods in programming languages, with emphasis on model checking and abstract interpretation, to applying these techniques in cybersecurity. As such, her current projects are: Android security, timing evaluation of embedded systems, and synthesis of program analyzers from formal language semantics.
Klaus Havelund & Doron Peled – Efficient Runtime Verification of First-Order Temporal Properties
Radu Iosif – Program Verification with Separation Logic
Abstract: In this talk Radu Iosif will introduce Separation Logic as a framework for the development of modular program analyses for sequential, inter-procedural and concurrent programs. Because program verification eventually boils down to deciding logical queries such as the validity of verification conditions, the core of the talk is dedicated to a survey of decision procedures for Separation Logic, that stem from either SMT, proof theory or automata theory. Incidentally I will address issues related to decidability and computational complexity of such problems, in order to expose certain sources of intractability.
Radu Iosif is a full-time researcher in the French National Research Center (CNRS) at the Verimag laboratory, since 2002. Previously, he obtained a PhD in Computer Science from Politecnico di Torino, Italy, and spent time as a Research Associate at Kansas State University, USA. His main interests are in program verification, mainly in applications of logic and automata theory to finding scalable techniques that can cope with real-life software systems.