Interactive verification of concurrent systems using symbolic execution

DOI10.3233/AIC-2010-0458MaRDI QIDQ3568235zbMATH OpenOpenAlexFDO

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

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

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

Recommendations

• Verifying Concurrent Systems with Symbolic Execution
• scientific article; zbMATH DE number 1324660
• Symbolic execution of concurrent systems using Petri nets
• Verification of concurrent systems with VerCors
• Verifying concurrent systems with symbolic execution. Temporal reasoning is symbolic execution with a little induction.
• Automatic and hierarchical verification for concurrent systems

Cited in

(11)

• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Proving linearizability with temporal logic
• Completeness of fair ASM refinement
• PBMC: Symbolic Slicing for the Verification of Concurrent Programs
• Verifying Concurrent Systems with Symbolic Execution
• Formal verification of a lock-free stack with hazard pointers
• Verifying concurrent systems with symbolic execution. Temporal reasoning is symbolic execution with a little induction.
• Compositional reasoning using intervals and time reversal
• Automated flaw detection in algebraic specifications
• An application of temporal projection to interleaving concurrency
• Loop invariant symbolic execution for parallel programs

Describes a project that uses

Uses Software

• KIV

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

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