【摘 要】
：
可满足性模理论(satisfiability modulo theories,SMT)是判定一阶逻辑公式在组合背景理论下的可满足性问题.SMT的背景理论使其能很好地描述实际领域中的各种问题,结合高效的
【机 构】
：
基础软件国家工程研究中心（中国科学院软件研究所）,中国科学院大学,计算机科学国家重点实验室（中国科学院软件研究所）,中央财经大学信息学院
【基金项目】
：
国家自然科学基金项目(61170072,61303057);中国科学院、国家外国专家局创新团队国际合作伙伴计划~~
论文部分内容阅读
可满足性模理论(satisfiability modulo theories,SMT)是判定一阶逻辑公式在组合背景理论下的可满足性问题.SMT的背景理论使其能很好地描述实际领域中的各种问题,结合高效的可满足性判定算法,SMT在测试用例自动生成、程序缺陷检测、RTL(register transfer level)验证、程序分析与验证、线性逻辑约束公式优化问题求解等一些最新研究领域中有着突出的优势.首先阐述SMT问题的基础SAT(satisfiability)问题及判定算法;其次对SMT问题、判定算法进行了总结,分析了主流的SMT求解器,包括Z3,Yices2,CVC4等;然后着重介绍了SMT求解技术在典型领域中的实际应用,对目前的研究热点进行了阐述;最后对SMT未来的发展前景进行了展望,目的是试图推动SMT的发展,为此领域的相关人员提供有益的参考.
其他文献
施蛰存的文学创作是从诗开始的，他的文学翻译工作也是从诗开始的。施蛰存的文学翻译主张兼收并蓄，但他更热衷于现代主义诗歌的译介，他所翻译的外国现代主义诗歌作品一直影响到新
一、目的通过对白藜芦醇(RESVERATROL, Res)的处方前研究,制备和初步评价Res复合磷脂脂质体,比较其与单一磷脂脂质体在稳定性和其他方面的优势,并初步考察Res复合磷脂脂质体
列车横向悬挂系统可分为被动悬挂和主动悬挂两种形式,半主动悬挂是主动悬挂的一种形式.传统的被动悬挂系统的参数无法在车辆运行的过程中实施调节,难以适应列车在高速运行时
文章基于附加值贸易视角,利用WIOD数据库测度了中国整体及三类技术制造业行业参与全球价值链的程度及其在国际分工中的地位。研究结果表明,1995~2011年中国参与全球价值链的
钛合金材料对粘着磨损和微动磨损的敏感性限制其用于滑动机械部件,通过工艺试验,摸索出一种钛合金镀锌活化后化学镀镍的工艺方法,经这种方法处理的钛合金材料其摩擦系数减小,
随着我国高速公路信息化建设的蓬勃发展,如何提升高速公路的安全等级和运行效率成为我国高速公路建设新的关注要点。在诸多影响因素当中,冰雪冻雨等恶劣气象灾害对高速公路的
采用超声疲劳振动技术研究了桥梁钢Q345qC的母材和圆形对接焊接接头试件的高周与超高周疲劳性能.试验发现,在105～109循环周次内焊接接头的疲劳性能远低于母材,且无论是母材还
本文针对如何有效地对汽车后桥减速器主齿螺母拧紧扭矩进行控制，列出了当前所用到的四种扭矩控制方法，对每一种扭矩控制方法进行了力学分析，并分析了每一种方法的优缺点，在此基础
在对目前医疗影像存储与传输系统（PACS）存在问题进行分析的基础上，阐述其设计需求，进而提出PACS存储、数据保护等解决方案，并以安徽医科大学第一附属医院为例设计PACS整体架构。
<正> 高空观览车是一台高35米的大型钢结构件游艺机械,见图1示意图。它有一对互相对称的钢结构支承和一个直径为25米的钢结构转盘,转盘安装在长度为4.5米的主轴上,主轴两端各