Automated repair of heap-manipulating programs using deductive synthesis

DOI10.1007/978-3-030-67067-2_17MaRDI QIDQ2234087zbMATH OpenOpenAlexFDO

Authors Thanh-Toan Nguyen, Quang-Trung Ta, Ilya Sergey, Wei-Ngan Chin

Publication date 18 October 2021

Full work available at URL https://doi.org/10.1007/978-3-030-67067-2_17

Mathematics Subject Classification ID

Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Automatic program repair using formal verification and expression templates
• Connecting program synthesis and reachability: automatic program repair using test-input generation
• Specification-based program repair using SAT
• Sound and complete mutation-based program repair
• Program repair without regret

Cites work

• Automated mutual explicit induction proof in separation logic
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Automatic program repair using formal verification and expression templates
• BI as an assertion language for mutable data structures
• Compositional shape analysis by means of bi-abduction
• Concise read-only specifications for better synthesis of programs with pointers
• Enhancing Program Verification with Lemmas
• Enhancing modular OO verification with separation logic
• Sequent calculi for induction and infinite descent
• Specification-based program repair using SAT

Cited in

(4)

• Connecting program synthesis and reachability: automatic program repair using test-input generation
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
• Fast Automated Abstract Machine Repair Using Simultaneous Modifications and Refactoring
• Automatic program repair using formal verification and expression templates

This page was built for publication: Automated repair of heap-manipulating programs using deductive synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2234087)