Verifying Concurrent Systems with Symbolic Execution

DOI10.1093/LOGCOM/12.4.549MaRDI QIDQ3146300zbMATH OpenOpenAlexFDO

Authors Michael Balser, Christoph Duelli, Wolfgang Reif, Gerhard Schellhorn

Publication date 11 September 2002

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/7834bb7bb3a73da5950c52dfeb0c1f9016646d8e

zbMATH Keywords

interval temporal logictemporal formulastransition systems

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Interactive verification of concurrent systems using symbolic execution
• Verification of concurrent systems with VerCors
• Symbolic execution of concurrent systems using Petri nets
• Verifying concurrent programs against sequential specifications
• Automatic and hierarchical verification for concurrent systems
• Verification of fine-grain concurrent programs
• Verification of concurrent programs: The automata-theoretic framework

Cited in

(13)

• A verification system for concurrent programs based on the Boyer-Moore prover
• Using integer programming to verify general safety and liveness properties
• Automatic and hierarchical verification for concurrent systems
• Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
• Loop invariant symbolic execution for parallel programs
• Symbolic execution of concurrent systems using Petri nets
• PBMC: Symbolic Slicing for the Verification of Concurrent Programs
• Interactive verification of concurrent systems using symbolic execution
• scientific article; zbMATH DE number 2080057 (Why is no real title available?)
• A dynamic logic for deductive verification of multi-threaded programs
• Verifying concurrent systems with symbolic execution. Temporal reasoning is symbolic execution with a little induction.
• Simulation Refinement for Concurrency Verification
• ENFORCING CONCURRENT TEMPORAL BEHAVIORS

Describes a project that uses

Uses Software

• CoFI
• KIV

This page was built for publication: Verifying Concurrent Systems with Symbolic Execution

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