Synthesizing (Differential) Invariants by Reduction Non-convex Programming to SDP

-----------------------------------------------------------------------
         Distinguished Seminar
-----------------------------------------------------------------------
Speaker: Professor Naijun ZHAN
         Distinguished Research Professor
         Institute of Software Chinese Academy of Sciences (ISCAS)

Title:  "Synthesizing (Differential) Invariants by Reduction Non-convex
         Programming to SDP"

Date:   Monday, 9 October 2023

Time:   4:00pm - 5:00pm

Venue:  Lecture Theater F
        (Leung Yat Sing Lecture Theater)
        near lift 25/26, HKUST


Abstract:

Invariant Generation plays a central role in the verification of programs
and hybrid systems. As the constraint solving techniques advance rapidly
in recent years, particularly optimization-based constraint solving,
optimization based invariant generation becomes more and more promising
and has been successfully applied to verification of programs and hybrid
systems. However, how to deal with non-convex programming derived from
invariant generation is still challenging. In this talk, I report our
recent work on efficient invariant generation by reduction of non-convex
programming to SDP.


********************
Biography:

Naijun Zhan is a distinguished research professor of Institute of
Software Chinese Academy of Sciences (ISCAS), the acting director of the
State Key Lab. of Computer Science. He got his bachelor degree and
master degree both from Nanjing University, and his PhD from ISCAS. Prior
to joining ISCAS, he worked at the Faculty of Mathematics and Informatics,
Mannheim University, Germany as a research fellow. His research interests
cover formal design of real-time, embedded and hybrid systems,
program verification, and so on. He is on the editorial boards of Journal
of Automated Reasoning, Formal Aspects of Computing, Journal of Logical
and Algebraic Methods in Programming, Research Director: Cyber Physical
System, Journal of Software, etc.,a member of the steering committees of
SETTA and MEMOCODE, the pc co-chairs of FM 2021, SETTA 2016, the general
co-chairs of MEMOCODE 2018, MEMOCODE2019 and ICESS 2019, and serves more
than 100 international conferences program committees e.g., CAV, RTSS,
HSCC, TACAS, FM, ICCPS, EMSOFT and so on. He published more than 100
papers in international leading journals and conferences, 2 books and 4
book chapters, and edited 4 conference proceedings and 5 journal
special issues. See lcs.ios.ac.cn/~znj [lcs.ios.ac.cn] for more details.