Invited speakers

Chin Wei Ngan Laurent Fribourg
Chin Wei Ngan Laurent Fribourg
School of Computing National University of Singapore, Singapore LSV, CNRS & ENS de Cachan, France

Chin Wei Ngan

School of Computing, National University of Singapore, Singapore

Title: "Specification, Verification and Inference"

Abstract
Traditionally, the focus of specification mechanism has been on improving its ability to cover a wider range of problems more accurately, while the effectiveness of verification is left to the underlying theorem provers. Our work attempts a novel approach, where the focus is on designing good specification mechanisms that can achieve both better expressiveness and better verifiability. Moreover, we shall also highlight a unified specification mechanism that can be used for both verification and inference. Our framework allows preconditions and postconditions to be selectively inferred via a set of uninterpreted relations which are computed using bi-abduction, and modularly synthesized to support concise specification for program codes.

Bio
Wei-Ngan Chin is presently an Associate Professor in the Department of Computer Science, National University of Singapore. His research interests are in programming languages and software engineering. He has worked on various program analyses and verification techniques that are aimed at improving clarity, reliability and reusability of software.

His current research is supported by an MOE project on "Specification and Verification for Future Programmers".

Laurent Fribourg

LSV, CNRS & ENS de Cachan, France

Title: "Control of Switching Systems by Invariance Analysis" (Joint work with Romain Soulat)

Abstract
Switched systems are embedded devices widespread in industrial applications such as power electronics and automotive control. They consist of continuous-time dynamical subsystems and a rule that controls the switching between them. Under a suitable control rule, the system can improve its steady-state performance and meet essential properties such as safety and stability in desirable operating zones. We explain that such controller synthesis problems are related to the construction of appropriate invariants of the state space, which approximate the limit sets of the system trajectories. We present a new approach of invariant construction based on a technique of state space decomposition interleaved with forward fixed point computation. The method is illustrated in a case study taken from the field of power electronics.

Bio
Laurent Fribourg is a CNRS Senior Researcher working at École Normale Supérieure de Cachan (ENSC), France. Since 2007, he has been Scientific Coordinator of Institut Farman, which federates interdisciplinary projects between 5 Laboratories of ENSC. He has been Director of LSV, the Computer Science Lab. of ENSC since 2011. He has written more than 70 international publications in the field of Logic Programming, Program Testing, and Model Checking.