报告人：Naijun Zhan, research professor, Institute of Software, Chinese Academy of Sciences
报告地点：腾讯会议ID: 180 615 282
报告摘要：Interpolation-based techniques have become popularized in recent years because of their inherently modular and local reasoning, which can scale up existing formal verification techniques like theorem proving, model-checking, abstraction interpretation, and so on, while the scalability is the bottleneck of these techniques. Craig interpolant generation plays a central role in interpolation-based techniques, and therefore has drawn increasing attentions. In the literature, there are various works done on how to automatically synthesize interpolants for decidable fragments of first-order logic, linear arithmetic, array logic, equality logic with uninterpreted functions (EUF), etc., and their combinations. But Craig interpolant generation for non-linear theory and its combination with the aforementioned theories are still in infancy, although some attempts have been done.
In this talk, we first prove that a polynomial interpolant of the form h(x)>0 exists for two mutually contradictory polynomial formulas F(x,y) and G(x,z), with the form f1>=0 /\ ... /\ fn >= 0, where fis are polynomials in x,y or x,z, and the quadratic module generated by fis is Archimedean. Moreover, we show that such interpolant can be computed efficiently through solving a semi-definite programming problem (SDP). In addition, we propose a verification approach to assure the validity of the synthesized interpolant and consequently avoid the unsoundness caused by numerical error in SDP solving. Finally, we demonstrate how to apply our approach to invariant generation in program verification.
报告人简介: Naijun Zhan is a research professor of State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences. He got his bachelor degree and master degree both from Naijun University, and his PhD from Institute of Software Chinese Academy of Sciences. Prior to join Institute of Software, Chinese Academy of Sciences, he worked at the Faculty of Mathematics and Informatics, Mannheim University, Germany as a research assistant. He is a distinguished research professor of Chinese Academy of Sciences (since 2015), the winner of Outstanding Youth Fund of Natural Science Foundation of China (in 2016). His research interests include formal design of real-time, embedded and hybrid systems, program verification, concurrent computation models, modal and temporal logics, etc. Currently, he serves the editorial boards of Formal Aspects of Computing, Journal of Logical and Algebraic Methods in Programming, Journal of Software, Journal of Computer Research and Development.