Towards Abstraction-Based Verification of Shape Calculus

DOI10.1016/J.ENTCS.2012.05.013MaRDI QIDQ5404093zbMATH OpenOpenAlexWikidataFDO

Authors Federico Buti, Massimo Callisto de Donato, Maria Rita Di Berardini, Emanuela Merelli, Luca Tesei, Flavio Corradini

Publication date 21 March 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2012.05.013

zbMATH Keywords

systems biologyabstract interpretationprocess algebraspatiality

Mathematics Subject Classification ID

Systems biology, networks (92C42) Computational aspects related to convexity (52B55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• scientific article; zbMATH DE number 1953039
• Shape-Value Abstraction for Verifying Linearizability
• Verification, Model Checking, and Abstract Interpretation
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• Formal verification of a geometry algorithm: a quest for abstract views and symmetry in Coq proofs
• Abstraction of object graphs in program verification
• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
• Tools and Algorithms for the Construction and Analysis of Systems
• Mind the Shapes: Abstraction Refinement Via Topology Invariants
• Automated Verification of Shape and Size Properties Via Separation Logic

Cites work

• scientific article; zbMATH DE number 7020138 (Why is no real title available?)
• scientific article; zbMATH DE number 7020139 (Why is no real title available?)
• Abstract Interpretation Frameworks
• Bone remodelling in \textsc{BioShape}
• Bone remodelling: a complex automata-based model running in BioShape

Cited in

(3)

• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• Shape-Value Abstraction for Verifying Linearizability
• Mind the Shapes: Abstraction Refinement Via Topology Invariants

Describes a project that uses

Uses Software

• BioShape

This page was built for publication: Towards Abstraction-Based Verification of Shape Calculus

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