Rajeev Alur
Skip Abstract Section
Abstract
A promising, useful tool for future programming development environments.
- Akiba, T., Imajo, K., Iwami, H., Iwata, Y., Kataoka, T., Takahashi, N., Mmoskal, M., Swamy, N. Calibrating research in program synthesis using 72,000 hours of programmer time. Technical Report, MSR, 2013.Google Scholar
- Alur, R., Bodík, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A. Syntax-guided synthesis. In Proc. FMCAD, 2013, 1--17.Google Scholar
- Alur, R., Radhakrishna, A., Udupa, A. Scaling enumerative program synthesis via divide and conquer. In Proc. TACAS, LNCS 10205, 2017, 319--336.Google Scholar
- Clarke, E., Grumberg, O., Peled, D. Model Checking. MIT Press, 2000.Google Scholar
- de Moura, L., Bjørner, N. Satisfiability Modulo Theories: Introduction and applications. Commun. ACM 54, 9 (2011), 69--77. Google ScholarDigital Library
- Devlin, J., Uesato, J., Bhupatiraju, S., Singh, R., Mohamed, A., Kohli, P. Robustfill: Neural program learning under noisy I/O. In Proc. ICML, 2017, 990--998.Google Scholar
- Eldib, H., Wu, M., Wang, C. Synthesis of fault-attack countermeasures for cryptographic circuits. In Proc. CAV, LNCS 9780, 2016, 343--363.Google Scholar
- Garg, P., Löding, C., Madhusudan, P., Neider, D. ICE: A robust framework for learning invariants. In Proc. CAV, LNCS 8559, 2014, 69--87. Google ScholarDigital Library
- Ghalaty, N., Aysu, A., Schaumont, P. Analyzing and eliminating the causes of fault sensitivity analysis. In Proc. DATE, 2014, 1--6. Google ScholarDigital Library
- Gulwani, S. Automating string processing in spreadsheets using input--output examples. In Proc. POPL, 2011, 317--330. Google ScholarDigital Library
- Gulwani, S., Harris, W.R., Singh, R. Spreadsheet data manipulation using examples. Commun. ACM, 55, 8 (2012), 97--105. Google ScholarDigital Library
- Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R. Synthesis of loop-free programs. In Proc. PLDI, 2011, 62--73. Google ScholarDigital Library
- Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A. Oracle-guided component-based program synthesis. In Proc. ICSE, 2010, 215--224. Google ScholarDigital Library
- Kuncak, V., Mayer, M., Piskac, R., Suter, P. Software synthesis procedures. Commun. ACM, 55, 2. Google ScholarDigital Library
- Le, X.D., Chu, D., Lo, D., Le Goues, C., Visser, W. S3: Syntax- and semantic-guided repair synthesis via programming by examples. In Proc. FSE, 2017, 593--604. Google ScholarDigital Library
- Malik, S., Zhang, L. Boolean satisfiability: From theoretical hardness to practical success. Commun. ACM, 52, 8 (2009), 76--82. Google ScholarDigital Library
- Manna, Z., Waldinger, R. Fundamentals of deductive program synthesis. IEEE Trans. Softw. Eng. 18, 8 (1992), 674--704. Google ScholarDigital Library
- Massalin, H. Superoptimizer -- A look at the smallest program. In Proc. ASPLOS, 1987, 122--126. Google ScholarCross Ref
- Mechtaev, S., Yi, J., Roychoudhury, A. Angelix: Scalable multiline program patch synthesis via symbolic analysis. In Proc. ICSE, 2016, 691--701. Google ScholarDigital Library
- Mitchell, T. Machine Learning. McGraw-Hill, 1997. Google ScholarDigital Library
- Osera, P., Zdancewic, S. Type-and-example-directed program synthesis. In Proc. PLDI, 2015, 619--630. Google ScholarDigital Library
- Polikarpova, N., Kuraj, I., Solar-Lezama, A. Program synthesis from polymorphic refinement types. In Proc. PLDI, 2016, 522--538. Google ScholarDigital Library
- Quinlan, J. Introduction to decision trees. Mach. Learn. 1, 1 (1986), 81--106. Google ScholarDigital Library
- Raychev, V., Vechev, M.T., Yahav, E. Code completion with statistical language models. In Proc. PLDI, 2014, 419--428. Google ScholarDigital Library
- Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.W. Counterexample-guided quantifier instantiation for synthesis in SMT. In Proc. CAV, 2015, 198--216.Google Scholar
- Schkufza, E., Sharma, R., Aiken, A. Stochastic program optimization. Commun. ACM 59, 2 (2016), 114--122. Google ScholarDigital Library
- Seshia, S.A. Combining induction, deduction, and structure for verification and synthesis. Proc. IEEE 103, 11 (2015), 2036--2051.Google ScholarCross Ref
- Solar-Lezama, A. Program sketching. STTT 15, 5--6 (2013), 475--495. Google ScholarDigital Library
- Solar-Lezama, A., Rabbah, R., Bodík, R., Ebcioglu, K. Programming by sketching for bit-streaming programs. In Proc. PLDI, 2005, 281--294. Google ScholarDigital Library
- Srivastava, S., Gulwani, S., Foster, J.S. Template-based program verification and program synthesis. STTT 15, 5--6 (2013), 497--518. Google ScholarDigital Library
- Stump, A., Sutcliffe, G., Tinelli, C. Starexec: A cross-community infrastructure for logic solving. In Proc. IJCAR, 2014, 367--373.Google Scholar
- Udupa, A., Raghavan, A., Deshmukh, J., Mador-Haim, S., Martin, M., Alur, R. TRANSIT: Specifying protocols with concolic snippets. In Proc. PLDI, 2013, 287--296. Google ScholarDigital Library
- Warren, H.S. Hacker's Delight. Addison-Wesley, 2002. Google ScholarDigital Library
Index Terms
- Search-based program synthesis
Recommendations
Accelerating search-based program synthesis using learned probabilistic models
PLDI '18A key challenge in program synthesis concerns how to efficiently search for the desired program in the space of possible programs. We propose a general approach to accelerate search-based program synthesis by biasing the search towards likely programs. ...
From program verification to program synthesis
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesThis paper describes a novel technique for the synthesis of imperative programs. Automated program synthesis has the potential to make programming and the design of systems easier by allowing programs to be specified at a higher-level than executable ...
From program verification to program synthesis
POPL '10This paper describes a novel technique for the synthesis of imperative programs. Automated program synthesis has the potential to make programming and the design of systems easier by allowing programs to be specified at a higher-level than executable ...
Comments