Verification of concurrent programs using Petri net unfoldings
DOI10.1007/978-3-030-67067-2_9zbMATH Open1472.68087OpenAlexW3121117370MaRDI QIDQ2234071FDOQ2234071
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
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
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)
Cites Work
- Inductive data flow graphs
- Thread-modular abstraction refinement.
- An improvement of McMillan's unfolding algorithm
- Software verification for weak memory via program transformation
- Verification of sequential and concurrent programs
- Thread Quantification for Concurrent Shape Analysis
- Verification of parameterized concurrent programs by modular reasoning about data and control
- Predicate abstraction and refinement for verifying multi-threaded programs
- Automated hypersafety verification
- Verification of concurrent programs using trace abstraction refinement
- Static analysis of run-time errors in embedded critical parallel C 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 Practical Approach to Verification of Mobile Systems Using Net Unfoldings
- A verifiable low-level concurrent programming model based on colored Petri nets
- 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)
