约束求解与定理证明专题前言.pdf
《约束求解与定理证明专题前言.pdf》由会员分享,可在线阅读,更多相关《约束求解与定理证明专题前言.pdf(2页珍藏版)》请在咨信网上搜索。
1、 软件学报 ISSN 1000-9825,CODEN RUXUEW E-mail: Journal of Software,2023,34(8):34653466 doi:10.13328/ki.jos.006871 http:/ 中国科学院软件研究所版权所有.Tel:+86-10-62562563 约束求解与定理证明专题前言 蔡少伟1,陈振邦2,王 戟2,詹博华1,赵永望3 1(中国科学院 软件研究所,北京 100190)2(国防科技大学 计算机学院,湖南 长沙 410073)3(浙江大学 计算机科学与技术学院,浙江 杭州 310007)通信作者:蔡少伟,E-mail: 中文引用格式:蔡少伟
2、,陈振邦,王戟,詹博华,赵永望.约束求解与定理证明专题前言.软件学报,2023,34(8):3465 3466.http:/ 随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.形式化方法使用严格的数学语言对计算机系统建模,并在计算机的辅助下验证系统的正确性.与测试不同,形式化方法可以完全排除某些类型的错误.约束求解和定理证明是形式化方法中的两大关键技术.在约束求解方面,SAT 和 SMT 求解器已经在学术界和工业界得到了广泛应用,比如 SAT 求解器用于 EDA 领域的等价性验证,SMT 求解器用于程序验证和白盒模糊测试等.交互式定理证明通过人和计算机之间的交
3、互完成证明,能够验证非常复杂的系统和性质,例如编译器和操作系统的正确性验证.约束求解与定理证明专题关注约束求解和定理证明的理论、技术、工具与应用,包括在 EDA、符号执行、模型检测、程序分析与验证、系统安全等领域的应用.本专题公开征文,共收到投稿 16 篇.论文均通过了形式审查,内容涉及约束求解、定理证明以及它们的应用.特约编辑先后邀请了多位专家参与审稿工作,每篇投稿至少邀请 2 位专家进行评审.稿件经初审、复审、中国软件大会 ChinaSoft 2022 会议宣读和终审 4 个阶段,最终有 6 篇论文入选本专题.基于不可满足核的近似逼近可达性分析 提出了一种新型的基于不变式求解的可达性分析方
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 约束 求解 定理 证明 专题 前言
1、咨信平台为文档C2C交易模式,即用户上传的文档直接被用户下载,收益归上传人(含作者)所有;本站仅是提供信息存储空间和展示预览,仅对用户上传内容的表现方式做保护处理,对上载内容不做任何修改或编辑。所展示的作品文档包括内容和图片全部来源于网络用户和作者上传投稿,我们不确定上传用户享有完全著作权,根据《信息网络传播权保护条例》,如果侵犯了您的版权、权益或隐私,请联系我们,核实后会尽快下架及时删除,并可随时和客服了解处理情况,尊重保护知识产权我们共同努力。
2、文档的总页数、文档格式和文档大小以系统显示为准(内容中显示的页数不一定正确),网站客服只以系统显示的页数、文件格式、文档大小作为仲裁依据,平台无法对文档的真实性、完整性、权威性、准确性、专业性及其观点立场做任何保证或承诺,下载前须认真查看,确认无误后再购买,务必慎重购买;若有违法违纪将进行移交司法处理,若涉侵权平台将进行基本处罚并下架。
3、本站所有内容均由用户上传,付费前请自行鉴别,如您付费,意味着您已接受本站规则且自行承担风险,本站不进行额外附加服务,虚拟产品一经售出概不退款(未进行购买下载可退充值款),文档一经付费(服务费)、不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
4、如你看到网页展示的文档有www.zixin.com.cn水印,是因预览和防盗链等技术需要对页面进行转换压缩成图而已,我们并不对上传的文档进行任何编辑或修改,文档下载后都不会有水印标识(原文档上传前个别存留的除外),下载后原文更清晰;试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓;PPT和DOC文档可被视为“模板”,允许上传人保留章节、目录结构的情况下删减部份的内容;PDF文档不管是原文档转换或图片扫描而得,本站不作要求视为允许,下载前自行私信或留言给上传者【自信****多点】。
5、本文档所展示的图片、画像、字体、音乐的版权可能需版权方额外授权,请谨慎使用;网站提供的党政主题相关内容(国旗、国徽、党徽--等)目的在于配合国家政策宣传,仅限个人学习分享使用,禁止用于任何广告和商用目的。
6、文档遇到问题,请及时私信或留言给本站上传会员【自信****多点】,需本站解决可联系【 微信客服】、【 QQ客服】,若有其他问题请点击或扫码反馈【 服务填表】;文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“【 版权申诉】”(推荐),意见反馈和侵权处理邮箱:1219186828@qq.com;也可以拔打客服电话:4008-655-100;投诉/维权电话:4009-655-100。