On the combination of polyhedral abstraction and SMT-based model checking for Petri nets

DOI10.1007/978-3-030-76983-3_9zbMath1489.68150arXiv2104.09850OpenAlexW3163218045MaRDI QIDQ2117166

Nicolas Amat, Silvano Dal Zilio, Bernard Berthomieu

Publication date: 21 March 2022

Full work available at URL: https://arxiv.org/abs/2104.09850

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)

Related Items (1)

Accelerating the computation of dead and concurrent places using reductions

Uses Software

• z3
• Cubicle
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Stubborn versus structural reductions for Petri nets
• Infinite-state invariant checking with IC3 and predicate abstraction
• Understanding IC3
• An SMT-Based Approach to Coverability Analysis
• SAT-Based Model Checking without Unrolling
• Hierarchical Set Decision Diagrams and Regular Models
• Reduction
• Automatic Decomposition of Petri Nets into Automata Networks – A Synthetic Account
• Structural Reductions Revisited
• Petri Net Reductions for Counting Markings
• Model Checking Software
• Bounded model checking using satisfiability solving

This page was built for publication: On the combination of polyhedral abstraction and SMT-based model checking for Petri nets