Specification engineering and modular verification using a web-integrated verifying compiler
Specification engineering and modular verification using a web-integrated verifying compiler
复制标题
使用网络集成验证编译器进行规范工程和模块化验证
DOI：
10.1109/icse.2012.6227243
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
M. Sitaraman
中科院分区：
文献类型：
--
作者：
Charles T. Cook;Heather K. Harton;Hampton Smith;M. Sitaraman
该演示将介绍RESOLVE网络集成环境，该环境专门用于捕获组件关系，并允许构建和组合经过验证的通用组件。该环境促进了基于团队的软件开发，并已用于多个机构的本科CS教育。该环境可以很容易地模拟“假设”场景，包括替代规范风格对验证的影响，并催生了大量的研究和实验。演示将说明通用软件验证中的问题和高阶断言的作用。它将显示当验证失败时如何精确定位逻辑错误。视频介绍URL：http://www.youtube.com/watch? v=9vg3WuxeOkA。
This demonstration will present the RESOLVE web-integrated environment, which has been especially built to capture component relationships and allow construction and composition of verified generic components. The environment facilitates team-based software development and has been used in undergraduate CS education at multiple institutions. The environment makes it easy to simulate “what if” scenarios, including the impact of alternative specification styles on verification, and has spawned much research and experimentation. The demonstration will illustrate the issues in generic software verification and the role of higher-order assertions. It will show how logical errors are pinpointed when verification fails. Introductory video URL: http://www.youtube.com/watch?v=9vg3WuxeOkA.