Reasoning about assignments in recursive data structures

DOI10.1007/978-3-642-19829-8_11MaRDI QIDQ2999318zbMATH OpenOpenAlexFDO

Authors Alejandro Tamalet, Ken Madlener

Publication date 12 May 2011

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-19829-8_11

Mathematics Subject Classification ID

Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Scope Logic: An Extension to Hoare Logic for Pointers and Recursive Data Structures
• Automatically analyzing inductive properties for recursive data structures
• scientific article; zbMATH DE number 1841809
• Reasoning in Abella about structural operational semantics specifications
• Frame rule for mutually recursive procedures manipulating pointers

Cites work

• A Formalisation of Smallfoot in HOL
• scientific article; zbMATH DE number 1612488 (Why is no real title available?)
• scientific article; zbMATH DE number 2013592 (Why is no real title available?)
• scientific article; zbMATH DE number 1390329 (Why is no real title available?)
• scientific article; zbMATH DE number 3410595 (Why is no real title available?)
• Proving pointer programs in higher-order logic
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Theorem Proving in Higher Order Logics

Describes a project that uses

Uses Software

• Why3
• KRAKATOA
• Caduceus
• Eiffel
• Smallfoot

This page was built for publication: Reasoning about assignments in recursive data structures

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