首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   91篇
  完全免费   32篇
  自动化技术   123篇
  2018年   2篇
  2017年   4篇
  2016年   1篇
  2015年   1篇
  2014年   2篇
  2013年   2篇
  2012年   2篇
  2011年   7篇
  2010年   7篇
  2009年   5篇
  2008年   10篇
  2007年   12篇
  2006年   3篇
  2005年   7篇
  2004年   5篇
  2003年   1篇
  2002年   5篇
  2001年   3篇
  2000年   3篇
  1999年   2篇
  1997年   4篇
  1996年   3篇
  1995年   3篇
  1994年   4篇
  1993年   3篇
  1992年   3篇
  1991年   4篇
  1990年   1篇
  1989年   8篇
  1987年   1篇
  1986年   1篇
  1984年   1篇
  1979年   2篇
  1975年   1篇
排序方式: 共有123条查询结果,搜索用时 109 毫秒
1.
PVM并行程序验证系统的原理与实现   总被引:5,自引:0,他引:5  
本文主要介绍PVM并行程序验证系统的基本原理和实现技术。首先,我们扼要分析PVM程序的构成与特点,然后阐述验证系统的理论模型和验证算法;最后,讨论开发过程中的若干关键技术,本系统的研制可为产行程序的自动转换和分析验证提供了一个可视化的运行环境。  相似文献
2.
Specifying coalgebras with modal logic   总被引:5,自引:0,他引:5  
We propose to use modal logic as a logic for coalgebras and discuss it in view of the work done on coalgebras as a semantics of object-oriented programming. Two approaches are taken: First, standard concepts of modal logic are applied to coalgebras. For a certain kind of functor it is shown that the logic exactly captures the notion of bisimulation and a complete calculus is given. Examples of verifications of object properties are given. Second, we discuss the relationship of this approach with the coalgebraic logic of Moss (Coalgebraic logic, Ann Pure Appl. Logic 96 (1999) 277–317.).  相似文献
3.
Model checking JAVA programs using JAVA PathFinder   总被引:5,自引:0,他引:5  
This paper describes a translator called Java PathFinder (Jpf), which translates from Java to Promela, the modeling language of the Spin model checker. Jpf translates a given Java program into a Promela model, which then can be model checked using Spin. The Java program may contain assertions, which are translated into similar assertions in the Promela model. The Spin model checker will then look for deadlocks and violations of any stated assertions. Jpf generates a Promela model with the same state space characteristics as the Java program. Hence, the Java program must have a finite and tractable state space. This work should be seen in a broader attempt to make formal methods applicable within NASA’s areas such as space, aviation, and robotics. The work is a continuation of an effort to formally analyze, using Spin, a multi-threaded operating system for the Deep-Space 1 space craft, and of previous work in applying existing model checkers and theorem provers to real applications.  相似文献
4.
A single complete rule for data refinement   总被引:4,自引:0,他引:4  
One module is said to be refined by a second if no program using the second module can detect that it is not using the first; in that case the second module can replace the first in any program. Data refinement transforms the interior pieces of a module — its state and consequentially its operations — in order to refine the module overall.A method for data refinement is sound if applying it actually does refine the module; a method is complete if any refinement of modules can be realised by its application.It has been known for some time that there are two methods of data refinement which are jointly complete for boundedly-nondeterministic programs: any refinement can be realised by applying one method then the other. Those two methods are formulated in terms of relations between states. Here it is shown that using predicate transformers, instead, allows a single complete method.  相似文献
5.
一种构造代码安全性证明的方法   总被引:4,自引:2,他引:2       下载免费PDF全文
郭 宇  陈意云  林春晓 《软件学报》2008,19(10):2720-2727
提出一种构造代码安全性证明的新方法.这种方法的基本思想是,在基础逻辑中定义辅助递归函数来帮助构造证明.这种构造方法在不增加系统信任计算基础的情况下可以极大地减轻构造证明的工作量,并且减小安全性证明的规模同时介绍了该方法在一个FPCC系统中的应用.在这个系统中使用该方法使得代码的安全性证明可以自动产生.全部工作的细节已在证明辅助工具Coq中得以实现.  相似文献
6.
The verified software repository: a step towards the verifying compiler   总被引:3,自引:3,他引:0  
The verified software repository is dedicated to a long-term vision of a future in which all computer systems justify the trust that society increasingly places in them. This would be accompanied by a substantial reduction in the current high costs of programming error, incurred during the design, development, testing, installation, maintenance, evolution, and retirement of computer software. An important technical contribution to this vision will be a verifying compiler: a tool-set that automatically proves that a program will always meet its specification, insofar as this has been formalised, without even needing to run it. This has been a challenge for computing research for over 30 years, but the current state of the art now gives grounds for hope that it may be implemented in the foreseeable future. Achievement of the overall vision will depend also on continued progress of research into dependability and software evolution, as envisaged by the UKCRC Grand Challenge project in dependable systems evolution. The verified software repository is a first step towards the realisation of this long-term vision. It will maintain and develop an evolving collection of state-of-the-art tools, together with a representative portfolio of real programs and specifications on which to test, evaluate, and develop the tools. It will contribute initially to the inter-working of tools, and eventually to their integration. It will promote transfer of the relevant technology to industrial tools and into software engineering practice. It will build on the recognised achievements of practical formal development of safety-critical computer applications, and contribute to an international initiative in verified software, covering theory, tools, and experimental validation. Received April 2005 Revised November 2005 Accepted November 2005 by C. B. Jones  相似文献
7.
A mechanically verified incremental garbage collector   总被引:3,自引:0,他引:3  
As an application of a system designed for concurrent program verification, we describe a formalisation and mechanical proof of the correctness of Ben-Ari's incremental garbage collection algorithm. The proof system is based on the Manna-Pnueli model of concurrency and is implemented as an extension of the Boyer-Moore prover. The correctness of the garbage collector is represented by two theorems, stating a) that nothing except garbage is ever collected (safety), and b) that all garbage is eventually collected (liveness). We compare our mechanised treatment with several published proofs of the same results.  相似文献
8.
软件安全漏洞的静态检测技术   总被引:3,自引:1,他引:2       下载免费PDF全文
张林  曾庆凯 《计算机工程》2008,34(12):157-159
软件安全漏洞问题日益严重,静态漏洞检测提供从软件结构和代码中寻找漏洞的方法。该文研究软件漏洞静态检测的两个主要方面:静态分析和程序验证,重点分析词法分析、规则检查、类型推导、模型检测、定理证明和符号执行等方法,将常用的静态检测工具按方法归类,讨论、总结静态检测技术的优势、适用性和发展趋势。  相似文献
9.
区间上非线性程序的终止性判定   总被引:3,自引:1,他引:2       下载免费PDF全文
姚勇 《软件学报》2010,21(12):3116-3123
分析了如下类型程序的终止性:While x∈Ω do {x:=f(x)} end.其中,x是程序变量,Ω是一个区间,f是一个连续函数.这类程序被称为区间上非线性程序.证明了上面程序不终止的必要条件是函数在区间内部或边界上有不动点.如果不动点不在区间的边界,则上述结果是充要条件.仅仅在区间边界上有不动点的情况下,对函数略加限制,也建立了相应结果.特别地,对逐段多项式连续函数程序的终止性给出了完备判定算法.  相似文献
10.
Programming and Verifying Subgame-Perfect Mechanisms   总被引:2,自引:0,他引:2  
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号