DocumentCode :
555855
Title :
QED: a proof system based on reduction and abstraction for the static verification of concurrent software
Author :
Elmas, Tayfun
Author_Institution :
Coll. of Eng., Koc Univ., Istanbul, Turkey
Volume :
2
fYear :
2010
fDate :
2-8 May 2010
Firstpage :
507
Lastpage :
508
Abstract :
We present a proof system and supporting tool, QED, for the static verification of concurrent software. Our key idea is to simplify the verification of a program by rewriting it with larger atomic actions. We demonstrated the simplicity and effectiveness of our approach on benchmarks with intricate synchronization.
Keywords :
concurrency control; program verification; rewriting systems; QED supporting tool; abstraction; concurrent software; program verification; proof system; rewriting; static verification; Concurrent computing; Data structures; Instruction sets; Interference; Software tools; Synchronization; abstraction; atomicity; concurrent programs; reduction;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Engineering, 2010 ACM/IEEE 32nd International Conference on
Conference_Location :
Cape Town
ISSN :
0270-5257
Print_ISBN :
978-1-60558-719-6
Type :
conf
DOI :
10.1145/1810295.1810454
Filename :
6062120
Link To Document :
https://search.ricest.ac.ir/dl/search/defaultta.aspx?DTC=49&DC=555855
بازگشت