Using contracts to guide the search-based verification of concurrent programs
Search-based techniques can be used to identify whether a concurrent program exhibits faults such as race conditions, deadlocks, and starvation: a fitness function is used to guide the search to a region of the program’s state space in which these concurrency faults are more likely occur. In this sh...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | text |
| Language: | English |
| Published: |
Institutional Knowledge at Singapore Management University
2013
|
| Subjects: | |
| Online Access: | https://ink.library.smu.edu.sg/sis_research/4914 https://ink.library.smu.edu.sg/context/sis_research/article/5917/viewcontent/PoskittPoulding.SSBSE.2013.pdf |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Institution: | Singapore Management University |
| Language: | English |
| Summary: | Search-based techniques can be used to identify whether a concurrent program exhibits faults such as race conditions, deadlocks, and starvation: a fitness function is used to guide the search to a region of the program’s state space in which these concurrency faults are more likely occur. In this short paper, we propose that contracts specified by the developer as part of the program’s implementation could be used to provide additional guidance to the search. We sketch an example of how contracts might be used in this way, and outline our plans for investigating this verification approach. |
|---|