[Curriculum vitae] Arjun Radhakrishna
An up-to-date version of this page can be found here.


I am a researcher in the PROSE team at Microsoft working on program synthesis. Previously, I was a post-doctoral researcher at the University of Pennsylvania working in the group of Prof. Rajeev Alur. Before that, I completed my PhD at IST Austria under the guidance of Prof. Thomas A. Henzinger. Check out my dissertation here.

My research area relates to using programming languages and formal methods to help programmers and designers develop reliable, safe, and correct systems. In particular, I have been working heavily on program synthesis. However, I'm interested in all domains of formal methods and rigourous system engineering.

My specific interests are in developing tools to handle soft and quantitative specifications in various domains such as concurrency and embedded systems. Soft specifications are program properties which are desirable, but are not necessary for correctness (e.g., program performance and energy consumption).

News
  • Paper on Starling: Callback Typestates for Android Classes [pdf] was accepted at ICSE 2018. This work is about the automated learning of callin/callback protocols from android framework classes. Our implementation discovered several unknown bugs and corner cases in the android framework.
  • Paper on Scaling Enumerative Program Synthesis via Divide and Conquer [pdf] was accepted at TACAS 2017. The paper contains a full description of a novel, efficient algorithm for the Syntax-Guided Synthesis problem.
  • I presented preliminary results on the Synthesis of Interface Specifications for Android Classes at the IBM PL day 2016. This work is about the automated learning of asynchronous typestate for android framework classes. Our implementation discovered several unknown bugs in the android framework. Technical report can be found here.
  • EUSolver (built by Abhishek Udupa and me) performed exceedingly well in the Syntax-guided Synthesis (SyGuS) competition 2016, winning the "general" and "programming-by-examples" track. EUSolver combines enumerative techniques for program synthesis [Udupa et. al. PLDI 2013] with unification [CAV 2015].
  • Roopsha Samanta and I presented a tutorial on Trace-based Synchronization Synthesis for Concurrent Programs at POPL 2016. The tutorial will cover a large part of our work on synthesis for concurrency from the past few years.
  • Recent and upcoming service:
    • CAV 2018: Program Committee.
    • CAV 2017: Program Committee.
    • SYNT 2017: Program Committee.
    • (EC)2 2016: Program Committee.
    • SYNT 2016: Program Committee.
    • CAV 2016: External Reviewing Committee.
    • PLDI 2016: External Reviewing Committee.
Major Projects
  • Performance-aware Synthesis for Concurrency. Usable concurrency synthesis has been a long-standing goal, with over three decades of active research going into it. Here, a programmer is expected to write a program that is correct in a sequential context, and the synthesizer inserts sufficient synchronization (locks) to make the program behave correctly in a concurrent setting. However, the issue of performance of the synthesized program has not been fully addressed. In this project, we attempt to address this issue by both optimizing the synchronization inserted by the synthesizer, and by avoiding synchronization completely by using more "programmer-like" techniques.
  • Quantitative Specifications for Reactive Systems. In this project, we attempt to construct a quantitative specification framework for analysis of reactive systems. Our framework is built on a novel notion called simulation distances. A simulation distance measures some aspect of "match" of a given system with respect to a property. The "match" could be anything including a measure of correctness (how often the system violates the property) or robustness (how much can the system be externally disturbed before it violates the property). We give algorithms to synthesize optimal systems with respect to this quantitative specifications.
Dissertation

The goal of formal methods has long been to produce software or hardware systems with provable guarantees on correctness. However, not all correct systems are equally desirable and not all incorrect systems are equally undesirable. In many cases, the notion of desirability of a system can be encoded as a quantity. Example of such quantities include execution time and energy consumption. My dissertation develops techniques for formal verification and synthesis for such quantitative specifications.

My dissertation was awarded the 2014 ACM SIGBED Paul Caspi Memorial Dissertation Award. The award is presented annually to the author of an outstanding dissertation in the area of Embedded Systems to recognize work that significantly advances the state of the art in the science of embedded systems, in the spirit and legacy of Dr. Paul Caspi's work.

Quantitative Specifications for Verification and Synthesis
Arjun Radhakrishna
PhD Thesis, Institute of Science and Technology, Austria
July 2014
Publications
[ Google Scholar, DBLP ]
Starling: Callback Typestates for Android Classes
Arjun Radhakrishna, Nicholas V. Lewchenko, Shawn Meier, Sergio Mover, Krishna Chaitanya Sripad, Damien Zufferey, Bor-Yuh Evan Chang, and Pavol Cerny
ICSE 2018
Scaling Enumerative Program Synthesis via Divide and Conquer
Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa
TACAS 2017
Synthesis through Unification
Rajeev Alur, Pavol Cerny, and Arjun Radhakrishna
CAV 2015
From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis
Pavol Cerny, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, and Thorsten Tarrach
CAV 2015
Runner-up at the CAV artifact evaluation
Segment Abstraction for Worst-Case Execution Time Analysis
Pavol Cerny, Thomas A. Henzinger, Laura Kovacs, Arjun Radhakrishna, and Jakob Zwirchmayr
ESOP 2015
Succinct Representation of Concurrent Trace Sets
Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna, Roopsha Samanta, and Throsten Tarrach
POPL 2015
Interface Simulation Distances
Pavol Cerny, Martin Chmelik, Thomas Henzinger, and Arjun Radhakrishna
TCS 2014
Regression-free Synthesis for Concurrency
Pavol Cerny, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Throsten Tarrach
CAV 2014
Battery Transition Systems
Udi Boker, Thomas A. Henzinger, and Arjun Radhakrishna
POPL 2014
Efficient Synthesis for Concurrency using Semantics-Preserving Transformations
Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, and Thorsten Tarrach
CAV 2013
Quantitative Abstraction Refinement
Pavol Cerny, Thomas Henzinger, and Arjun Radhakrishna
POPL 2013
Synthesis from Incompatible Specifications
Pavol Cerny, Sivakanth Gopi, Thomas Henzinger, Arjun Radhakrishna, and Nishant Totla
EMSOFT 2012
Nominated for the Best Paper award
Interface Simulation Distances
Pavol Cerny, Martin Chmelik, Thomas Henzinger, and Arjun Radhakrishna
GANDALF 2012
Quantitative Synthesis for Concurrent Programs
Pavol Cerny, Krishnendu Chatterjee, Thomas Henzinger, Arjun Radhakrishna, and Rohit Singh
CAV 2011
Simulation Distances
Pavol Cerny, Thomas Henzinger, and Arjun Radhakrishna
CONCUR 2010.
Model Checking of Linearizability of Concurrent List Implementations
Pavol Cerny, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, and Rajeev Alur
CAV 2010
Quantitative Simulation Games
Pavol Cerny, Thomas A. Henzinger, and Arjun Radhakrishna
Essays in Memory of Amir Pnueli, 2010
GIST: A Solver for Probabilistic Games
Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, and Arjun Radhakrishn
CAV 2010