- R. Alur, L. D’Antoni, S. Gulwani, D. Kini, and M. Viswanathan. Automated grading of DFA constructions.In Francesca Rossi, editor, IJCAI. IJCAI/AAAI, 2013.
- R. Alur, M. Martin, M. Raghothaman, C. Stergiou, S. Tripakis, and A. Udupa. Synthesizing finite-state protocols from scenarios and requirements. 10th Haifa Verification Conference, 2014.
- A. Butez, Y. Wang, and S. Lafortune. State-partition-based control of discrete event systems for enforcement of regular language specifications. In IFAC World Congress 2014.
- A. Cheung, A. Solar-Lezama, and S. Madden. Optimizing database-backed applications with query synthesis. In Hans-Juergen Boehm and Cormac Flanagan, editors, PLDI, pages 3–14. ACM, 2013.
- C. Chen, L. Jia, H. Xu, C. Luo, W. Zhou, and B. T. Loo. A formal framework for secure routing protocols. In USENIX Symposium on Networked Systems Design and Implementation (NSDI) (demonstration), 2013.
- A. Donze, G. Juniwal, J. C. Jensen, and S. A. Seshia. GPSGrader: Synthesizing temporal logic testers for auto-grading. In Submitted to CAV 2014.
- J. A. DeCastro, H. Kress-Gazit: Guaranteeing reactive high-level behaviors for robots with complex dynamics. IROS 2013: 749-756
- E. Dallal, A. Colombo, D. Del Vecchio, and S. Lafortune. Supervisory control for collision avoidance in vehicular networks with imperfect measurements. In Proceedings of the 52nd IEEE Conference on Decision and Control (CDC). December 2013, pp. 6298-6303.
- E. Dallal and S. Lafortune. On Most Permissive Observers in Dynamic Sensor Activation Problems. IEEE Trans. Automat. Contr. 59(4): 966-981 (2014).
- R. Ehlers, S. A. Seshia, and H. Kress-Gazit. Synthesis with Identifiers. In Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 415–433, January 2014.
- T. Hottelier, R. Bodik and K. Ryokai. Programming by Manipulation for Layout . Berkeley Technical Report, Aug 2014.
- J. Jeon, X. Qiu, J. S. Foster and A. Solar-Lezama. PASKET: Synthesizing Models of the Observer Pattern for Event-Driven Frameworks. Under review.
- G. Jing, R. Ehlers, H. Kress-Gazit: Shortcut through an evil door: Optimality of correct-by-construction controllers in adversarial environments. IROS 2013: 4796-4802
- G. Jing, H. Kress-Gazit: Improving the continuous execution of reactive LTL-based controllers. ICRA 2013: 5439-5445
- E. Lu and Ras Bodík. Quicksilver: Automatic synthesis of relational queries. Technical report, University of California, Berkeley, Technical Report No. UCB/EECS-2013-68, 2013.
- R. Luna, M. Lahijanian, M. Moll, and L. E. Kavraki. Asymptotically Optimal Stochastic Motion Planning with Temporal Goals. Workshop on the Algorithmic Foundations of Robotics (WAFR), Istanbul, Turkey, 2014.
- R. Luna, M. Lahijanian, M. Moll, and L. E. Kavraki. Fast Stochastic Motion Planning with Optimality Guarantees using Local Policy Reconfiguration. IEEE International Conference on Robotics and Automation, Hong Kong, China, 2014.
- R. Luna, M. Lahijanian, M. Moll, and L. E. Kavraki. Optimal and Efficient Stochastic Motion Planning in Partially-Known Environments. The Twenty-Eighth AAAI Conference on Artificial Intelligence, Quebec City, Canada, 2014.
- M. R. Maly, M. Lahijanian, L. E. Kavraki, H, Kress-Gazit, M. Y. Vardi. Iterative temporal motion planning for hybrid systems in partially unknown environments. HSCC 2013: 353-362
- L. A. Meyerovich, M. E. Torok, E. Atkinson, and R. Bodík. Parallel schedule synthesis for attribute grammars. In Alex Nicolau, Xiaowei Shen, Saman P. Amarasinghe, and Richard Vuduc, editors, PPOPP, pages 187–196. ACM, 2013.
- F. Miao, M. Pajic, R. Mangharam, G. J. Pappas. Networked Realization of Discrete-Time Controllers. In American Control Conference. Washington, DC, June 2013.
- P-M. Osera and S. Zdancewic. Teaching induction with functional programming and a proof assistant. In An Education Symposium at SPLASH, SPLASH-E, 2013.
- P M. Phothilimthana, T. Jelves, R. Shah, N. Totla, S. Chasins, and R. Bodík. Chlorophyll: Synthesis-aided compiler for lowpower spatial architectures. In ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2014.
- V. Raman and H. Kress-Gazit. Synthesis for multi-robot controllers with interleaved motion. In IEEE International Conference on Robotics and Automation 2014
- V. Raman, N. Piterman, and H. Kress-Gazit. Provably correct continuous control for high-level robot behaviors with actions of arbitrary execution durations. In IEEE/RSJ International Conference on Intelligent Robots and Systems, ICRA 2013, pages 4075–4081
- I. Saha, R. Ramaitithima, V. Kumar, G. J. Pappas and S. A. Seshia. Automated Composition of Motion Primitives for Multi-Robot Systems from Safe LTL Specifications. IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2014.
- A. Udupa, A. Raghavan, J. V. Deshmukh, S. Mador-Haim, M. M. K. Martin, R. Alur. TRANSIT: specifying protocols with concolic snippets. PLDI 2013: 287-296
- K. W. Wong, C. Finucane, H. Kress-Gazit. Provably-correct robot control with LTLMoP, OMPL and ROS. IROS 2013: 2073
- Y.-C. Wu and S. Lafortune. Synthesis of insertion functions for enforcement of opacity security properties. In Automatica.
- A. Wang, A. Gurney, X. Han, J. Cao, B T. Loo, C. Talcott, and A. Scedrov. A reduction-based approach towards scaling up formal analysis of internet configurations. In 33rd Annual IEEE International Conference on Computer Communications (INFOCOM), 2014.
- A. Wang, S, Moarref, B T. Loo, U. Topcu, and A. Scedrov. Automated synthesis of reactive controllers for software-defined networks. In ICNP, pages 1–6. IEEE, 2013.
- X. Yin and S. Lafortune. A general approach for synthesis of supervisors for partially-observed discrete-event systems. In IFAC World Congress 2014.
- X. Yin and S. Lafortune. "Synthesis of Maximally Permissive Non-blocking Supervisors for Partially Observed Discrete Event Systems". In CDC 2014.
- Y. Yuan, R. Alur, B. T. Loo. Netegg: Programming network policies by examples. 13th ACM Workshop on Hot Topics in Networks, 2014.
- Y. Yuan, A. Wang, R. Alur, and B. T. Loo. On the feasibility of automation for bandwidth allocation problems in data centers. In Formal Methods in Computer-Aided Design, FMCAD 2013, pages 42–45.

