Automatically analyzing inductive properties for recursive data structures

DOI10.13328/J.CNKI.JOS.005467MaRDI QIDQ4624672zbMATH OpenFDO

Authors Zhenhao Tang, Bin Li, Juan Zhai, Jian-hua Zhao

Publication date 22 February 2019

Full work available at URL https://doi.org/10.13328/J.CNKI.JOS.005467

zbMATH Keywords

program analysisrecursive data structuresinterprocedural analysisHoare-style program verificationinductive properties

Mathematics Subject Classification ID

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

Recommendations

• Static Analysis
• Pattern-based verification of programs with extended linear linked data structures
• Reasoning about heap manipulating programs using automata techniques
• Automatic inference of heap properties exploiting value domains
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic

Cited in

(4)

• Recursive proofs for inductive tree data-structures
• Automatic visualization of recursion trees: a case study on generic programming
• Reasoning about assignments in recursive data structures
• scientific article; zbMATH DE number 2090862 (Why is no real title available?)

This page was built for publication: Automatically analyzing inductive properties for recursive data structures

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