Compositional reasoning for shared-variable concurrent programs
Scalable and automatic formal verification for concurrent systems is always demanding. In this paper, we propose a verification framework to support automated compositional reasoning for concurrent programs with shared variables. Our framework models concurrent programs as succinct automata and supp...
Saved in:
Main Authors: | ZHANG, Fuyuan, ZHAO, Yongwang, SANAN, David, LIU, Yang, TIU, Alwen, LIN, Shang-Wei, SUN, Jun |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2018
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4649 https://ink.library.smu.edu.sg/context/sis_research/article/5652/viewcontent/FM2018.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
Similar Items
-
A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic
by: LE, Xuan Bach, et al.
Published: (2022) -
A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic
by: LE, Xuan Bach, et al.
Published: (2022) -
Refinement-based specification and security analysis of separation kernels
by: Zhao, Yongwang, et al.
Published: (2020) -
A Quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic
by: Le, Xuan-Bach, et al.
Published: (2023) -
A comprehensive formal specification of ARINC 653 with conformity proof
by: FENG, Zhang, et al.
Published: (2024)