Deductive Program Repair
作者： Etienne Kneuss , Manos Koukoutos , Viktor Kuncak , None
DOI: 10.1007/978-3-319-21668-3_13
关键词:
摘要: We present an approach to program repair and its application programs with recursive functions over unbounded data types. Our formulates in the framework of deductive synthesis that uses existing structure as a hint guide synthesis. introduce new specification construct for symbolic tests. rely on such user-specified tests well automatically generated ones localize fault speed up implementation is able eliminate errors within seconds from variety functional programs, including computation code implementations structures. The resulting are formally verified by Leon system.
springer.com
core.ac.uk
croustillant.ch 参考文章(30)
Philippe Suter, Ali Sinan Köksal, Viktor Kuncak, Satisfiability modulo recursive programs static analysis symposium. ,vol. 6887, pp. 298- 315 ,(2011) , 10.1007/978-3-642-23702-7_23
Christian von Essen, Barbara Jobstmann, Program Repair without Regret Computer Aided Verification. pp. 896- 911 ,(2013) , 10.1007/978-3-642-39799-8_64
Leonardo de Moura, Nikolaj Bjørner, Z3: an efficient SMT solver tools and algorithms for construction and analysis of systems. pp. 337- 340 ,(2008) , 10.1007/978-3-540-78800-3_24
Sanjit A. Seshia, Mukund Raghothaman, Garvit Juniwal, Rajeev Alur, Rastislav Bodik, Abhishek Udupa, Milo M. K. Martin, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Syntax-guided synthesis Other univ. web domain. ,(2013)
Divya Gopinath, Muhammad Zubair Malik, Sarfraz Khurshid, Specification-based program repair using SAT tools and algorithms for construction and analysis of systems. pp. 173- 188 ,(2011) , 10.1007/978-3-642-19835-9_15
Barbara Jobstmann, Andreas Griesmayer, Roderick Bloem, Program Repair as a Game Computer Aided Verification. pp. 226- 238 ,(2005) , 10.1007/11513988_23
Roopsha Samanta, Oswaldo Olivo, E. Allen Emerson, Cost-Aware Automatic Program Repair static analysis symposium. ,vol. 8723, pp. 268- 284 ,(2014) , 10.1007/978-3-319-10936-7_17
Robert Konighofer, Roderick Bloem, Automated error localization and correction for imperative programs formal methods in computer-aided design. pp. 91- 100 ,(2011) , 10.5555/2157654.2157671
Manuel Fähndrich, Francesco Logozzo, Static Contract Checking with Abstract Interpretation Formal Verification of Object-Oriented Software. ,vol. 6528, pp. 10- 30 ,(2011) , 10.1007/978-3-642-18070-5_2
Andreas Griesmayer, Roderick Bloem, Byron Cook, Repair of Boolean Programs with an Application to C Computer Aided Verification. pp. 358- 371 ,(2006) , 10.1007/11817963_33