Unbounded-Thread Program Verification using Thread-State Equations

DOI10.1007/978-3-319-40229-1_35zbMath1475.68174OpenAlexW2490797398MaRDI QIDQ2817949

Peizun Liu, Konstantinos Athanasiou, 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

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (7)

Computing Parameterized Invariants of Parameterized Petri Nets ⋮ Unnamed Item ⋮ Directed reachability for infinite-state systems ⋮ Towards efficient verification of population protocols ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Computing parameterized invariants of parameterized Petri nets

Uses Software

• z3

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The covering and boundedness problems for vector addition systems
• Parallel program schemata
• Expand, enlarge and check: new algorithms for the coverability problem of WSTS
• Old and New Algorithms for Minimal Coverability Sets
• An SMT-Based Approach to Coverability Analysis
• All for the Price of Few
• New Search Strategies for the Petri Net CEGAR Approach
• Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with Pruning
• Well (and Better) Quasi-Ordered Transition Systems
• On the Efficient Computation of the Minimal Coverability Set for Petri Nets
• Reasoning about systems with many processes
• Applying CEGAR to the Petri Net State Equation
• Well-structured transition systems everywhere!

This page was built for publication: Unbounded-Thread Program Verification using Thread-State Equations