检索规则说明:AND代表“并且”;OR代表“或者”;NOT代表“不包含”;(注意必须大写,运算符两边需空一格)
检 索 范 例 :范例一: (K=图书馆学 OR K=情报学) AND A=范并思 范例二:J=计算机应用与软件 AND (U=C++ OR U=Basic) NOT M=Visual
作 者:Byron Cook
机构地区:[1]亚马逊云科技
出 处:《软件和集成电路》2025年第1期10-13,共4页Software and Integrated Circuit
摘 要:开发者在运用自动推理工具时,需要具备特殊的思维方式—并非全面枚举所有可能的输入情况及潜在的错误路径,而是要侧重于明确系统运作的机制,精准识别出确保系统无误运行所不可或缺的条件,并进一步借助严谨的数学证明手段,来验证这些条件是否为真。在应用自动推理技术的10多年时间里,亚马逊云科技发现,经过验证的代码通常比未经过验证的代码性能更好,这主要是因为在验证过程中我们所做的bug(漏洞)修复工作通常会提升代码的运行性能,且经过验证的代码更容易更新、修改和操作。
关 键 词:自动推理 数学证明 精准识别 枚举 验证过程 修复工作 漏洞 开发者
分 类 号:TP393.09[自动化与计算机技术—计算机应用技术]
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在链接到云南高校图书馆文献保障联盟下载...
云南高校图书馆联盟文献共享服务平台 版权所有©
您的IP:216.73.216.33