Invited speakers
 |
 |
| 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.