About the Winter School
We are excited to invite you to the Winter School on Formal Verification and Program Synthesis, hosted at CSE IIT Delhi from December 3rd to 6th, 2024. This workshop is designed to provide participants with a comprehensive overview of recent advancements in constraint solvers and automated reasoning, along with their cutting-edge applications in diverse fields such as the verification of deep neural networks, security, blockchains and synthesis. The four-day workshop will feature a series of lectures and hands-on sessions led by Subodh Sharma, Kumar Madhukar, and Priyanka Golia .
List of Topics
- Subodh Sharma: Introduction to Symbolic Execution and Bounded Model Checking; Applications to Security and Blockchains. Tools: CProver
- Kumar Madhukar: Verification of Deep Neural Networks, Abstraction-Refinement, Invariants and Connection to Program Verification Hands-on session with a DNN verification tool (NeuralSAT/Marabou).
- Priyanka Golia: Introduction to propositional logic modeling, constraint encoding, and the basics of SAT (Satisfiability) and SMT (Satisfiability Modulo Theories) solvers (basic introduction to DPLL and CDCL). Applications of these solvers in synthesis! Tools: Manthan, MiniSAT, Z3.
Logistics
- Dates: 3-6 December 2024
- Venue: Room 101, Bharti Building, CSE Department, IIT Delhi. Here is the pinned location.
- Travel Support: We will provide travel support of 3000 INR for outstation candidates and 1000 INR for students from Delhi-NCR.
- Accommodation: Hostel accommodation has been arranged for all participants who opted for it. Male participants are requested to report to Girnar Hostel, while female participants should report to Sahyadri Hostel. Please carry a valid government-issued ID (such as Aadhar Card) and your institute ID for verification. Participants are required to check out before lunch on December 7, 2024.
- After winter school: Interested students will be encouraged to apply for internships at IIT Delhi during eight weeks of summer 2025. Stipend will be offered to cover living and stay expenses in the IIT hostel during the internship.
Please note that we will NOT give any certificate of completion and will NOT provide recommendation letters to graduate schools or otherwise for participating in the school.
Programme
This is tentative. It is subject to change depending upon attendee interests.
Registration Deadline is over
We have sent out emails to all shortlisted students. We are pleased to inform you that hostel accommodation has been arranged for all participants who opted for it. Selected participants are requested to plan their travel accordingly. Hostel check-in will be available starting from December 2nd.
- Software Model Checking for People Who Love Automata
- Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks