【摘 要】
:
PAR方法通过对问题规约进行形式化演算得到用递推关系描述的算法,并专门设计Radl算法语言用于描述该算法.通过使用软件自动化技术实现了由Radl算法自动生成Apla程序的支撑平台,并对实现系统的核心算法使用最弱前置谓词方法进行了形式化验证.
【机 构】
:
武汉大学软件工程国家重点实验室,湖北 武汉 430072;江西师范大学省高性能计算重点实验室,江西 南昌 330022
【出 处】
:
2012年全国理论计算机科学学术年会(NCTCS2012)
论文部分内容阅读
PAR方法通过对问题规约进行形式化演算得到用递推关系描述的算法,并专门设计Radl算法语言用于描述该算法.通过使用软件自动化技术实现了由Radl算法自动生成Apla程序的支撑平台,并对实现系统的核心算法使用最弱前置谓词方法进行了形式化验证.
其他文献
Consider a simple polygon P and a point s on the frontier of (a)P.For any realδ>0 there exists a shortest path ρ inside of P such that s is on the path ρ,and for each point p in (a)P,there exists a po
Christian Anfinsen proposed that the native states of proteins reside in the free energy minima.This “thermodynamic hypothesis” has been widely accepted as the “central dogma” of protein folding.
In image restoration of spatial domain,there need to make use of the available structure of image blurring matrix,and use diagonalization or convolution to substitute the matrix-vector product involvi
序列结构比对是生物信息学中用来预测新生物体序列的结构和功能的一种重要方法.为了识别新序列的结构同源性,序列结构比对不但要考虑序列的相似性,还要考虑残基之间相互作用而导致的空间保守结构,因此是经典的NP-hard问题.
A large numbers of data sources in DataSpace and ubiquitous data object may has relevant with different types of data objects,therefore,finding the potential relevance of heterogeneous data has become
Segmentation of license plate image is the first step in a license plate recognition system.The plate segmentation result is crucial to and determines the final result of license plate recognition/ana
Image segmentation is an essential component of image analysis system,and determines the quality of the nal result of image analysis.This paper proposed a kernelized fuzzy c-means clustering algorithm
In this paper,the coverage problem of repeaters has been investigated and an optimization-based model for the planning of repeaters has been presented.Meta-Heuristic search algorithm including Simulat
As the core of FM-index and compressed suffix array,the Burrows-Wheeler Transform (BWT) plays a key role in indexing genomic sequence data for pattern search.It can run in O(n) bits,typically in total
形式化方法是验证并发系统可靠性和安全性的重要手段.对高级语言开发的并发系统自动抽取的模型进行形式化验证是模型检测技术领域中的一个研究热点.