Formal Methods Update Meeting 2026

Meeting Programme

The schedule below is tentative; further details will be added in due course.

July 1, 2026 Pre-Event Tutorial

TimeSpeakerTitle
9:00 PM – 10:30 PM Shibashis Guha Tutorial on Reactive Synthesis

July 2, 2026 Main Event, Day 1

TimeSpeakerTitle
9:00 AM – 9:30 AM Opening Remarks
9:30 AM – 10:00 AM Sujata Ghosh A Modal Approach Towards Substitutions
10:00 AM – 10:30 AM S. P. Suresh Intruder Theories
Tea Break · 10:30 AM – 10:45 AM
10:45 AM – 11:15 AM K. C. Sivaramakrishnan From Convergence to Confidence: Push-Button Verification for Replicated Data Types
11:15 AM – 11:45 AM Ashish Mishra Refinement Types: A Powerful Machinery for Verification, Synthesis and Testing
Tea Break · 11:45 AM – 12:00 PM
12:00 PM – 12:30 PM Abhishek Singh State Reachability Under Weak Memory: From Decidability Frontiers to Visibility-Guided Testing
12:30 PM – 1:00 PM Subodh Sharma Formal Verification of End-to-End Verifiable Election Protocols
Lunch Break · 1:00 PM – 2:30 PM
2:30 PM – 3:00 PM Siddhartha Gadgil Autoformalization by Combinator Code Generation
3:00 PM – 3:30 PM Piyush Kurur Certified Regular Expression Matcher in Rocq
3:30 PM – 4:00 PM Shweta Rajiv Bridging Bit-Vectors and Natural Numbers in Isabelle/HOL
Tea Break · 4:00 PM – 4:30 PM
4:30 PM – 5:00 PM Ramit Das Verifying Error Correction Coding Algorithms using Symbolic Trajectory Evaluation
5:00 PM – 5:30 PM Gourav Takhar Incorrectness Proofs with Underapproximation Invariants
5:30 PM – 6:00 PM Ravindra Metta
Banquet

July 3, 2026 Main Event, Day 2

TimeSpeakerTitle
9:30 AM – 10:00 AM Aiswarya C. Edit Distance of Finite State Transducers
10:00 AM – 10:30 AM Supratik Chakraborty Proof Systems for QBF Synthesis: Extracting Skolem and Herbrand Functions
Tea Break · 10:30 AM – 10:45 AM
10:45 AM – 11:15 AM B. Srivathsan Generalized Timed Automata
11:15 AM – 11:45 AM Pranshu Gaba Sure-Almost-Sure and Sure-Limit-Sure Window Mean Payoff in Markov Decision Processes
Tea Break · 11:45 AM – 12:00 PM
12:00 PM – 12:30 PM Akshay S. Decision Tree Ensembles: A Sweet Spot between Machine Learning and Formal Methods
12:30 PM – 1:00 PM Deepak D'Souza Understanding the IC3 verification algorithm
Lunch Break · 1:00 PM – 2:30 PM
2:30 PM – 3:00 PM Sumanth Prabhu On Robustness of Linear Classifiers to Targeted Data Poisoning
3:00 PM – 3:30 PM Amaldev Manuel Circuit Complexity of Regular Languages
3:30 PM – 4:00 PM Rishal S. P. Set Automata and Limits of Decidability of Two-Variable Logic on Data Words
Tea Break · 4:00 PM – 4:30 PM
4:30 PM – 5:00 PM Sreejith A V Regular Expressions over Countable Words
5:00 PM – 5:30 PM Sayan Mukherjee Synthesizing POMDP Policies: Sampling meets Model-checking via Learning
5:30 PM – 6:00 PM Abhisekh Sankaran

July 4, 2026 Post-Event Tutorial

TimeSpeakerTitle
10:00 AM onwards Society for Electronic Transactions and Security Applied Formal Methods in Cryptography