Publication:
Qed: a proof system based on reduction and abstraction for the static verification of concurrent software

Simple item page
dc.contributor.kuauthorElmas, Tayfun
dc.contributor.kuprofilePhD Student
dc.contributor.schoolcollegeinstituteGraduate School of Sciences and Engineering
dc.contributor.yokidN/A
dc.date.accessioned2024-11-09T22:58:02Z
dc.date.issued2010
dc.description.abstractWe 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. © 2010 ACM.
dc.description.indexedbyScopus
dc.description.openaccessYES
dc.description.publisherscopeInternational
dc.description.sponsorshipAssociation for Computing Machinery (ACM)
dc.description.sponsorshipIEEE Computer Society
dc.description.sponsorshipTechnical Council on Software Engineering (tcse)
dc.description.sponsorshipSIGSOFT
dc.description.sponsorshipComputer Society - South Africa
dc.description.volume2
dc.identifier.doi10.1145/1810295.1810454
dc.identifier.isbn9781-6055-8719-6
dc.identifier.issn0270-5257
dc.identifier.linkhttps://www.scopus.com/inward/record.uri?eid=2-s2.0-77954746890anddoi=10.1145%2f1810295.1810454andpartnerID=40andmd5=1043a43814e6e609057d8bb3eee9f487
dc.identifier.quartileN/A
dc.identifier.scopus2-s2.0-77954746890
dc.identifier.urihttp://dx.doi.org/10.1145/1810295.1810454
dc.identifier.urihttps://hdl.handle.net/20.500.14288/7657
dc.keywordsAbstraction
dc.keywordsAtomicity
dc.keywordsConcurrent programs
dc.keywordsReduction abstraction
dc.keywordsAtomic actions
dc.keywordsConcurrent program
dc.keywordsConcurrent software
dc.keywordsProof system
dc.keywordsStatic verification
dc.keywordsSupporting tool
dc.keywordsAbstracting
dc.keywordsComputer system firewalls
dc.keywordsVerification
dc.keywordsComputer software selection and evaluation
dc.languageEnglish
dc.publisherInstitute of Electrical and Electronics Engineers (IEEE)
dc.sourceProceedings - International Conference on Software Engineering
dc.subjectComputer engineering
dc.titleQed: a proof system based on reduction and abstraction for the static verification of concurrent software
dc.typeConference proceeding
dspace.entity.typePublication
local.contributor.authoridN/A
local.contributor.kuauthorElmas, Tayfun

Files

Collections

Publications without Fulltext