Article(id=1241719226717762296, tenantId=1146029695717560320, journalId=1146032081894723586, issueId=1241719216169079576, articleNumber=null, orderNo=4, doi=10.3981/j.issn.2097-0781.2023.01.003, pmid=null, cstr=null, oa=null, hot=null, price=null, onlineType=0, articleFormat=0, articleType=null, articleTypeStr=research-article, receivedDate=1672934400000, receivedDateStr=2023-01-06, revisedDate=1675872000000, revisedDateStr=2023-02-09, acceptedDate=null, acceptedDateStr=null, onlineDate=1679587200000, onlineDateStr=2023-03-24, pubDate=1679241600000, pubDateStr=2023-03-20, doiRegisterDate=null, doiRegisterDateStr=null, onlineIssueDate=1679587200000, onlineIssueDateStr=2023-03-24, onlineJustAcceptDate=null, onlineJustAcceptDateStr=null, onlineFirstDate=null, onlineFirstDateStr=null, sourceXml=null, magXml=null, createTime=1773978533676, creator=sys-migrate, updateTime=1773978533676, updator=sys-migrate, issue=Issue{id=1241719216169079576, tenantId=1146029695717560320, journalId=1146032081894723586, year='2023', volume='2', issue='1', pageStart='5', pageEnd='143', issueExtLink='null', onlineDate='null', pubDate='null', beforeIssueId=null, nextIssueId=null, price=null, status=1, issueComplete=1, articleOrder=1, issueType=-1, specialIssue=1, createTime=1773978531159, creator=sys-migrate, updateTime=1774001248771, updator=13041195026, preIssue=null, nextIssue=null, ext={EN=IssueExt(id=1241814500781916967, tenantId=1146029695717560320, journalId=1146032081894723586, issueId=1241719216169079576, language=EN, specialIssueTitle=Science and Technology Foresight, coverIllustrator=null, specialIssueEditor=null, specialIssueAbout=null), CN=IssueExt(id=1241814500781916968, tenantId=1146029695717560320, journalId=1146032081894723586, issueId=1241719216169079576, language=CN, specialIssueTitle=形式化方法与复杂计算系统可信保障, coverIllustrator=null, specialIssueEditor=null, specialIssueAbout=null)}, issueFiles=null}, startPage=33, endPage=45, ext={EN=ArticleExt(id=1241719230249358118, articleId=1241719226717762296, tenantId=1146029695717560320, journalId=1146032081894723586, language=EN, title=Formal Methods and System Software: Practice and Suggestions, columnId=1149656489310208610, journalTitle=Science and Technology Foresight, columnName=Review and Commentary, runingTitle=null, highlight=null, articleAbstract=
The growing need for highly reliable system software has drawn widespread interest in formal methods in the industry. This paper presents an overview of the mainstream formal methods and analyzes the current research status in this regard. Then, it describes the application of formal methods in the design and implementation of operating systems, compilers, synchronization primitives, file systems, database systems, and distributed consensus protocols. On this basis, it summarizes the experience learned in applying formal methods to system software and discusses potential challenges from the theoretical and engineering aspects. Finally, it gives some suggestions on how to address these challenges.
, correspAuthors=Haibo CHEN, authorNote=null, correspAuthorsNote=
†
, copyrightStatement=null, copyrightOwner=null, extLink=null, articleAbsUrl=null, sourceXml=null, magXml=null, pdfUrl=null, pdf=null, pdfFileSize=null, pdfExtLink=null, richHtmlUrl=null, mobilePdfUrl=null, reviewReport=null, pdfFirstPage=null, abstractGraph=null, abstractGraphContent=null, abstractVideo=null, citation=null, cebUrl=null, magXmlContent=null, mapNumber=null, authorCompany=null, fund=null, authors=null, authorsList=Haoran DING, Zhaoguo WANG, Ming FU, Haibo CHEN), CN=ArticleExt(id=1241719230089982722, articleId=1241719226717762296, tenantId=1146029695717560320, journalId=1146032081894723586, language=CN, title=形式化方法与系统软件：实践与发展建议, columnId=1148708266483446458, journalTitle=前瞻科技, columnName=综述与述评, runingTitle=null, highlight=null, articleAbstract=
对高可靠系统软件需求的不断增加使得形式化方法在工业界引起了广泛的兴趣。文章概述了当前主流形式化方法，分析了国内外研究态势，并介绍了形式化方法在设计和实现操作系统、编译器、同步原语、文件系统、数据库系统和分布式共识协议等方面的实践。基于这些实践，进一步总结了形式化方法在系统软件中应用的经验，并从理论和工程两方面讨论其可能面临的挑战，最后针对这些挑战提出发展建议。
, correspAuthors=陈海波, authorNote=null, correspAuthorsNote=
†
, copyrightStatement=null, copyrightOwner=null, extLink=null, articleAbsUrl=null, sourceXml=g5qLBxxp75NhUHGMy3fhtg==, magXml=Xhb//2dwDDFzWecOk6Qsvw==, pdfUrl=null, pdf=czGWYl9OcI2ralLRlZV4Sg==, pdfFileSize=2505933, pdfExtLink=null, richHtmlUrl=null, mobilePdfUrl=null, reviewReport=null, pdfFirstPage=null, abstractGraph=UT3j8+N+uznLytGTjaXk6w==, abstractGraphContent=null, abstractVideo=null, citation=null, cebUrl=null, magXmlContent=N9jN6TFJhIksvNz9v6vTtA==, mapNumber=null, authorCompany=null, fund=null, authors=
 |
丁浩然，博士研究生。研究方向为基于形式化方法的系统软件验证与优化。参与设计和实现了世界上第1个形式化验证过的细粒度并发内存文件系统AtomFS、自动生成并验证SQL优化规则的工具WeTune等，相关成果发表在中国计算机学会推荐的系统和数据库领域A类国际顶级会议SOSP和SIGMOD。电子信箱：nhaorand@sjtu.edu.cn。 |
 |
陈海波，上海交通大学特聘教授，博士研究生导师。上海交通大学并行与分布式系统研究所所长，领域操作系统教育部工程研究中心主任。中国计算机学会系统软件专业委员会副主任，OpenHarmony技术指导委员会创始主席，国际计算机学会（ACM）旗舰杂志Communications of the ACM首位中国学者编委与领域共同主席。国家杰出青年科学基金获得者，国际电气与电子工程师协会（IEEE）会士，ACM杰出科学家。主要研究领域为操作系统、分布式系统与形式化方法。研究成果通过产学研深度结合被应用到数十亿设备，产生了广泛的学术与产业影响。获陈嘉庚青年科学奖、教育部技术发明奖一等奖、中国青年科技奖、全国优秀博士学位论文奖及华为卓越贡献个人奖，ASPLOS、EuroSys、VEE等最佳论文奖，DSN时间检验奖，SIGMOD研究亮点奖等。主持撰写的《现代操作系统：原理与实现》获得2020年度“最受读者喜爱的IT图书奖”。电子信箱：haibochen@sjtu.edu.cn。 |
, authorsList=丁浩然, 王肇国, 付明, 陈海波)}, authors=[Author(id=1241719253976535910, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, orderNo=0, firstName=null, middleName=null, lastName=null, nameCn=null, orcid=null, stid=null, country=null, authorPic=null, dead=0, email=nhaorand@sjtu.edu.cn, emailSecond=null, emailThird=null, correspondingAuthor=0, authorType=1, ext={EN=AuthorExt(id=1241719254052033385, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, authorId=1241719253976535910, language=EN, stringName=Haoran DING, firstName=Haoran, middleName=null, lastName=DING, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
1, address=1. School of Software, Shanghai Jiao Tong University, Shanghai 200240, China, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null), CN=AuthorExt(id=1241719254106559339, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, authorId=1241719253976535910, language=CN, stringName=丁浩然, firstName=null, middleName=null, lastName=null, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
1, address=1.上海交通大学软件学院，上海 200240, bio={"img":"blZrWKKkECkt7bRTnEO3Bg==","content":"
丁浩然，博士研究生。研究方向为基于形式化方法的系统软件验证与优化。参与设计和实现了世界上第1个形式化验证过的细粒度并发内存文件系统AtomFS、自动生成并验证SQL优化规则的工具WeTune等，相关成果发表在中国计算机学会推荐的系统和数据库领域A类国际顶级会议SOSP和SIGMOD。电子信箱：nhaorand@sjtu.edu.cn。
"}, bioImg=blZrWKKkECkt7bRTnEO3Bg==, bioContent=
丁浩然，博士研究生。研究方向为基于形式化方法的系统软件验证与优化。参与设计和实现了世界上第1个形式化验证过的细粒度并发内存文件系统AtomFS、自动生成并验证SQL优化规则的工具WeTune等，相关成果发表在中国计算机学会推荐的系统和数据库领域A类国际顶级会议SOSP和SIGMOD。电子信箱：nhaorand@sjtu.edu.cn。
, aboutCorrespAuthor=null)}, companyList=[AuthorCompany(id=1241719253846512476, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, xref=null, ext=[AuthorCompanyExt(id=1241719253850706781, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, companyId=1241719253846512476, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1. School of Software, Shanghai Jiao Tong University, Shanghai 200240, China), AuthorCompanyExt(id=1241719253859095390, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, companyId=1241719253846512476, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1.上海交通大学软件学院，上海 200240)])]), Author(id=1241719255582954350, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, orderNo=1, firstName=null, middleName=null, lastName=null, nameCn=null, orcid=null, stid=null, country=null, authorPic=null, dead=0, email=null, emailSecond=null, emailThird=null, correspondingAuthor=0, authorType=1, ext={EN=AuthorExt(id=1241719255671034736, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, authorId=1241719255582954350, language=EN, stringName=Zhaoguo WANG, firstName=Zhaoguo, middleName=null, lastName=WANG, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
1, address=1. School of Software, Shanghai Jiao Tong University, Shanghai 200240, China, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null), CN=AuthorExt(id=1241719255754920817, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, authorId=1241719255582954350, language=CN, stringName=王肇国, firstName=null, middleName=null, lastName=null, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
1, address=1.上海交通大学软件学院，上海 200240, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null)}, companyList=[AuthorCompany(id=1241719253846512476, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, xref=null, ext=[AuthorCompanyExt(id=1241719253850706781, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, companyId=1241719253846512476, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1. School of Software, Shanghai Jiao Tong University, Shanghai 200240, China), AuthorCompanyExt(id=1241719253859095390, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, companyId=1241719253846512476, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1.上海交通大学软件学院，上海 200240)])]), Author(id=1241719255838806902, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, orderNo=2, firstName=null, middleName=null, lastName=null, nameCn=null, orcid=null, stid=null, country=null, authorPic=null, dead=0, email=null, emailSecond=null, emailThird=null, correspondingAuthor=0, authorType=1, ext={EN=AuthorExt(id=1241719255914304377, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, authorId=1241719255838806902, language=EN, stringName=Ming FU, firstName=Ming, middleName=null, lastName=FU, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
2, address=2. Huawei Dresden Research Center, Dresden 01069, Germany, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null), CN=AuthorExt(id=1241719255981413243, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, authorId=1241719255838806902, language=CN, stringName=付明, firstName=null, middleName=null, lastName=null, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
2, address=2.华为德累斯顿研究所，德国德累斯顿 01069, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null)}, companyList=[AuthorCompany(id=1241719253909427040, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, xref=null, ext=[AuthorCompanyExt(id=1241719253917815649, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, companyId=1241719253909427040, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=2. Huawei Dresden Research Center, Dresden 01069, Germany), AuthorCompanyExt(id=1241719253922009954, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, companyId=1241719253909427040, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=2.华为德累斯顿研究所，德国德累斯顿 01069)])]), Author(id=1241719256052716415, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, orderNo=3, firstName=null, middleName=null, lastName=null, nameCn=null, orcid=null, stid=null, country=null, authorPic=null, dead=0, email=haibochen@sjtu.edu.cn, emailSecond=null, emailThird=null, correspondingAuthor=1, authorType=1, ext={EN=AuthorExt(id=1241719256140796802, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, authorId=1241719256052716415, language=EN, stringName=Haibo CHEN, firstName=Haibo, middleName=null, lastName=CHEN, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
1, †, address=1. School of Software, Shanghai Jiao Tong University, Shanghai 200240, China, bio=null, bioImg=null, bioContent=null, aboutCorrespAuthor=null), CN=AuthorExt(id=1241719256216294276, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, authorId=1241719256052716415, language=CN, stringName=陈海波, firstName=null, middleName=null, lastName=null, prefix=null, suffix=null, authorComment=null, nameInitials=null, affiliation=null, department=null, xref=
1, †, address=1.上海交通大学软件学院，上海 200240, bio={"img":"Xaido4GOZFk4GqLJ2wVPUA==","content":"
陈海波，上海交通大学特聘教授，博士研究生导师。上海交通大学并行与分布式系统研究所所长，领域操作系统教育部工程研究中心主任。中国计算机学会系统软件专业委员会副主任，OpenHarmony技术指导委员会创始主席，国际计算机学会（ACM）旗舰杂志Communications of the ACM首位中国学者编委与领域共同主席。国家杰出青年科学基金获得者，国际电气与电子工程师协会（IEEE）会士，ACM杰出科学家。主要研究领域为操作系统、分布式系统与形式化方法。研究成果通过产学研深度结合被应用到数十亿设备，产生了广泛的学术与产业影响。获陈嘉庚青年科学奖、教育部技术发明奖一等奖、中国青年科技奖、全国优秀博士学位论文奖及华为卓越贡献个人奖，ASPLOS、EuroSys、VEE等最佳论文奖，DSN时间检验奖，SIGMOD研究亮点奖等。主持撰写的《现代操作系统：原理与实现》获得2020年度“最受读者喜爱的IT图书奖”。电子信箱：haibochen@sjtu.edu.cn。
"}, bioImg=Xaido4GOZFk4GqLJ2wVPUA==, bioContent=
陈海波，上海交通大学特聘教授，博士研究生导师。上海交通大学并行与分布式系统研究所所长，领域操作系统教育部工程研究中心主任。中国计算机学会系统软件专业委员会副主任，OpenHarmony技术指导委员会创始主席，国际计算机学会（ACM）旗舰杂志Communications of the ACM首位中国学者编委与领域共同主席。国家杰出青年科学基金获得者，国际电气与电子工程师协会（IEEE）会士，ACM杰出科学家。主要研究领域为操作系统、分布式系统与形式化方法。研究成果通过产学研深度结合被应用到数十亿设备，产生了广泛的学术与产业影响。获陈嘉庚青年科学奖、教育部技术发明奖一等奖、中国青年科技奖、全国优秀博士学位论文奖及华为卓越贡献个人奖，ASPLOS、EuroSys、VEE等最佳论文奖，DSN时间检验奖，SIGMOD研究亮点奖等。主持撰写的《现代操作系统：原理与实现》获得2020年度“最受读者喜爱的IT图书奖”。电子信箱：haibochen@sjtu.edu.cn。
, aboutCorrespAuthor=null)}, companyList=[AuthorCompany(id=1241719253846512476, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, xref=null, ext=[AuthorCompanyExt(id=1241719253850706781, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, companyId=1241719253846512476, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1. School of Software, Shanghai Jiao Tong University, Shanghai 200240, China), AuthorCompanyExt(id=1241719253859095390, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, companyId=1241719253846512476, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1.上海交通大学软件学院，上海 200240)])])], keywords=[Keyword(id=1241719256384066438, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=EN, orderNo=1, keyword=formal methods), Keyword(id=1241719256455369608, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=EN, orderNo=2, keyword=operating systems), Keyword(id=1241719256535061386, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=EN, orderNo=3, keyword=database), Keyword(id=1241719256597975948, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=EN, orderNo=4, keyword=file systems), Keyword(id=1241719256702833550, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=EN, orderNo=5, keyword=distributed consensus protocols), Keyword(id=1241719256790913936, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=CN, orderNo=1, keyword=形式化方法), Keyword(id=1241719256849634193, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=CN, orderNo=2, keyword=操作系统), Keyword(id=1241719256920937363, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=CN, orderNo=3, keyword=数据库), Keyword(id=1241719257009017749, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=CN, orderNo=4, keyword=文件系统), Keyword(id=1241719257084515222, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=CN, orderNo=5, keyword=分布式共识协议)], refs=[Reference(id=1241719258103731117, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2019, volume=30, issue=1, pageStart=33, pageEnd=61, url=null, language=null, rfNumber=[1], rfOrder=0, authorNames=王戟, 詹乃军, 冯新宇, journalName=软件学报, refType=null, unstructuredReference=王戟, 詹乃军, 冯新宇, 等. 形式化方法概貌[J].
软件学报,
2019,
30(1): 33-61., articleTitle=形式化方法概貌, refAbstract=null), Reference(id=1241719258196005808, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2009, volume=null, issue=null, pageStart=207, pageEnd=220, url=null, language=null, rfNumber=[2], rfOrder=1, authorNames=Klein G, Elphinstone K, Heiser G, journalName=Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, refType=null, unstructuredReference=
Klein G,
Elphinstone K,
Heiser G, et al. seL4: Formal verification of an OS kernel[C]//
Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. New York: ACM Press,
2009: 207-220., articleTitle=seL4: Formal verification of an OS kernel, refAbstract=null), Reference(id=1241719258279891890, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2017, volume=null, issue=null, pageStart=252, pageEnd=269, url=null, language=null, rfNumber=[3], rfOrder=2, authorNames=Luke N, Sigurbjarnarson H, Zhang K Y, journalName=Proceedings of the 26th Symposium on Operating Systems Principles, refType=null, unstructuredReference=
Luke N,
Sigurbjarnarson H,
Zhang K Y, et al. Hyperkernel: Push-button verification of an OS kernel[C]//
Proceedings of the 26th Symposium on Operating Systems Principles. New York: ACM Press,
2017:252-269., articleTitle=Hyperkernel: Push-button verification of an OS kernel, refAbstract=null), Reference(id=1241719258342806452, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2002, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[4], rfOrder=3, authorNames=Nipkow T, Paulson L C, Wenzel M, journalName=Berlin, refType=null, unstructuredReference=
Nipkow T,
Paulson L C,
Wenzel M. Isabelle/HOL: A proof assistant for higher-order logic[M].
Berlin, Heidelberg: Springer,
2002., articleTitle=Isabelle/HOL: A proof assistant for higher-order logic, refAbstract=null), Reference(id=1241719258426692534, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2021, volume=null, issue=null, pageStart=427, pageEnd=440, url=null, language=null, rfNumber=[5], rfOrder=4, authorNames=Kokologiannakis M, Vafeiadis V, journalName=Silva A, Leino K R M. Proceedings of the 33rd International Conference on Computer Aided Verification. Berlin, refType=null, unstructuredReference=
Kokologiannakis M,
Vafeiadis V. GenMC: A model checker for weak memory models[C]//
Silva A, Leino K R M. Proceedings of the 33rd International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer,
2021: 427-440., articleTitle=GenMC: A model checker for weak memory models, refAbstract=null), Reference(id=1241719258493801400, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=1982, volume=null, issue=null, pageStart=337, pageEnd=351, url=null, language=null, rfNumber=[6], rfOrder=5, authorNames=Queille J P, Sifakis J, journalName=Goos G, Hartmains J.Proceedings of the 5th International Symposium on Programming. Berlin, refType=null, unstructuredReference=
Queille J P,
Sifakis J. Specification and verification of concurrent systems in CESAR[C]//
Goos G, Hartmains J.Proceedings of the 5th International Symposium on Programming. Berlin, Heidelberg: Springer,
1982: 337-351., articleTitle=Specification and verification of concurrent systems in CESAR, refAbstract=null), Reference(id=1241719258569298874, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2021, volume=null, issue=null, pageStart=851, pageEnd=865, url=null, language=null, rfNumber=[7], rfOrder=6, authorNames=de Lima Chehab R L, Paolillo A, Behrens D, journalName=Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles, refType=null, unstructuredReference=
de Lima Chehab R L,
Paolillo A,
Behrens D, et al. CLoF: A compositional lock framework for multi-level NUMA systems[C]//
Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles. New York: ACM Press,
2021: 851-865., articleTitle=CLoF: A compositional lock framework for multi-level NUMA systems, refAbstract=null), Reference(id=1241719258678350779, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2015, volume=null, issue=null, pageStart=18, pageEnd=37, url=null, language=null, rfNumber=[8], rfOrder=7, authorNames=Chen H G, Ziegler D, Chajed T, journalName=Proceedings of the 25th Symposium on Operating Systems Principles, refType=null, unstructuredReference=
Chen H G,
Ziegler D,
Chajed T, et al. Using Crash Hoare logic for certifying the FSCQ file system[C]//
Proceedings of the 25th Symposium on Operating Systems Principles. New York: ACM Press,
2015: 18-37., articleTitle=Using Crash Hoare logic for certifying the FSCQ file system, refAbstract=null), Reference(id=1241719260121191356, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2016, volume=null, issue=null, pageStart=59, pageEnd=79, url=null, language=null, rfNumber=[9], rfOrder=8, authorNames=Xu F W, Fu M, Feng X Y, journalName=Chaudhuri S, Farzar A.Proceedings of the 28th International Conference on Computer Aided Verification. Berlin, refType=null, unstructuredReference=
Xu F W,
Fu M,
Feng X Y, et al. A practical verification framework for preemptive OS kernels[C]//
Chaudhuri S, Farzar A.Proceedings of the 28th International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer,
2016: 59-79., articleTitle=A practical verification framework for preemptive OS kernels, refAbstract=null), Reference(id=1241719260192494526, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=259, pageEnd=274, url=null, language=null, rfNumber=[10], rfOrder=9, authorNames=Zou M, Ding H R, Du D, journalName=Proceedings of the 27th ACM Symposium on Operating Systems Principles, refType=null, unstructuredReference=
Zou M,
Ding H R,
Du D, et al. Using concurrent relational logic with helpers for verifying the AtomFS file system[C]//
Proceedings of the 27th ACM Symposium on Operating Systems Principles. New York: ACM Press,
2019: 259-274., articleTitle=Using concurrent relational logic with helpers for verifying the AtomFS file system, refAbstract=null), Reference(id=1241719260259603392, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2016, volume=null, issue=null, pageStart=653, pageEnd=669, url=null, language=null, rfNumber=[11], rfOrder=10, authorNames=Gu R H, Shao Z, Chen H, journalName=Proceedings of the 12th USENIX conference on Operating Systems Design and Implementation, refType=null, unstructuredReference=
Gu R H,
Shao Z,
Chen H, et al. CertiKOS: An extensible architecture for building certified concurrent OS kernels[C]//
Proceedings of the 12th USENIX conference on Operating Systems Design and Implementation. New York: ACM Press,
2016: 653-669., articleTitle=CertiKOS: An extensible architecture for building certified concurrent OS kernels, refAbstract=null), Reference(id=1241719260318323650, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2022, volume=null, issue=null, pageStart=465, pageEnd=484, url=null, language=null, rfNumber=[12], rfOrder=11, authorNames=Li X, Li X, Dall C, journalName=Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, refType=null, unstructuredReference=
Li X,
Li X,
Dall C, et al. Design and verification of the arm confidential compute architecture[C]//
Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation. New York: ACM Press,
2022: 465-484., articleTitle=Design and verification of the arm confidential compute architecture, refAbstract=null), Reference(id=1241719260393821124, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2021, volume=null, issue=null, pageStart=423, pageEnd=439, url=null, language=null, rfNumber=[13], rfOrder=12, authorNames=Chajed T, Tassarotti J, Theng M, journalName=Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation, refType=null, unstructuredReference=
Chajed T,
Tassarotti J,
Theng M, et al. GoJournal: A verified, concurrent, crash-safe journaling system[C]//
Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation. New York: ACM Press,
2021: 423-439., articleTitle=GoJournal: A verified, concurrent, crash-safe journaling system, refAbstract=null), Reference(id=1241719260477707206, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=111, pageEnd=125, url=null, language=null, rfNumber=[14], rfOrder=13, authorNames=Jiang H R, Liang H J, Xiao S Y, journalName=Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, refType=null, unstructuredReference=
Jiang H R,
Liang H J,
Xiao S Y, et al. Towards certified separate compilation for concurrent programs[C]//
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM Press,
2019: 111-125., articleTitle=Towards certified separate compilation for concurrent programs, refAbstract=null), Reference(id=1241719260557398984, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2015, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[15], rfOrder=14, authorNames=Hawblitzel C, Howell J, Kapritsos M, journalName=Proceedings of the 25th Symposium on Operating Systems Principles, refType=null, unstructuredReference=
Hawblitzel C,
Howell J,
Kapritsos M, et al. IronFleet: Proving practical distributed systems correct[C]//
Proceedings of the 25th Symposium on Operating Systems Principles. New York: ACM Press,
2015, doi: 10.1145/2815400.2815428., articleTitle=IronFleet: Proving practical distributed systems correct, refAbstract=null), Reference(id=1241719260645479370, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2017, volume=null, issue=null, pageStart=917, pageEnd=934, url=null, language=null, rfNumber=[16], rfOrder=15, authorNames=Bond B, Hawblitzel C, Kapritsos M, journalName=Proceedings of the 26th USENIX Conference on Security Symposium, refType=null, unstructuredReference=
Bond B,
Hawblitzel C,
Kapritsos M, et al. Vale: Verifying high-performance cryptographic assembly code[C]//
Proceedings of the 26th USENIX Conference on Security Symposium. New York: ACM Press,
2017: 917-934., articleTitle=Vale: Verifying high-performance cryptographic assembly code, refAbstract=null), Reference(id=1241719260733559756, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2020, volume=null, issue=null, pageStart=197, pageEnd=210, url=null, language=null, rfNumber=[17], rfOrder=16, authorNames=Lorch J R, Chen Y X, Kapritsos M, journalName=Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, refType=null, unstructuredReference=
Lorch J R,
Chen Y X,
Kapritsos M, et al. Armada: Low-effort verification of high-performance concurrent programs[C]//
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM Press,
2020: 197-210., articleTitle=Armada: Low-effort verification of high-performance concurrent programs, refAbstract=null), Reference(id=1241719260796474318, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2020, volume=null, issue=null, pageStart=99, pageEnd=115, url=null, language=null, rfNumber=[18], rfOrder=17, authorNames=Hance T, Lattuada A, Hawblitzel C, journalName=Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation, refType=null, unstructuredReference=
Hance T,
Lattuada A,
Hawblitzel C, et al. Storage systems are distributed systems (so verify them that way!)[C]//
Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation. New York: ACM Press,
2020: 99-115., articleTitle=Storage systems are distributed systems (so verify them that way!), refAbstract=null), Reference(id=1241719260867777488, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2022, volume=null, issue=null, pageStart=447, pageEnd=463, url=null, language=null, rfNumber=[19], rfOrder=18, authorNames=Chajed T, Tassarotti J, Theng M, journalName=Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, refType=null, unstructuredReference=
Chajed T,
Tassarotti J,
Theng M, et al. Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning[C]//
Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation. New York: ACM Press,
2022: 447-463., articleTitle=Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning, refAbstract=null), Reference(id=1241719260926497746, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2010, volume=null, issue=null, pageStart=348, pageEnd=370, url=null, language=null, rfNumber=[20], rfOrder=19, authorNames=Leino K R M, journalName=Clarke E M,Voronkov A. Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Berlin, refType=null, unstructuredReference=
Leino K R M. Dafny: An automatic program verifier for functional correctness[C]//
Clarke E M,Voronkov A. Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Berlin, Heidelberg: Springer,
2010: 348-370., articleTitle=Dafny: An automatic program verifier for functional correctness, refAbstract=null), Reference(id=1241719260989412308, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2008, volume=null, issue=null, pageStart=337, pageEnd=340, url=null, language=null, rfNumber=[21], rfOrder=20, authorNames=de Moura L, Bjørner N, journalName=Ramakrishnan C R, Rehof J. Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, refType=null, unstructuredReference=
de Moura L,
Bjørner N. Z3: An efficient SMT solver[C]//
Ramakrishnan C R, Rehof J. Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer,
2008: 337-340., articleTitle=Z3: An efficient SMT solver, refAbstract=null), Reference(id=1241719261056521174, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2016, volume=null, issue=null, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[22], rfOrder=21, authorNames=Sigurbjarnarson H, Bornholt J, Torlak E, journalName=Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation, refType=null, unstructuredReference=
Sigurbjarnarson H,
Bornholt J,
Torlak E, et al. Push-button verification of file systems via crash refinement[C]//
Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation. New York: ACM Press,
2016, doi: 10.5555/3026877.3026879., articleTitle=Push-button verification of file systems via crash refinement, refAbstract=null), Reference(id=1241719261119435736, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2020, volume=null, issue=null, pageStart=41, pageEnd=61, url=null, language=null, rfNumber=[23], rfOrder=22, authorNames=Nelson L, van Geffen J, Torlak E, journalName=Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation, refType=null, unstructuredReference=
Nelson L,
van Geffen J,
Torlak E, et al. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel[C]//
Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation. New York: ACM Press,
2020: 41-61., articleTitle=Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel, refAbstract=null), Reference(id=1241719261182350298, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2022, volume=null, issue=null, pageStart=485, pageEnd=501, url=null, language=null, rfNumber=[24], rfOrder=23, authorNames=Yao J, Tao R, Gu R, journalName=Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, refType=null, unstructuredReference=
Yao J,
Tao R,
Gu R, et al. DuoAI:Fast, Automated inference of inductive invariants for verifying distributed protocols[C]//
Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation. New York: ACM Press,
2022: 485-501., articleTitle=DuoAI:Fast, Automated inference of inductive invariants for verifying distributed protocols, refAbstract=null), Reference(id=1241719261241070556, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2013, volume=null, issue=null, pageStart=135, pageEnd=152, url=null, language=null, rfNumber=[25], rfOrder=24, authorNames=Torlak E, Bodik R, journalName=Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, refType=null, unstructuredReference=
Torlak E,
Bodik R. Growing solver-aided languages with rosette[C]//
Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software. New York: ACM Press,
2013: 135-152., articleTitle=Growing solver-aided languages with rosette, refAbstract=null), Reference(id=1241719261312373726, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=225, pageEnd=242, url=null, language=null, rfNumber=[26], rfOrder=25, authorNames=Nelson L, Bornholt J, Gu R H, journalName=Proceedings of the 27th ACM Symposium on Operating Systems Principles, refType=null, unstructuredReference=
Nelson L,
Bornholt J,
Gu R H, et al. Scaling symbolic evaluation for automated verification of systems code with Serval[C]//
Proceedings of the 27th ACM Symposium on Operating Systems Principles. New York: ACM Press,
2019: 225-242., articleTitle=Scaling symbolic evaluation for automated verification of systems code with Serval, refAbstract=null), Reference(id=1241719261383676896, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=1999, volume=null, issue=null, pageStart=193, pageEnd=207, url=null, language=null, rfNumber=[27], rfOrder=26, authorNames=Biere A, Cimatti A, Clarke E, journalName=Cleaveland W R.Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, refType=null, unstructuredReference=
Biere A,
Cimatti A,
Clarke E, et al. Symbolic model checking without BDDs[C]//
Cleaveland W R.Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer,
1999: 193-207., articleTitle=Symbolic model checking without BDDs, refAbstract=null), Reference(id=1241719261454980066, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2021, volume=null, issue=null, pageStart=530, pageEnd=545, url=null, language=null, rfNumber=[28], rfOrder=27, authorNames=Oberhauser J, De Lima Chehab R L, Behrens D, journalName=Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, refType=null, unstructuredReference=
Oberhauser J,
De Lima Chehab R L,
Behrens D, et al. VSync: Push-button verification and optimization for synchronization primitives on weak memory models[C]//
Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. New York: ACM Press,
2021: 530-545., articleTitle=VSync: Push-button verification and optimization for synchronization primitives on weak memory models, refAbstract=null), Reference(id=1241719261517894628, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2013, volume=null, issue=FAST’13, pageStart=null, pageEnd=null, url=null, language=null, rfNumber=[29], rfOrder=28, authorNames=Lu L Y, Arpaci-Dusseau A C, Arpaci-Dusseau R H, journalName=Proceedings of the 11th USENIX Conference on File and Storage Technologies, refType=null, unstructuredReference=
Lu L Y,
Arpaci-Dusseau A C,
Arpaci-Dusseau R H, et al. A study of linux file system evolution[C]//
Proceedings of the 11th USENIX Conference on File and Storage Technologies (FAST’13). New York: ACM Press,
2013, doi: 10.5555/2591272.2591276., articleTitle=A study of linux file system evolution, refAbstract=null), Reference(id=1241719261576614886, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=10.1145/279227.279229, pmid=null, pmcid=null, year=1998, volume=16, issue=2, pageStart=133, pageEnd=169, url=https://dl.acm.org/doi/10.1145/279227.279229, language=null, rfNumber=[30], rfOrder=29, authorNames=Lamport L, journalName=ACM Transactions on Computer Systems, refType=null, unstructuredReference=
Lamport L. The part-time parliament[J].
ACM Transactions on Computer Systems,
1998,
16(2): 133-169., articleTitle=The part-time parliament, refAbstract=Recent archaeological discoveries on the island of Paxos reveal that the parliament functioned despite the peripatetic propensity of its part-time legislators. The legislators maintained consistent copies of the parliamentary record, despite their frequent forays from the chamber and the forgetfulness of their messengers. The Paxon parliament's protocol provides a new way of implementing the state machine approach to the design of distributed systems.), Reference(id=1241719261664695272, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2002, volume=null, issue=null, pageStart=45, pageEnd=48, url=null, language=null, rfNumber=[31], rfOrder=30, authorNames=Lamport L, Matthews J, Tuttle M, journalName=Proceedings of the 10th Workshop on ACM SIGOPS European Workshop, refType=null, unstructuredReference=
Lamport L,
Matthews J,
Tuttle M, et al. Specifying and verifying systems with TLA
+[C]//
Proceedings of the 10th Workshop on ACM SIGOPS European Workshop. New York: ACM Press,
2002: 45-48., articleTitle=Specifying and verifying systems with TLA
+, refAbstract=null), Reference(id=1241719261735998440, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2014, volume=null, issue=null, pageStart=305, pageEnd=320, url=null, language=null, rfNumber=[32], rfOrder=31, authorNames=Ongaro D, Ousterhout J, journalName=Proceedings of the 2014 USENIX conference on USENIX Annual Technical Conference, refType=null, unstructuredReference=
Ongaro D,
Ousterhout J. In search of an understandable consensus algorithm[C]//
Proceedings of the 2014 USENIX conference on USENIX Annual Technical Conference. New York: ACM Press,
2014: 305-320., articleTitle=In search of an understandable consensus algorithm, refAbstract=null), Reference(id=1241719261803107306, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=445, pageEnd=454, url=null, language=null, rfNumber=[33], rfOrder=32, authorNames=Wang Z G, Zhao C G, Mu S, journalName=Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, refType=null, unstructuredReference=
Wang Z G,
Zhao C G,
Mu S, et al. On the parallels between paxos and raft, and how to port optimizations[C]//
Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing. New York: ACM Press,
2019: 445-454., articleTitle=On the parallels between paxos and raft, and how to port optimizations, refAbstract=null), Reference(id=1241719261878604779, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2018, volume=null, issue=null, pageStart=221, pageEnd=230, url=null, language=null, rfNumber=[34], rfOrder=33, authorNames=Begoli E, Camacho-Rodríguez J, Hyde J, journalName=Proceedings of the 2018 International Conference on Management of Data, refType=null, unstructuredReference=
Begoli E,
Camacho-Rodríguez J,
Hyde J, et al. Apache Calcite: A foundational framework for optimized query processing over heterogeneous data sources[C]//
Proceedings of the 2018 International Conference on Management of Data. New York: ACM Press,
2018: 221-230., articleTitle=Apache Calcite: A foundational framework for optimized query processing over heterogeneous data sources, refAbstract=null), Reference(id=1241719261941519340, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2022, volume=null, issue=null, pageStart=94, pageEnd=107, url=null, language=null, rfNumber=[35], rfOrder=34, authorNames=Wang Z G, Zhou Z, Yang Y C, journalName=Proceedings of the 2022 International Conference on Management of Data, refType=null, unstructuredReference=
Wang Z G,
Zhou Z,
Yang Y C, et al. WeTune: Automatic discovery and verification of query rewrite rules[C]//
Proceedings of the 2022 International Conference on Management of Data. New York: ACM Press,
2022: 94-107., articleTitle=WeTune: Automatic discovery and verification of query rewrite rules, refAbstract=null), Reference(id=1241719262004433901, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2017, volume=null, issue=null, pageStart=273, pageEnd=297, url=null, language=null, rfNumber=[36], rfOrder=35, authorNames=Kim J, Sjöberg V, Gu R H, journalName=Proceedings of the 15th Asian Symposium on Programming Languages and Systems, refType=null, unstructuredReference=
Kim J,
Sjöberg V,
Gu R H, et al. Safety and liveness of MCS lock—Layer by layer[C]//
Proceedings of the 15th Asian Symposium on Programming Languages and Systems. Berlin: Springer,
2017: 273-297., articleTitle=Safety and liveness of MCS lock—Layer by layer, refAbstract=null), Reference(id=1241719262075737070, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2015, volume=50, issue=8, pageStart=215, pageEnd=226, url=null, language=null, rfNumber=[37], rfOrder=36, authorNames=Chabbi M, Fagan M, Mellor-Crummey J, journalName=ACM SIGPLAN Notices, refType=null, unstructuredReference=
Chabbi M,
Fagan M,
Mellor-Crummey J. High performance locks for multi-level NUMA systems[J].
ACM SIGPLAN Notices,
2015,
50(8): 215-226., articleTitle=High performance locks for multi-level NUMA systems, refAbstract=null), Reference(id=1241719262142845935, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2019, volume=null, issue=null, pageStart=1, pageEnd=15, url=null, language=null, rfNumber=[38], rfOrder=37, authorNames=Dice D, Kogan A, journalName=Proceedings of the Fourteenth EuroSys Conference 2019, refType=null, unstructuredReference=
Dice D,
Kogan A. Compact NUMA-aware locks[C]//
Proceedings of the Fourteenth EuroSys Conference 2019. New York: ACM Press,
2019: 1-15., articleTitle=Compact NUMA-aware locks, refAbstract=null), Reference(id=1241719262214149104, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=10.1145/78969.78972, pmid=null, pmcid=null, year=1990, volume=12, issue=3, pageStart=463, pageEnd=492, url=https://dl.acm.org/doi/10.1145/78969.78972, language=null, rfNumber=[39], rfOrder=38, authorNames=Herlihy M P, Wing J M, journalName=ACM Transactions on Programming Languages and Systems, refType=null, unstructuredReference=
Herlihy M P,
Wing J M. Linearizability: A correctness condition for concurrent objects[J].
ACM Transactions on Programming Languages and Systems,
1990,
12(3): 463-492., articleTitle=Linearizability: A correctness condition for concurrent objects, refAbstract=A concurrent object is a data object shared by concurrent processes. Linearizability is a correctness condition for concurrent objects that exploits the semantics of abstract data types. It permits a high degree of concurrency, yet it permits programmers to specify and reason about concurrent objects using known techniques from the sequential domain. Linearizability provides the illusion that each operation applied by concurrent processes takes effect instantaneously at some point between its invocation and its response, implying that the meaning of a concurrent object's operations can be given by pre- and post-conditions. This paper defines linearizability, compares it to other correctness conditions, presents and demonstrates a method for proving the correctness of implementations, and shows how to reason about concurrent objects, given they are linearizable.), Reference(id=1241719262272869361, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=2013, volume=null, issue=null, pageStart=111, pageEnd=120, url=null, language=null, rfNumber=[40], rfOrder=39, authorNames=Biely M, Milosevic Z, Santos N, journalName=Proceedings of the 2012 IEEE 31st Symposium on Reliable Distributed Systems, refType=null, unstructuredReference=
Biely M,
Milosevic Z,
Santos N, et al. S-paxos: Offloading the leader for high throughput state machine replication[C]//
Proceedings of the 2012 IEEE 31st Symposium on Reliable Distributed Systems. Piscataway: IEEE Press,
2013: 111-120., articleTitle=S-paxos: Offloading the leader for high throughput state machine replication, refAbstract=null), Reference(id=1241719262352561138, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=527, pageEnd=536, url=null, language=null, rfNumber=[41], rfOrder=40, authorNames=Marandi P J, Primi M, Schiper N, journalName=Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems & Networks (DSN). Piscataway:IEEE Press, 2010, refType=null, unstructuredReference=
Marandi P J,
Primi M,
Schiper N, et al. Ring Paxos: A high-throughput atomic broadcast protocol[C]//
Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems & Networks (DSN). Piscataway:IEEE Press, 2010: 527-536., articleTitle=Ring Paxos: A high-throughput atomic broadcast protocol, refAbstract=null), Reference(id=1241719262423864308, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=10.1016/0304-3975(91)90224-P, pmid=null, pmcid=null, year=1991, volume=82, issue=2, pageStart=253, pageEnd=284, url=https://linkinghub.elsevier.com/retrieve/pii/030439759190224P, language=null, rfNumber=[42], rfOrder=41, authorNames=Abadi M, Lamport L, journalName=Theoretical Computer Science, refType=null, unstructuredReference=
Abadi M,
Lamport L. The existence of refinement mappings[J].
Theoretical Computer Science,
1991,
82(2): 253-284., articleTitle=The existence of refinement mappings, refAbstract=null), Reference(id=1241719262490973173, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=null, pmid=null, pmcid=null, year=null, volume=null, issue=null, pageStart=2735, pageEnd=2748, url=null, language=null, rfNumber=[43], rfOrder=42, authorNames=Zhou Q, Arulraj J, Navathe S B, journalName=Proceedings of the 2022 IEEE 38th International Conference on Data Engineering (ICDE). Piscataway:IEEE Press, 2022, refType=null, unstructuredReference=
Zhou Q,
Arulraj J,
Navathe S B, et al. SPES: A symbolic approach to proving query equivalence under bag semantics[C]//
Proceedings of the 2022 IEEE 38th International Conference on Data Engineering (ICDE). Piscataway:IEEE Press, 2022: 2735-2748., articleTitle=SPES: A symbolic approach to proving query equivalence under bag semantics, refAbstract=null), Reference(id=1241719262553887734, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, doi=10.1145/3140587.3062348, pmid=null, pmcid=null, year=2017, volume=52, issue=6, pageStart=510, pageEnd=524, url=https://dl.acm.org/doi/10.1145/3140587.3062348, language=null, rfNumber=[44], rfOrder=43, authorNames=Chu S M, Weitz K, Cheung A, journalName=ACM SIGPLAN Notices, refType=null, unstructuredReference=
Chu S M,
Weitz K,
Cheung A, et al. HoTTSQL: Proving query rewrites with univalent SQL semantics[J].
ACM SIGPLAN Notices,
2017,
52(6): 510-524., articleTitle=HoTTSQL: Proving query rewrites with univalent SQL semantics, refAbstract=Every database system contains a query optimizer that performs query rewrites. Unfortunately, developing query optimizers remains a highly challenging task. Part of the challenges comes from the intricacies and rich features of query languages, which makes reasoning about rewrite rules difficult. In this paper, we propose a machine-checkable denotational semantics for SQL, the de facto language for relational database, for rigorously validating rewrite rules. Unlike previously proposed semantics that are either non-mechanized or only cover a small amount of SQL language features, our semantics covers all major features of SQL, including bags, correlated subqueries, aggregation, and indexes. Our mechanized semantics, called HoTT SQL, is based on K-Relations and homotopy type theory, where we denote relations as mathematical functions from tuples to univalent types. We have implemented HoTTSQL in Coq, which takes only fewer than 300 lines of code and have proved a wide range of SQL rewrite rules, including those from database research literature (e.g., magic set rewrites) and real-world query optimizers (e.g., subquery elimination). Several of these rewrite rules have never been previously proven correct. In addition, while query equivalence is generally undecidable, we have implemented an automated decision procedure using HoTTSQL for conjunctive queries: a well studied decidable fragment of SQL that encompasses many real-world queries.)], funds=null, companyList=[AuthorCompany(id=1241719253846512476, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, xref=null, ext=[AuthorCompanyExt(id=1241719253850706781, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, companyId=1241719253846512476, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1. School of Software, Shanghai Jiao Tong University, Shanghai 200240, China), AuthorCompanyExt(id=1241719253859095390, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, companyId=1241719253846512476, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=1.上海交通大学软件学院，上海 200240)]), AuthorCompany(id=1241719253909427040, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, xref=null, ext=[AuthorCompanyExt(id=1241719253917815649, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, companyId=1241719253909427040, language=EN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=2. Huawei Dresden Research Center, Dresden 01069, Germany), AuthorCompanyExt(id=1241719253922009954, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, companyId=1241719253909427040, language=CN, country=null, province=null, city=null, postcode=null, companyName=null, departmentName=null, remark=2.华为德累斯顿研究所，德国德累斯顿 01069)])], figs=[ArticleFig(id=1241719257214538648, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=EN, label=null, caption=null, figureFileSmall=w/kheaPOyd2udYopvh1jrQ==, figureFileBig=UT3j8+N+uznLytGTjaXk6w==, tableContent=null), ArticleFig(id=1241719257285841818, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=CN, label=图1, caption=
形式化方法应用案例概览, figureFileSmall=w/kheaPOyd2udYopvh1jrQ==, figureFileBig=UT3j8+N+uznLytGTjaXk6w==, tableContent=null), ArticleFig(id=1241719257495557022, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=EN, label=null, caption=null, figureFileSmall=KpL20ZnfLRypPCRwsj3LCw==, figureFileBig=ogcM6Kkj1XGDAA/1pK6L/Q==, tableContent=null), ArticleFig(id=1241719257566860192, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=CN, label=图2, caption=
VSync系统流程图, figureFileSmall=KpL20ZnfLRypPCRwsj3LCw==, figureFileBig=ogcM6Kkj1XGDAA/1pK6L/Q==, tableContent=null), ArticleFig(id=1241719257646551969, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=EN, label=null, caption=null, figureFileSmall=M/2bW0X8pC9bxjbo7B19Pg==, figureFileBig=0rLTfPndhpx0LwJxEOpDjA==, tableContent=null), ArticleFig(id=1241719257717855139, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=CN, label=图3, caption=
CLoF系统流程图, figureFileSmall=M/2bW0X8pC9bxjbo7B19Pg==, figureFileBig=0rLTfPndhpx0LwJxEOpDjA==, tableContent=null), ArticleFig(id=1241719257793352613, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=EN, label=null, caption=null, figureFileSmall=gEKlhnzueTgKELlSg6gyWg==, figureFileBig=oiHTjTOK/GxTjgr18FAJYg==, tableContent=null), ArticleFig(id=1241719257852072871, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=CN, label=图4, caption=
文件系统操作的可线性化, figureFileSmall=gEKlhnzueTgKELlSg6gyWg==, figureFileBig=oiHTjTOK/GxTjgr18FAJYg==, tableContent=null), ArticleFig(id=1241719257944347561, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=EN, label=null, caption=null, figureFileSmall=xjGQGuo3VWinnFtYnaCwog==, figureFileBig=4hwTj86OaowuUkimCM0QHg==, tableContent=null), ArticleFig(id=1241719257998873515, tenantId=1146029695717560320, journalId=1146032081894723586, articleId=1241719226717762296, language=CN, label=图5, caption=
WeTune系统架构图, figureFileSmall=xjGQGuo3VWinnFtYnaCwog==, figureFileBig=4hwTj86OaowuUkimCM0QHg==, tableContent=null)], attaches=null, journal=Journal(id=1129340393107079197, delFlag=0, nameCn=前瞻科技, nameEn=Science and Technology Foresight, nameHistory1=null, nameHistory2=null, issn=2097-0781, eissn=, cn=10-1786/N, coden=null, periodic=2, language=CN, oaType=null, ccby=null, superviseOffice=null, ownerOffice=null, pubOffice=null, editorOffice=null, officeType=null, aims=null, clcCode=null, officeProv=null, officeCity=null, officeAddr=null, officeZip=null, officeEmail=null, officePhone=null, editDirector=null, officeDirector=null, officeDirectorPhone=null, officeStaffNum=null, officeEmpNum=null, coverPicUrl=ti95jJIJzXaf02YNe1UF2A==, journalPrice=null, startedYear=null, abbrevIsoEn=Sci Technol Fore, journalRemark=null, publicationField=null, createdTime=null, updatedTime=1757931223825, createdBy=null, updatedBy=15831073675, firstLetterCn=S, firstLetterEn=S, subjectCode=Natural Sciences, subjectName=自然科学, subjectCodeEn=Natural Sciences, subjectNameEn=null, picCn=ti95jJIJzXaf02YNe1UF2A==, picEn=cuGsq8KPhoqtfsQROuZvoQ==, jcr=null, cjcr=null, exts=[JournalExt(id=1174411930946125939, language=CN, name=前瞻科技, nameHistory1=null, nameHistory2=null, managedBy=, sponsoredBy=, publishedBy=, editorOffice=, officeProv=null, officeCity=null, officeAddr=, officeZip=, editDirector=null, officeDirector=null, officePhone=null, coverPicUrl=null, journalRemark=, submitArticleUrl=null, websiteUrl=http://www.qianzhankeji.cn/CN/2097-0781/home.shtml, createdTime=1757931223856, updatedTime=1757931223856, createdBy=15831073675, updatedBy=15831073675, submissionGuidelinesUrl=http://www.qianzhankeji.cn/CN/column/column7.shtml, submissionAuthorUrl=https://qzkjauthor.cast.org.cn/webm/, submissionEditorUrl=https://qzkjeditor.cast.org.cn/webm/, submissionReviewUrl=https://qzkjauthor.cast.org.cn/webm/, submissionCeEditorUrl=https://qzkjeditor.cast.org.cn/webm/, submissionAeEditorUrl=https://qzkjeditor.cast.org.cn/webm/, option={"copyright":""}), JournalExt(id=1174411931076149364, language=EN, name=Science and Technology Foresight, nameHistory1=null, nameHistory2=null, managedBy=, sponsoredBy=, publishedBy=, editorOffice=, officeProv=null, officeCity=null, officeAddr=, officeZip=, editDirector=null, officeDirector=null, officePhone=null, coverPicUrl=null, journalRemark=, submitArticleUrl=null, websiteUrl=http://www.qianzhankeji.cn/EN/2097-0781/home.shtml, createdTime=1757931223887, updatedTime=1757931223887, createdBy=15831073675, updatedBy=15831073675, submissionGuidelinesUrl=http://www.qianzhankeji.cn/EN/column/column7.shtml, submissionAuthorUrl=https://qzkjauthor.manuscriptcloud.com/login, submissionEditorUrl=https://qzkjeditor.manuscriptcloud.com/login, submissionReviewUrl=https://qzkjauthor.manuscriptcloud.com/login, submissionCeEditorUrl=https://qzkjeditor.manuscriptcloud.com/login, submissionAeEditorUrl=https://qzkjeditor.manuscriptcloud.com/login, option={"copyright":""})], databaseList=null, tenantJournalId=1146032081894723586, websiteList=[Website(id=1148243202353652128, webName=null, webTitle=null, webDomain=null, webCopyrigh=null, webIpcNo=null, seoTitle=null, seoKeywords=null, seoDescription=null, tenantJournalId=null, journalId=1146032081894723586, journalNameCn=null, journalNameEn=null, grayFlag=null, tenantId=1146029695717560320, platformId=null, journalGroupId=null, journalGroupNameCn=null, journalGroupNameEn=null, type=1, domain=https://castjournals.cast.org.cn/joweb/qzkj/CN, language=CN, createTime=1751692112768, createBy=18614031015, updateTime=1753516254852, updateBy=18614031015, name=《前瞻科技》中文站点, tplId=1146099689490845704, title=前瞻科技, delFlag=0, indexPage=/home, props=[WebsiteProps(id=1148618977242275853, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=articleTextType, value=kx, createTime=1751781704483, updateTime=1751781704483, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977217110026, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=banner, value=null, createTime=1751781704477, updateTime=1751781704477, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977204527113, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=logo, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic?fileId=skpCN5mVIzgEJbdUXu8/8A==, createTime=1751781704474, updateTime=1751781704474, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977233887244, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=picServerUrl, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic, createTime=1751781704481, updateTime=1751781704481, creator=18614031015, updator=18614031015), WebsiteProps(id=1148618977225498635, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1148243202353652128, code=staticResourcePath, value=https://castjournals.cast.org.cn/joweb/cast_kjdb_cn_619/, createTime=1751781704479, updateTime=1751781704479, creator=18614031015, updator=18614031015)]), Website(id=1155894377965830154, webName=null, webTitle=null, webDomain=null, webCopyrigh=null, webIpcNo=null, seoTitle=null, seoKeywords=null, seoDescription=null, tenantJournalId=null, journalId=1146032081894723586, journalNameCn=null, journalNameEn=null, grayFlag=null, tenantId=1146029695717560320, platformId=null, journalGroupId=null, journalGroupNameCn=null, journalGroupNameEn=null, type=1, domain=https://castjournals.cast.org.cn/joweb/qzkj/EN, language=EN, createTime=1753516295187, createBy=18614031015, updateTime=1753516295187, updateBy=18614031015, name=《前瞻科技》英文站点, tplId=1146101810881728533, title=Science and Technology Foresight, delFlag=0, indexPage=/home, props=[WebsiteProps(id=1155894740970233959, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=articleTextType, value=kx, createTime=1753516381733, updateTime=1753516381733, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740953456740, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=banner, value=null, createTime=1753516381729, updateTime=1753516381729, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740945068131, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=logo, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic?fileId=skpCN5mVIzgEJbdUXu8/8A==, createTime=1753516381727, updateTime=1753516381727, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740966039654, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=picServerUrl, value=https://castjournals.cast.org.cn/joweb/kjdb/CN/file/pic, createTime=1753516381732, updateTime=1753516381732, creator=18614031015, updator=18614031015), WebsiteProps(id=1155894740961845349, tenantId=1146029695717560320, journalId=null, journalGroupId=null, siteId=1155894377965830154, code=staticResourcePath, value=https://castjournals.cast.org.cn/joweb/cast_kjdb_cn_619/, createTime=1753516381731, updateTime=1753516381731, creator=18614031015, updator=18614031015)])], journalTitle=前瞻科技, weixinUrl=null, journalUrl=null, iacademicId=null, status=0, seqNo=null, journalTitleEn=Science and Technology Foresight, journalPhotoCn=ti95jJIJzXaf02YNe1UF2A==, journalPhotoEn=cuGsq8KPhoqtfsQROuZvoQ==, journalFirstLetter=S, journalRecommend=null, journalNew=null, journalCollection=null, jcrJf=null, cjcrJf=null, jcrJfStr=null, cjcrJfStr=null, submissionFirstDecision=null, sciSubjectClassification=null, casSubjectClassification=null, citeScore=null, totalCitationFrequency=null, icpCode=null, psCode=null, advertisingLicenseCode=null, copyrightInformation=null, country=null, option=, provinceCode=null, provinceName=null, collectFlag=false), detailUrlCn=https://castjournals.cast.org.cn/joweb/qzkj/CN/10.3981/j.issn.2097-0781.2023.01.003, detailUrlEn=https://castjournals.cast.org.cn/joweb/qzkj/EN/10.3981/j.issn.2097-0781.2023.01.003, pdfUrlCn=https://castjournals.cast.org.cn/joweb/qzkj/CN/PDF/10.3981/j.issn.2097-0781.2023.01.003, pdfUrlEn=https://castjournals.cast.org.cn/joweb/qzkj/EN/PDF/10.3981/j.issn.2097-0781.2023.01.003, aliStartDate=null, aliEndDate=null, collectionFlag=false, citedCount=null, citedUrl=null, reference=null)
PDF Download
Full
2281
1171
Close Full
