Unbounded-thread program verification using thread-state equations

DOI10.1007/978-3-319-40229-1_35MaRDI QIDQ2817949zbMATH OpenOpenAlexFDO

Authors Konstantinos Athanasiou, Peizun Liu, Thomas Wahl

Publication date 5 September 2016

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-40229-1_35

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) 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

• Efficient coverability analysis by proof minimization
• Verification of Boolean programs with unbounded thread creation
• An SMT-based approach to coverability analysis
• Proof spaces for unbounded parallelism
• Computer Aided Verification

Cites work

• All for the price of few (parameterized verification through view abstraction)
• An SMT-based approach to coverability analysis
• Applying CEGAR to the Petri net state equation
• Expand, enlarge and check: new algorithms for the coverability problem of WSTS
• From many places to few: automatic abstraction refinement for Petri nets
• scientific article; zbMATH DE number 3688740 (Why is no real title available?)
• scientific article; zbMATH DE number 3582425 (Why is no real title available?)
• Minimal coverability set for Petri nets: Karp and Miller algorithm with pruning
• New search strategies for the Petri net CEGAR approach
• Old and new algorithms for minimal coverability sets
• On the Efficient Computation of the Minimal Coverability Set for Petri Nets
• Parallel program schemata
• Reasoning about systems with many processes
• The covering and boundedness problems for vector addition systems
• Well (and better) quasi-ordered transition systems
• Well-structured transition systems everywhere!

Cited in

(10)

• Computing parameterized invariants of parameterized Petri nets
• The decidability of verification under PS 2.0
• Directed reachability for infinite-state systems
• Verification of Boolean programs with unbounded thread creation
• Efficient coverability analysis by proof minimization
• Affine extensions of integer vector addition systems with states
• Computing Parameterized Invariants of Parameterized Petri Nets
• Affine extensions of integer vector addition systems with states
• scientific article; zbMATH DE number 7407775 (Why is no real title available?)
• Verifying Generalised and Structural Soundness of Workflow Nets via Relaxations

Describes a project that uses

Uses Software

• z3

This page was built for publication: Unbounded-thread program verification using thread-state equations

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