A verifiable low-level concurrent programming model based on colored Petri nets

DOI10.1007/s11432-011-4300-1zbMath1267.68078OpenAlexW2267214576MaRDI QIDQ350966

Yuan Dong, Sheng-Yuan Wang

Publication date: 3 July 2013

Published in: Science China. Information Sciences (Search for Journal in Brave)

Full work available at URL: http://engine.scichina.com/doi/10.1007/s11432-011-4300-1

zbMATH Keywords

verificationabstract machinecolored Petri netslow-level concurrent programs

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) 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)

Uses Software

• UNITY
• JFlow
• TALx86

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Resources, concurrency, and local reasoning
• Building certified libraries for PCC: dynamic storage allocation
• Stack-based typed assembly language
• Independence and concurrent separation logic
• Communicating sequential processes
• Bytecode verification on Java smart cards
• Verification of safety properties for concurrent assembly code
• Permission accounting in separation logic
• An axiomatic basis for computer programming