Automatic numeric abstractions for heap-manipulating programs

DOI10.1145/1706299.1706326zbMath1312.68063OpenAlexW2003383232MaRDI QIDQ5255075

No author found.

Publication date: 11 June 2015

Published in: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1706299.1706326

zbMATH Keywords

terminationabstractionshape analysisseparation logicprogram verification

Mathematics Subject Classification ID

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

Related Items (10)

Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ A generic framework for heap and value analyses of object-oriented programming languages ⋮ Verification of heap manipulating programs with ordered data by extended forest automata ⋮ Disproving Inductive Entailments in Separation Logic via Base Pair Approximation ⋮ Complexity and resource bound analysis of imperative programs using difference constraints ⋮ Counterexample Validation and Interpolation-Based Refinement for Forest Automata ⋮ Automatically verifying temporal properties of pointer programs with cyclic proof ⋮ Relational Decomposition ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification ⋮ Ranking Functions for Linear-Constraint Loops

This page was built for publication: Automatic numeric abstractions for heap-manipulating programs