Back to Search
Start Over
Verification of Concurrent Programs Using Petri Net Unfoldings
- Source :
- Lecture Notes in Computer Science ISBN: 9783030670665, VMCAI
- Publication Year :
- 2021
- Publisher :
- Springer International Publishing, 2021.
-
Abstract
- Given a verification problem for a concurrent program (with a fixed number of threads) over infinite data domains, we can construct a model checking problem for an abstraction of the concurrent program through a Petri net (a problem which can be solved using McMillan’s unfoldings technique). We present a method of abstraction refinement which translates Floyd/Hoare-style proofs for sample traces into additional synchronization constraints for the Petri net.
- Subjects :
- Model checking
050101 languages & linguistics
Computer science
Programming language
Concurrency
Data domain
05 social sciences
02 engineering and technology
Construct (python library)
Petri net
Mathematical proof
computer.software_genre
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Synchronization (computer science)
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
0501 psychology and cognitive sciences
computer
Abstraction (linguistics)
Subjects
Details
- ISBN :
- 978-3-030-67066-5
- ISBNs :
- 9783030670665
- Database :
- OpenAIRE
- Journal :
- Lecture Notes in Computer Science ISBN: 9783030670665, VMCAI
- Accession number :
- edsair.doi...........9f25def55be3513e2b44c17a67cd66c9