- R. Alur, R. Bodik, G. Juniwal, M.M.K. Martin, M. Raghothaman, S.A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. Syntax-guided Synthesis, FMCAD 2013
- R. Alur, L. D’Antoni, J. V. Deshmukh, M. Raghothaman, and Y. Yuan. Regular functions and cost register automata. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, pages 13–22.
- R. Alur, L. D’Antoni, M. Raghothaman. DReX: A Declarative Language for Efficiently Computable Regular String Transformations. In 28th 42nd ACM Symposium on Principles of Programming Languages, 2015.
- R. Alur, A. Durand-Gasselin, and A. Trivedi. From monadic second-order definable string transformations to transducers. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, pages 458–467.
- R. Alur, A. Freilich, and M. Raghothaman. Regular combinators for string transformations. 29th ACM/IEEE Symposium on Logic in Computer Science, 2014
- R. Alur and M. Raghothaman. Decision problems for additive regular functions. In F. V. Fomin, R. Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, ICALP (2), volume 7966 of Lecture Notes in Computer Science, pages 37–48. Springer, 2013.
- R. Alur and N. Singhania. Precise piecewise affine models from input-output data. In 14th ACM Intl. Conf. on Embedded Software (EMSOFT), 2014.
- D. Angluin and D. Fisman. Learning Omega Regular Languages. Algorithmic Learning Theory - 24th International Conference, ALT 2014.
- D. Broman, C. Brooks, L. Greenberg, E. A. Lee, S. Tripakis, M. Wetter, and M. Masin. Determinate Com- position of FMUs for Co-Simulation. In Proceedings of the 13th ACM IEEE International Conference on Embedded Software (EMSOFT’13), 2013.
- S. Chakraborty, D. Fremont, K. Meel, S. A. Seshia, and M. Y. Vardi. Distribution-aware sampling and weighted model counting for SAT. In AAAI 2014.
- S. Chakraborty, K.S. Meel, M.Y. Vardi. A Scalable Nearly Uniform Generator of SAT-Witnesses. In Proc. of CAV 2013.
- S. Chakraborty, K.S. Meel, M.Y. Vardi. A Scalable Approximate Model Counter. In Proc. of CP 2013.
- S. Chakraborty, K.S. Meel, M.Y. Vardi. Balancing Scalability and Uniform in SAT WItness Generator. In Proc. of DAC 2014.
- L. D'Antoni and R. Alur. Symbolic Visibly Pushdown Automata. In 26th International Conference on Computer-Aided Verification (CAV), 2014
- R. Ehlers, S. Lafortune, S. Tripakis, and M. Vardi. Bridging the gap between supervisory control and reactive synthesis: Case of full observation and centralized control. In Proceedings of the 12th International Workshop on Discrete Event Systems WODES 2014.
- R. Ehlers, S. A. Seshia, and H. Kress-Gazit. Synthesis with identifiers.In Kenneth L. McMillan and Xavier Rival, editors, VMCAI, volume 8318 of Lecture Notes in Computer Science, pages 415–433. Springer, 2014.
- R. Ehlers, U.Topcu. Resilience to Intermittent Assumption Violations in Reactive Synthesis. In 17th International Conference on Hybrid Systems: Computation and Control (HSCC 2014).
- Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider. ICE: A Robust Framework for Learning Invariants. CAV 2014: 69-87
- P. Garg, C. Löding, P. Madhusudan, and D. Neider. Learning universally quantified invariants of linear data structures. In Natasha Sharygina and Helmut Veith, editors, CAV, volume 8044 of Lecture Notes in Computer Science, pages 813–829. Springer, 2013.
- M. Lahijanian, Lydia E. Kavraki, and M. Y. Vardi. A sampling-based strategy planner for nondeterministic hybrid systems. In IEEE Conference on Robotics and Automation, 2014.
- Y. Lustig and M. Y. Vardi. Synthesis from component libraries. STTT, 15(5-6):603–618, 2013.
- S. Nain, Y. Lustig, M. Y. Vardi. Synthesis from Probabilistic Components. CoRR abs/1407.1667 (2014)
- E. Plaku, L. E. Kavraki, and M. Y. Vardi. Falsification of LTL safety properties in hybrid systems. STTT, 15(4):305–320, 2013.
- M. Raghothaman, A. Udupa. Language to Specify Syntax-Guided Synthesis Problems. CoRR abs/1405.5590 (2014)
- M. Rungger, M.J. Mazo, and P. Tabuada. Specification-guided controller synthesis for linear systems and safe linear-time temporal logic. In Proceedings of the 16th international conference on Hybrid systems: computation and control, pages 333– 342. ACM, 2013.
- M. Rungger and P. Tabuada. A symbolic approach to the design of robust cyber-physical systems. In Proceedings of the 52nd IEEE Conference on Decision and Control, 2013.
- M. Rungger and P. Tabuada. Discounting the Past in Robust Finite-State Systems. In IEEE Conference on Decision and Control, 2014.
- M. Rungger, M. Mazo Jr., P. Tabuada. Specification-guided controller synthesis for linear systems and safe linear-time temporal logic. HSCC 2013: 333-342
- M. Rungger and P. Tabuada. Abstracting and refining robustness for cyber-physical systems. In Proceedings of the 17th international conference on Hybrid systems: computation and control. ACM, 2014.
- C. Stergiou, S. Tripakis, E. Matsikoudis, and E. A. Lee. On the Verification of Timed Discrete-Event Models. In 11th International Conference on Formal Modeling and Analysis of Timed Systems – FORMATS 2013. Springer, 2013.
- P. Tabuada, Sina Y. Caliska, M. Rungger, and R. Majumdar. Towards robustness for cyber-physical systems. IEEE Transactions on Automatic Control, 2014.

