Keynote Speakers
Title: Guiding Formal Methods with Discovered Knowledge
Prof. Swarat Chaudhuri, Rice University
Systems for automated formal reasoning about programs depend on human specification at multiple levels. Users of such a system must write full specifications of the tasks that they want performed. The designer of the system is expected to formalize the domain-specific language in which tasks are described, and specify the domain-dependent heuristics that guide automated reasoning. The assumption of specifications reflects a common expectation in formal methods research: that humans hold deep knowledge about problem domains and instances. In practice, this expectation can be violated and lead to hard-to-use or brittle tools. In this talk, we describe a new class of formal methods that address this difficulty through automatic discovery of knowledge from corpora of pre-existing code, execution traces, and proofs.
The starting point of this work is the observation that a human who describes or solves a reasoning task does not do so in a vacuum, but using insights established through prior experiences of their own or others. The thesis is that such insights can be algorithmically learned from datasets of existing formal artifacts, and can lead to systems for automated reasoning that demand less human intervention than traditional tools. The talk will describe multiple instantiations of this thesis, including a statistical notion of program correctness, a program synthesis algorithm guided by a "neural" model of program syntax and semantics, and an approach to program verification that uses pre-existing formal proofs.
Speaker Bio
Swarat Chaudhuri is an associate professor of computer science at Rice University. He is an expert on methods for automated reasoning about systems and the application of such methods in computer-aided programming.
Swarat received a bachelor's degree in computer science from the Indian Institute of Technology, Kharagpur, in 2001, and a doctoral degree in computer science from the University of Pennsylvania in 2007. From 2008-2011, he was an assistant professor at the Pennsylvania State University, University Park. He is a recipient of the National Science Foundation CAREER award and the ACM SIGPLAN Outstanding Doctoral Dissertation Award.
Keynote Speakers
- Prof. Swarat Chaudhuri, Rice University
- Dr. Markulf Kohlweiss, Researcher, Microsoft Research
- Dr. Rajeev K. Ranjan, Senior Group Director, R&D Formal and Automated verification, Cadence
- Prof. Andreas Veneris, University of Toronto