Ankush Desai.

“ There are known knowns; there are things we know that we know. There are known unknowns; that is to say, there are things that we now know we don’t know. But there are also unknown unknowns – there are things we do not know we don’t know.” – Donald Rumsfeld

Graduate Student at University Of California, Berkeley

  • June, 2013 - Present
    • •
  • EECS Department

Advisors
Prof. Sanjit Seshia and Dr. Shaz Qadeer.

Research Interests

Design tools and methodologies for building reliable systems. I am interested in the areas of programming languages, model checking, and verification with focus on building complex real-world systems like a device drivers, distributed systems and distributed embedded systems.

Main Projects

  • P -> Event driven programming language for safe-asynchronous programs. P @ Github
  • ZING -> Explicit State Model-Checker for concurrent programs. Supports completely parallel search, stratified search based on delay bounding. ZING @ Github
  • COP -> Component Oriented Programming for building reliable distributed systems compositionally. Extending the programming language P with module system for compositional design. COP @ Github .. coming soon

Publications.

Links to my papers can be found at Google Scholar Page

Systematic Testing of Asynchronous Reactive Systems
  • Ankush Desai, Shaz Qadeer and Sanjit Seshia
    • •
  • FSE
    • •
  • 2015
Approximate Synchrony: An Abstraction for Distributed Almost-synchronous Systems
  • Ankush Desai, Sanjit Seshia, Shaz Qadeer, David Broman, and John Eidson
    • •
  • CAV
    • •
  • 2015
Endlessly Circulating Messages in IEEE 1588-2008 Systems
  • David Broman, P Derler, Ankush Desai, John Eidson, and Sanjit Seshia
    • •
  • International IEEE Symposium on Precision Clock Synchronization for Measurement, Control and Communication
    • •
  • 2014
Natural proofs for Asynchronous Programs using Almost-synchronous Invariants
  • Ankush Desai, Pranav Garg, and P. Madhusudan
    • •
  • OOPSLA
    • •
  • 2014
P: safe asynchronous event-driven programming
  • Ankush Desai, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani, Damien Zufferey
    • •
  • PLDI
    • •
  • 2013
Critical path based performance models for distributed queries
  • Ankush Desai, Kaushik Rajan, Kapil Vaswani
    • •
  • MSR-TR
    • •
  • 2012
Depth bounded explicit-state model checking
  • Abhishek Udupa, Ankush Desai and Sriram Rajamani
    • •
  • SPIN
    • •
  • 2011


Under Submission.


Building Reliable Systems using WYSIWYX (What You Specify Is What You eXecute)
  • Ankush Desai, Ethan Jackson, Amar Phanishayee, Shaz Qadeer and Sanjit Seshia
    • •
  • under submission