Efficient verification of imperative programs using auto2

DOI10.1007/978-3-319-89960-2_2zbMath1423.68295arXiv1610.06996OpenAlexW2765411061MaRDI QIDQ2324204

Bohua Zhan

Publication date: 16 September 2019

Full work available at URL: https://arxiv.org/abs/1610.06996

Mathematics Subject Classification ID

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

Related Items (2)

Auto2_Imperative_HOL ⋮ Reasoning about block-based cloud storage systems via separation logic

Uses Software

• Dafny
• Isabelle
• Isabelle/HOL
• Why3
• VeriFast
• AUTO2
• Edmonds-Karp
• Separation Logic
• Dijkstra Shortest Path

This page was built for publication: Efficient verification of imperative programs using auto2