Fluid updates: beyond strong vs. weak updates

DOI10.1007/978-3-642-11957-6_14MaRDI QIDQ3558225zbMATH OpenOpenAlexFDO

Authors Isil Dillig, Thomas Dillig, Alex Aiken

Publication date 4 May 2010

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-11957-6_14

Mathematics Subject Classification ID

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

Recommendations

• Weak updates and separation logic
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• Points-to analysis with efficient strong updates
• Strong-separation logic
• Unified reasoning about robustness properties of symbolic-heap separation logic

Cited in

(10)

• Inferring functional properties of matrix manipulating programs by abstract interpretation
• Decision procedures for flat array properties
• Analyzing Array Manipulating Programs by Program Transformation
• Lingva: generating and proving program properties using symbol elimination
• An extension of lazy abstraction with interpolation for programs with arrays
• Generic abstraction of dictionaries and arrays
• From invariant checking to invariant inference using randomized search
• Proving safety with trace automata and bounded model checking
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• An array content static analysis based on non-contiguous partitions

Describes a project that uses

Uses Software

• SLAM
• Coreutils
• SPEED

This page was built for publication: Fluid updates: beyond strong vs. weak updates

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