About

We are excited to host the second winter systems school during 4-8 December 2023 at CSE, IIT Delhi. We will study classic and contemporary topics in program analysis and optimization, taught by Sorav Bansal and Kumar Madhukar. The school will have a series of guest lectures, on symbolic execution and fuzzing, and their application to neural network analysis, by Subhajit Roy.

Inaugural talk by Ranjit Jhala on “Flux: A Language Integrated Verifier for Rust”

December 4th, 9-10:30 am (delivered virtually)

The last few decades have seen great strides in various technologies for analyzing programs. However, we believe these technologies will only become ubiquitous if they can be seamlessly integrated within programming languages with mature compilers, libraries and tools, so that programmers can use them continuously throughout the software development lifecycle (and not just as a means of post-facto validation.)

In this talk, we will describe Flux: a new language integrated verifier for the Rust programming language that lets the programmer write specifications — by combining logical refinements with Rust’s ownership mechanisms — which permits automatic verification using a combination of SMT and abstract interpretation.

We demonstrate the advantages of refinement types by using a suite of benchmarks to compare Flux with classical program logic based approaches as implemented in the state-of-the-art Prusti verifier. We show that by exploiting language structure to factor complex program invariants into simple types and refinements, Flux can make verification ergonomic by slashing specification lines by a factor of two, verification time by an order of magnitude, and the programmer’s annotation overhead from up to 24% of code size (average 14%), to nothing at all.

Tentative schedule:

4th Dec 0900-1030
Inaugural Talk
(Ranjit Jhala)		 1030-1100
Tea/Coffee		 1100-1230
Introductory Sessions
(30 mins for every speaker)		 1230-1400
Lunch		 1430-1700
Lab
5th Dec 0900-1030
Session I
(Sorav Bansal)		 1030-1100
Tea/Coffee		 1100-1230
Session II
(Sorav Bansal)		 1230-1400
Lunch		 1430-1700
Lab
6th Dec 0900-1030
Session I
(Subhajit Roy)		 1030-1100
Tea/Coffee		 1100-1230
Session II
(Subhajit Roy)		 1230-1400
Lunch		 1430-1700
Lab
7th Dec 0900-1030
Session I
(Kumar Madhukar)		 1030-1100
Tea/Coffee		 1100-1230
Session II
(Kumar Madhukar)		 1230-1400
Lunch		 1430-1700
Lab
8th Dec 0900-1000
Concluding Session I
(Kumar Madhukar)		 1000-1030
Tea/Coffee		 1030-1230
Concluding Session II
(Subhajit Roy)

Concluding Session III
(Sorav Bansal)		 1230-1400
Lunch		  

List of topics (speaker-wise):

  • Sorav Bansal: Introduction to logic, Hoare logic, Weakest precondition, Automatic invariant inference, Equivalence checking, Superoptimization: slides1, slides2, labs, demo-files: strlen_src.c, strlen_dst.c, s119.c, s119.s, bzip2.c

  • Subhajit Roy: Program Testing Fundamentals, Symbolic Execution, Symbolic Execution for testing Neural Networks, Neural network guided testing of Software Systems: slides, labs

  • Kumar Madhukar: Formal Verification of Deep Neural Networks, Abstraction-Refinement Techniques, Pruning and Slicing of DNNs, Verifying Learning-Augmented Systems, Recurrent, Convolutional, and Binarized Neural Networks, Explainability: introductory-slides, lecture-slides, lab, lab2

Submit your lab answers

Please use this Google form to submit your lab answers.

Submit your feedback on WSS23

Please use this Google form to submit your feedback on WSS23.

Logistics

  • Dates: 4-8 December 2023
  • Venue: The talks will be in Room 501 on the fourth floor of the Bharti Building and the labs will be held in Room LH504 on the fifth floor of the Lecture hall complex.
  • Accommodation We will try and provide hostel accommodation to the selected participants during 3-8 December 2023. You will need to check-out before lunch on 9th December 2023. Please be aware that the availability of hostel accommodation depends on several external factors that are beyond our control. While we expect everyone to be able to get hostel accommodation, do not assume this until you receive a confirmation from us. We will do our best to confirm this (for the selected participants) as soon as possible.
  • After winter school: Interested students will be encouraged to apply for internships at IIT Delhi during eight weeks of summer 2024. 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.

Application process

The typical profile of a participant will be a final-year undergraduate student or a post-graduate (Masters/PhD) student or an industry professional interested in getting introduced to advanced topics in program analysis and optimization.

Please fill the form at this link before 11:59pm on 31st October 12th November 2023 to apply to attend the Winter school. The form requires you to read a paper/blog, and write what you understood from it. Please budget at least two days for this.