Interactive verification of concurrent systems using symbolic execution

DOI10.3233/AIC-2010-0458zbMath1205.68217OpenAlexW2123183457MaRDI QIDQ3568235

Gerhard Schellhorn, Simon Bäumler, Wolfgang Reif, Michael Balser, Florian Nafz

Publication date: 17 June 2010

Published in: AI Communications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3233/aic-2010-0458

zbMATH Keywords

temporal logiccompositional reasoningtheorem proverinteractive verification

Mathematics Subject Classification ID

Related Items (7)

An application of temporal projection to interleaving concurrency ⋮ Automated flaw detection in algebraic specifications ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ Compositional reasoning using intervals and time reversal ⋮ Proving linearizability with temporal logic ⋮ Completeness of fair ASM refinement ⋮ Formal Verification of a Lock-Free Stack with Hazard Pointers

Uses Software

• KIV

This page was built for publication: Interactive verification of concurrent systems using symbolic execution