Talk: Democratizing Verification: Overcoming Expertise Gaps using Logic Learning and New Predictable Paradigms

LIVE STREAM: https://uwmadison.zoom.us/j/99822008057?pwd=SmUwNUdtdTc1Tis5ZERaVThTalhNZz09

Abstract: Software verification is key to engineering trustworthy and reliable systems. However, verification is at an impasse in techniques for practical adoption. In this talk, I will argue that the current state-of-the-art is fundamentally un-democratic: programmers have no hope of being able to use existing automated tools to verify their code without a Ph.D. in programming languages!

I address this challenge from both theoretical and practical standpoints, showing foundational theoretical results on the democratization gaps in existing automation and using these insights to build new algorithms that bridge these gaps. The central innovation in bridging the gap is data-driven logic learning, i.e., learning logical formulas from data.

Finally, I introduce a transformative vision of verification for the future through a new verification paradigm called Predictable Verification that is democratic by design. I conclude by highlighting my vision for the future on building verified systems without involving verification experts, using symbolic and deep machine learning to democratize verification, and discuss some new applications that benefit from synergies of reasoning and learning.

Bio: Adithya Murali is a doctoral candidate in programming languages at the University of Illinois Urbana-Champaign. His research interests span problems in program verification, program synthesis, and using learning techniques for verification and synthesis. His work covers the spectrum from theory to practice and appeared at several venues, including POPL,  PLDI, OOPSLA, CAV, ESOP, FMCAD, TOPLAS, and IJCAI. You can find more about his research, teaching, and advocacy efforts on his website: https://muraliadithya.github.io/