Published in Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I., 2017
We describe a SyGuS solver that combines the ideas of enumerative search and unification based synthesis
Download here
Published in University of Pennsylvania Library, 2016
Doctoral Dissertation
Download here
Published in Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II., 2015
We demonstrate how symmetry can be exploited to enable completion of protocol sketches (i.e., a partial or incomplete implementation of a distributed protocol), augmented with a set of high-level temporal logic requirements.
Download here
Published in Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014. Proceedings., 2014
This work demonstrates how finite-state protocols (i.e., protocols where the communicating agents do not have internal state variables) could be synthesized starting from a set of execution fragments of the protocol, together with a set of high-level temporal logic requirements.
Download here
Published in Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, 2013
The definition of the SyGuS problem, and a few solution strategies were described in this paper.
Download here
Published in ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, June 16-19, 2013, 2013
We demonstrated how a distributed protocol could be specified using a mix of protocol traces, incomplete protocol specifications and formal specifications expressed in linear temporal logic. This mixed specification was then compiled into a working protocol using program synthesis techniques.
Download here
Published in Model Checking Software - 18th International SPIN Workshop, Snowbird, UT, USA, July 14-15, 2011. Proceedings., 2011
We explored how explicit state model checking algorithms could be parallelized by utilizing the notion of iterative deepening.
Download here
Published in Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, 2011
This paper demonstrated how applications that were tolerant to some amount of “staleness” in the underlying consistency model could be parallelized more effectively.
Download here
Published in Proceedings of the 2009 ACM SIGPLAN/SIGBED conference on Languages, compilers, and tools for embedded systems, LCTES 2009, Dublin, Ireland, June 19-20, 2009, 2009
This paper extended the techniques presented in the CGO 2009 paper to synergistically utilize the CPU as well as the GPU for executing stream programs.
Download here
Published in Proceedings of the CGO 2009, The Seventh International Symposium on Code Generation and Optimization, Seattle, Washington, USA, March 22-25, 2009, 2009
This paper explored techniques to compile stream programs for efficient execution on GPUs.
Download here