- J. Galenson, P. Reames, R. Bodík, B, Hartmann, and K. Sen. Codehint: Dynamic and interactive synthesis of code snippets. In 36th International Conference on Software Engineering, ICSE 2014.
- A. Iannopollo, P. Nuzzo, S. Tripakis, and A. Sangiovanni-Vincentelli. Library-based scalable refinement checking for contractbased design. In Design, Automation and Test in Europe (DATE 2014).
- M. Persson, M. Törngren, A. Qamar, J. Westman, M. Biehl, S. Tripakis, H. Vangheluwe, and J. Denil. A Characterization of Integrated Multi-View Modeling for Embedded Systems. In Proceedings of the 13th ACM & IEEE International Conference on Embedded Software (EMSOFT’13), 2013.
- V. Preoteasa and S. Tripakis. Refinement Calculus of Reactive Systems.In Proceedings of the 14th ACM & IEEE International Conference on Embedded Software (EMSOFT’14), 2014.
- P. Nuzzo, A. Iannopollo, S. Tripakis, and A. L. Sangiovanni-Vincentelli. Are Interface Theories Equivalent to Contract Theories? In 12th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), 2014.
- J. Reineke and S. Tripakis. Basic Problems in Multi-View Modeling. In Tools and Algorithms for the Construction and Analysis of Systems – TACAS 2014, 2014.
- R. Singh, R. Singh, Z. Xu, R. Krosnick, A. Solar-Lezama. Modular Synthesis of Sketches Using Models. VMCAI 2014: 395-414
- A. Solar-Lezama. Program sketching. STTT 15(5-6): 475-495 (2013)
- E. Torlak, R. Bodík. A lightweight symbolic virtual machine for solver-aided host languages. PLDI 2014: 54.
- E. Torlak, R. Bodík. Growing solver-aided languages with rosette. Onward! 2013: 135-152
- S. Tripakis, R. Limaye, K. Ravindran, and G. Wang. On tokens and signals: Bridging the semantic gap be- tween dataflow models and hardware implementations. In International Conference on Embedded Computer Systems: Architectures, Modeling and Simulation – SAMOS XIV, 2014.
- S. Tripakis, C. Stergiou, M. Broy, and E. A. Lee. Error-Completion in Interface Theories. In International SPIN Symposium on Model Checking of Software – SPIN 2013, volume 7976 of LNCS. Springer, 2013.
- K. W. Wong, C. Finucane, H. Kress-Gazit. Provably-correct robot control with LTLMoP, OMPL and ROS. IROS 2013: 2073
- J. Zhao, S. Nagarakatte, M. M. K. Martin, S. Zdancewic: Formal verification of SSA-based optimizations for LLVM. PLDI 2013: 175-186