Madhusudan's homepage

Research Interests

Software verification; Security; Program Synthesis and Machine Learning; Logic and automata theory;

Outreach Interests

ConTraIL project: Privacy-preserving contact tracing project. See Whitepaper.

Current research projects and philosophy

My general research philosophy is to turn the theory lens (mainly logic and algorithms) towards practical computing domains. I shy away, for the most part, from working on problems purely motivated by theoretical concerns as well as those entirely based on heuristics to solve practical problems.

My current research interests are primarily in automating software verification, building correct-by-design secure distributed systems, and exploring synergies between machine learning and program synthesis for building intelligent systems.

Automating software verification: Proving a program safe using logical techniques is composed of two phases: finding possible inductive invariants and formally establishing that they are inductive invariants that prove safety.

For the latter problem, the main approach that I currently believe in for automation is the framework of natural proofs that we have been working on for the last 10 years. In particular, though I believe decidable logics are useful for this problem, I do not believe they will solely be powerful enough for addressing the needs of program verification, due to their inherent inexpressivity. Natural proofs aim for sound and oftentimes complete (though not decidable) approaches for this problem.

As for the former problem for finding invariants, I believe that a combination of several techniques that are proposed in recent literature (including interpolation and IC3) are called for. The primary techniques techniques I work on have been those based on learning and (more recently) finding uninterpreted invariants.

Building verified systems: My view on building verified systems is that they should be built correct by construction (as opposed to verifying existing systems), by proving more abstract systems correct and then refining them to concrete performant code. The proofs of abstract systems against complex specifications would invariably require considerable human input and intuition, while automation can help in refining abstract systems to performant code.

Machine Learning and Program Synthesis: One of my latest interests is in building synergies of program synthesis and machine learning--- I believe practical pattern-matching inductive techniques (like neural nets) can be combined with symbolic search (like synthesizing logical formulas and programs) to build more intelligent systems.

Note to prospective students

I am actively looking for Ph.D. students in the following areas. If you are interested, please apply for the Ph.D. program and write to me personally.

Machine learning and program synthesis; learning logics. Exploring new techniques that go beyond neural nets by using symbolic search, abstraction, and reasoning.

Building verified software using almost-automated verification, especially distributed systems that involve crptography, like blockchains, bitcoin, and smart contracts.

Logics and reasoning for program verification: especially logics involving expressive specifications for programs manipulating quantified specifications and datastructures. See papers on natural proofs in POPL 2012, PLDI 2013, PLDI 2014, and POPL 2018, and the Dryad and VCDryad) pages.

Invariant synthesis and mining specifications from code using machine learning, online learning, and learning logical formulas. See papers in CAV14, POPL16, TACAS16, TOCL18, TACAS18, OOPSLA18.

Exploring the world of uninterpreted programs--- we have discovered a new technique for verifying uninterpreted programs using complete/decidable techniques for generating inductive invariants. This opens up a wide avenue for future work--- tracttable verification, invariant synthesis, synergy with natural proofs, and program synthesis.

Earlier research Projects

Decidable logics for reasoning with heaps/dynamic data structures (Strand)

Security of web browser extensions (VEX)

Testing concurrent programs (Penelope)

Security of access control (VAC)

Annotation and proof mechanisms for safe concurrency (Accord)

Model-checking abstractions of programs (Getafix)

Decidable automata models (See page on visibly pushdown automata)

Software/tools:

VCDryad - An extension of VCC that provides sound but incomplete automatic mechanisms against Dryad specifications, a dialect of separation logic.

Dryad - Sound but incomplete mechanism for proving heap-based programs correct

CAV 2013 tool - for learning universally quantified invariants on linear data-structures using quantified data automata

Strand - Decidable logics/SMT solver for reasoning with heaps

Getafix - A boolean model-checker for concurrent and recursive programs

VEX - Static analysis of web-browser extensions for security vulnerabilities

Penelope - A testing tool for concurrent programs

VAC - Verifier of Access Control

JIST - Java Interface Synthesis Tool

Students and Post-doctoral researchers:

Students currently advised:

Angello Astorga (mining program specifications), jointly advised with Tao Xie

Adithya Murali (combining machine learning and program synthesis; learnin logics)

Shambwaditya Saha (synthesis, learning, mining specifications)

Formerly advised:

Students:

Pranav Garg (deductive verification; compositional verification)

Edgar Pek (static analysis; points-to analysis)

Francesco Sorrentino (testing concurrent programs)

Xiaokang Qiu
Thesis: Automatic Techniques for Proving Correctness of Heap-Manipulating Programs
Now postdoc at MIT/UMD.

Sruthi Bandhakavi; security of web extensions -- now at Google

Postdocs:

Gennaro Parlato -- now faculty at University of Southampton

Karl Palmskog-- now a postdoc at UT Austin.

Daniel Neider (automated deductiver verification, synthesis, learning, invariant synthesis)
Post-doctoral researcher in the ExCAPE project, jointly at Illinois and UCLA. -- now at Max Planck Institute

Courses:

Note to graduate students: If you are interested in mainstream software verification, I suggest that you take the course CS477 (Formal Methods in Software Development) followed by my course CS598MP (offered only once in a while) on Software Verification. The CS598MP course is more advanced, and CS477 will be a pre-requisite for it in the future. I also strongly encourage you to take the CS498 course on "Logic in Computer Science" (aka Logical Systems) offered by me or Prof. Viswanathan before you take CS58MP:Software Verification.

Spring '14: CS498: Logic in Computer Science

Fall '13: CS173: Discrete Structures

Fall '11: CS373: Intro to Theory of Computation

Spring '11: CS477: Formal Methods in Software Development

Earlier courses

Also check out the following:

Formal Methods Seminar at Illinois

The new Formal Methods Reading List