Research Interests
Software verification and formal methods; Interpretable, Robust, Trustworthy AI/ML; Program Synthesis and Machine Learning; Security and Privacy; 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 automated 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.
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 inductive
techniques from large data (like neural net models) can be combined with symbolic techniques
(learning/searching interpretable concepts, including logical formulas and programs) to build more
intelligent systems (see IJCAI paper).
One new permeating theme in my explorations is learning logics. We use learning of logic
formulas in applications ranging from software verification (ICE learning), software specification mining (learning preconditions and contracts), and in AI application (interpretable visual discriminators).
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 to learn interpretable (symbolic) concepts, abstraction, and reasoning (see IJCAI 2022 and POPL 2022 papers).
Learning logics: Theoretical and practical algorithms for learning logical concepts (see POPL 2022).
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, and new paper on inductive lemma synthesis.
Logics and reasoning for program verification: especially logics
involving expressive specifications for programs manipulating
quantified specifications and datastructures, in particular first order logic with least fixpoints.
See papers on natural proofs in POPL 2012, PLDI 2013, PLDI 2014, and POPL 2018, work on Frame Logic (ESOP 2020),
and new paper on inductive lemma synthesis for FO+lfp.
Building verified software using almost-automated verification,
especially distributed systems that involve crptography,
like blockchains, bitcoin, and smart contracts (see FMCAD 2019).
In particular, I am interested in theory and practice of refining abstract models to concrete distributed models.
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; learning logics)
Paul Krogmeier (learning 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:
Fall 2022:
CS521: Advanced Topics in Programming Systems: Trustworthy AI Systems (with Gagandeep Singh)
Earlier courses
Service
PC Member: OOPSLA 2022
PC Member: CONCUR 2022
PC Member: CSR 2022
PC Member: POPL 2022
PC Member: LATA 2021
PC Member: LATA 2020
PC Member: POPL 2019
PC Member: ICALP 2019
PC Member: CONCUR 2018
ERC: PLDI 2017
PC Member: Workshop on Automated Deduction for Separation Logics (ADSL), affiliated with LICS and FLOC, 2018.
PC Member: TACAS 2017
PC Member: Highlights of Logic, Automata, and Games, 2017.
PC Member: International Conference on Runtime Verification (RV 2017).
Tutorial on Machine-learning based methods for synthesizing invariants.
, at Computer Aided Verification (CAV), San Fransisco, USA, 2015.
PC Member: ICALP 2016: Int'l Colloq. on Automata Languages and Programming, Rome, Italy.
External Review Committee: CAV 2016: Computer Aided Verification, Toronto, Canada.
Co-chair/Organizer: SYNT 2015: 4th Workshop on Synthesis (associated CAV), San Francisco, USA.
PC Member: Trustworthy Global Computing (TGC), 2015, Madrid, Spain.
ERC Member: PLDI 2015, Portland, Oregon, USA.
PC Member: ACM/IEEE International Conference on
Model Driven Engineering Languages and Systems, 2014, Madrid, Spain.
PC Member: POPL 2015, Mumbai, India.
PC Member: PLDI 2014, Edinburgh, Scotland.
PC Member: CONCUR 2014, Rome, Italy
PC Member: SAS 2014, Munich, Germany
Earlier
2013: PC Member: MFCS, 2013, CAV 2013, Highlights of Logic, Automata, Games
2012: PC Chair: CAV 2012; PC Member: LPAR-18, POPL 2012.
2011: PC Member: CAV 2011, ATVA 2011, FSTTCS 2011.
2010: PC Member: FSTTCS 2010, ATVA 2010,
STACS 2010,
2009: PC member: CAV 2009,
LICS 2009, TIME 2009; Ext Rev Committee: PLDI 2009
2008: PC Member: APLAS 2008, CONCUR 2008.
2007 PC Chair: INFINITY 2007 (with CONCUR); PC Member: ICALP 2007
2006 PC member: ACM SAC.
2005 PC member: FSTTCS 2005, CAV 2005.
GDV 2005 (with CAV'05).
2004 PC member: FORMATS and FTRTFT, 2004
Other Activities: Organized events, invited talks, etc.