In this talk, I will present how ideas from Algebraic Geometry can be harnessed to design efficient algorithms for program synthesis and formal verification. I will begin with an accessible introduction to algebro-geometric algorithms, illustrating how classical results such as Hilbert’s Nullstellensatz and Positivstellensatz form the theoretical backbone of modern computational methods for solving systems of polynomial equations.
Building on this foundation, I will focus on one central theme from my recent research: template-based synthesis of polynomial programs and Skolem functions. I will discuss how synthesis problems can be expressed as systems of polynomial constraints and how Skolem functions can be algorithmically constructed using algebro-geometric principles. I will then describe our approach to ensuring soundness and semi-completeness while maintaining computational efficiency.
Finally, I will present experimental results comparing our algorithms with state-of-the-art synthesis and verification tools, highlighting how classical mathematical structures can inspire new algorithmic paradigms for formal methods. The talk is designed to be self-contained, with necessary definitions and motivating examples included throughout.
Zoom link: https://icts-res-in.zoom.us/j/99108753958?pwd=gbNBTswrROv95cROafaRwt2ewBc77i.1
Meeting ID: 991 0875 3958
Passcode: 313232