Reasoning about Assignments in Recursive Data Structures

DOI10.1007/978-3-642-19829-8_11zbMath1325.68157OpenAlexW1707734666MaRDI QIDQ2999318

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

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

Uses Software

• KRAKATOA
• Eiffel
• Why3
• Caduceus
• Smallfoot

Cites Work

• Proving pointer programs in higher-order logic
• A Formalisation of Smallfoot in HOL
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Theorem Proving in Higher Order Logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Reasoning about Assignments in Recursive Data Structures