一个实验性机械程序验证系统

葛湘川; 孙永强

首页> 中文期刊> 《上海交通大学学报》 >一个实验性机械程序验证系统

一个实验性机械程序验证系统

开具论文收录证明 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

本文介绍一个实验性的机械程序验证系统。该系统由VCG（验证条件生成器）,PROVER（定理化简）,以及RESOLUTION（消解）三部分组成。VCG采用归纳断言法产生验证条件。PROVER主要采用函数的识别和化简,一般代数式的代换与化简等手段,以证明不带量词的验证条件。RESOLUTION采用消解原理证明带量词的验证条件。该系统目前还处于实验阶段,在教学上可作为实验之用。该系统是用BASIC语言在WANG 2200计算机上实现的。

著录项

来源
《上海交通大学学报》 |1982年第2期|33-44|共12页
作者
葛湘川; 孙永强;
展开▼
作者单位

上海交通大学电工与计算机科学系;

上海交通大学电工与计算机科学系上海交通大学研究生;

展开▼
原文格式 PDF
正文语种 chi
中图分类
关键词

相似文献

中文文献
外文文献
专利

1. 基于微信小程序的校园身份验证系统的设计 [J] . 张志伟 ,乔雨 ,田季颖 . 电子制作 . 2020,第2期
2. PVM并行程序验证系统的原理与实现 [J] . 张兆庆 ,蒋昌俊 ,乔如良 . 计算机学报 . 1999,第4期
3. 计算机程序验证系统的开发方法 [J] . 章萃 . 科学 . 1999,第3期
4. 数控程序验证系统NCGV [J] . 黄和风 . 计算机辅助工程 . 1993,第1期
5. VDE:一个基于图形的IC设计高层次输入验证系统 [C] . 黄国勇 . 中国科协第三届青年学术年会 . 1998
6. 试飞验证系统模拟信号源总线接口及驱动程序设计 [A] . 宋洋 . 2015

一个实验性机械程序验证系统

摘要

著录项

相似文献

相关主题

期刊订阅