The last three days of the summer school were mostly hands-on, with Prof. Siddhartha Gadgil explaining important concepts such as inductive types and monads. I will probably write separate blogposts covering these topics standalone, as they are quite deep. The blog for inductive types will be based on a session which I plan to take as a part of the PACE Lab Research Huddle, which would be based upon my learnings in this summer school.
Day 3 - Prof. KV Raghavan on Program Analysis
This talk was a departure from the usual theme of type system-based verification as in Lean. It covered the overapproximation alternative, i.e. Program Analysis. I was mostly familiar with the contents of this talk, which primarily revolved around using Data Flow Analysis (DFA) to safeguard from low level bugs, such as null pointer exceptions, use-after-free (UAF) and accessing uninitialized variables. Proving properties such as these require a traversal of the Control Flow Graph (CFG) of the program, and there are excellent analyses which perform each of these depending on the precision and memory bandwidth available.
These analyses can be inter or intraprocedural (meaning performed across functions, or within the same function as context), flow sensitive or insensitive (depending on whether the analysis depends on the order of the statements in the CFG), as well as context sensitive or insensitive (depending on whether each function call site is analyzed independently or not). The talk covered some interesting examples and motivated the field well. I would still recommend Prof. Rupesh's course on Program Analysis (which I had taken during my third year) as a comprehensive look at the field.
Other talks
There were quite a few other talks, many of which were delivered by the winners of the hackathon Emergence had conducted earlier. I describe some of the interesting ones here. Harisankar, a fellow attendee, offers a more comprehensive look.
-
Transpiling python to lean - this is an ambitious project which can be fast-tracked because LLMs have become so good at coding. Considerable progress was made by Anirudh Gupta, an undergraduate student at IISc. The work supports quite a few constructs of Python, and supports a form of monadic theorem proving using the mvcgen tactic. I am still yet to look into the coverage of the prover itself, although the talk did show some simple examples coded up in imperative Python, being verified in Lean using pre and postcondition annotations.
-
Checking equivalence of database queries - Given a database schema, two SQL queries could be checked for equivalence. I have to check if there exists a deterministic algorithm to perform such a check, but the talk gave a good account of using Lean to demonstrate a proof-based technique to show equivalence. A shallow embedding was used, which demonstrated the power of Lean - most simple DSLs can be encoded in Lean and would execute as Lean code. This was great work done at Prof. Gadgil's group and presented by Ajay Nair.
Both these projects were in collaboration with Emergence. It remains to be seen as to how they scale and whether they can actually be used in industry, although they seem quite promising.
Conclusion
My overall experience was great, and it was good to see a lot of people from various walks of life interested in formal methods. Thanks to IISc and Emergence for the great week!