Verification of concurrent programs using Petri net unfoldings

DOI10.1007/978-3-030-67067-2_9MaRDI QIDQ2234071zbMATH OpenOpenAlexFDO

Authors Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Mehdi Naouar, Andreas Podelski, Claus Schätzle

Publication date 18 October 2021

Full work available at URL https://doi.org/10.1007/978-3-030-67067-2_9

zbMATH Keywords

verificationconcurrencyPetri netsunfoldings

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Construction and SAT-based verification of contextual unfoldings
• A verifiable low-level concurrent programming model based on colored Petri nets
• scientific article; zbMATH DE number 1670797
• Verification of bounded Petri nets using integer programming
• Program verification: state of the art, problems, and results. I

Cites work

• An improvement of McMillan's unfolding algorithm
• Automated hypersafety verification
• Inductive data flow graphs
• Predicate abstraction and refinement for verifying multi-threaded programs
• Software verification for weak memory via program transformation
• Static analysis of run-time errors in embedded critical parallel C programs
• Thread Quantification for Concurrent Shape Analysis
• Thread-modular abstraction refinement.
• Verification of concurrent programs using trace abstraction refinement
• Verification of parameterized concurrent programs by modular reasoning about data and control
• Verification of sequential and concurrent programs

Cited in

(14)

• Concurrent program verification with invariant-guided underapproximation
• Verification of concurrent programs using trace abstraction refinement
• A practical approach to verification of mobile systems using net unfolding
• An abstraction technique for describing concurrent program behaviour
• Experimenting Formal Proofs of Petri Nets Refinements
• Verification of bounded Petri nets using integer programming
• Abstract interpretation with unfoldings
• Causal Dataflow Analysis for Concurrent Programs
• Program Development in Computational Logic
• A verifiable low-level concurrent programming model based on colored Petri nets
• A Practical Approach to Verification of Mobile Systems Using Net Unfoldings
• Verifying parallel algorithms and programs using coloured Petri nets
• Verification of higher-order concurrent programs with dynamic resource creation
• Constraint-based automatic verification of abstract models of multithreaded programs

This page was built for publication: Verification of concurrent programs using Petri net unfoldings

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