?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=Mechanized+Verification+of+Fine-Grained+Concurrent+Programs&rft.creator=Sergey%2C+I&rft.creator=Nanevski%2C+A&rft.creator=Banerjee%2C+A&rft.description=Efficient+concurrent+programs+and+data+structures+rarely+employ+coarse-grained+synchronization+mechanisms+(i.e.%2C+locks)%3B+instead%2C+they+implement+custom+synchronization+patterns+via+fine-grained+primitives%2C+such+as+compare-and-swap.+Due+to+sophisticated+interference+scenarios+between+threads%2C+reasoning+about+such+programs+is+challenging+and+error-prone%2C+and+can+benefit+from+mechanization.+In+this+paper%2C+we+present+the+first+completely+formalized+framework+for+mechanized+verification+of+full+functional+correctness+of+fine-grained+concurrent+programs.+Our+tool+is+based+on+the+recently+proposed+program+logic+FCSL.+It+is+implemented+as+an+embedded+DSL+in+the+dependently-typed+language+of+the+Coq+proof+assistant%2C+and+is+powerful+enough+to+reason+about+programming+features+such+as+higher-order+functions+and+local+thread+spawning.+By+incorporating+a+uniform+concurrency+model%2C+based+on+state-transition+systems+and+partial+commutative+monoids%2C+FCSL+makes+it+possible+to+build+proofs+about+concurrent+libraries+in+a+thread-local%2C+compositional+way%2C+thus+facilitating+scalability+and+reuse%3A+libraries+are+verified+just+once%2C+and+their+specifications+are+used+ubiquitously+in+client-side+reasoning.+We+illustrate+the+proof+layout+in+FCSL+by+example%2C+outline+its+infrastructure%2C+and+report+on+our+experience+of+using+FCSL+to+verify+a+number+of+concurrent+algorithms+and+data+structures.&rft.subject=Compositional+program+verification%2C+concurrency%2C+separation%0D%0Alogic%2C+mechanized+proofs%2C+dependent+types&rft.publisher=ACM&rft.date=2015-06-01&rft.type=Proceedings+paper&rft.publisher=36th+ACM+SIGPLAN+Conference+on+Programming+Language+Design+and+Implementation&rft.source=+++++In%3A+++(Proceedings)+36th+ACM+SIGPLAN+Conference+on+Programming+Language+Design+and+Implementation.+(pp.+pp.+77-87).++ACM+(2015)+++++&rft.format=text&rft.identifier=https%3A%2F%2Fdiscovery.ucl.ac.uk%2Fid%2Feprint%2F10030730%2F1%2Ffcsl-pldi15.pdf&rft.identifier=https%3A%2F%2Fdiscovery.ucl.ac.uk%2Fid%2Feprint%2F10030730%2F&rft.rights=open