共查询到20条相似文献,搜索用时 152 毫秒
1.
PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C 等可执行程序. 相似文献
2.
迭代计算数据流等式的解,是数据流分析的常用方法.计算支配节点,从而识别自然循环,是许多现代编译器优化分析的重要组成部分.机械化验证高效的求解支配节点的算法通常是获得一个实际的“验证编译器”不可或缺的一部分.为了形式化证明一个高效的迭代求解严格支配节点的算法(CHK),首先建立了值域是逆序列表集合的半格结构,逆序列表中的元素是控制流图中节点的逆后序遍历次序,并证明了它是一个半格,其偏序满足上升链条件.然后使用半格结构,实现了一个基于工作表的Kildall迭代算法,计算严格支配节点.接下来,首先给出了控制流图中支配节点的定义性规范和相关性质定理,然后构造并证明了迭代求解算法所满足的重要性质.利用这些性质定理,相对于定义性规范,证明了该迭代求解算法的正确性和完备性.最后进行总结,并讨论未来工作.整个形式化开发使用的是定理证明助手Isabelle/HOL. 相似文献
3.
0/1背包问题动态规划算法的探讨 总被引:2,自引:0,他引:2
0/1背包问题是运筹学中的著名问题,有重要的使用价值,是算法研究的热点,目前较成熟的常用算法有贪心算法、动态规划、回溯法、分枝-限界法等.本文探讨动态规划的向前处理法.与教材不同的是,本文结合实例,给出递推关系式的具体递推过程,用图例表示背包问题的向前处理法求解过程;最后,用浅显的实例验证向前处理法算法所得最优解的正确性. 相似文献
4.
计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言是完备的.基于GJK算法设计了计算空间两条线段间距离的算法,用定理证明器HOL4对其相关的定义和定理进行形式化定义和证明,进而基于霍尔逻辑完成形式化表示和证明,对该算法的正确性实现了形式化验证.最后,给出了这一经过验证的算法在双臂机器人无碰撞运动规划中的应用. 相似文献
5.
形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值。 相似文献
6.
由于系统的巨大规模,操作系统设计和实现的正确性很难用传统的方法进行描述和验证.在汇编层形式化地对系统模块的功能语义进行建模,提出一种汇编级的系统状态模型,作为汇编语言层设计和验证的纽带.通过定义系统状态模型的合法状态和状态转换函数来建立系统状态模型的论域,并以此来描述汇编层的论域.通过验证汇编层的功能模块的正确性来保证汇编语言层设计的正确性,达到对系统功能实现的正确性验证.同时,使用定理证明工具Isabelle/HOL来形式化地描述这一系统状态模型,基于这一形式化模型,在Isabelle/HOL中验证系统模块的功能语义的正确性.以实现的安全可信OS(verified secure operating system,简称VSOS)为例,阐述了所提出的形式化设计和验证方法,说明了这一方法的可行性. 相似文献
7.
基于机器定理证明的形式验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.文件比较算法(File Comparison Algorithm)是一类成员众多,应用极为广泛,跨越生物信息学、情报检索、网络安全等多个应用领域的基础算法,但关于它们的形式验证工作很少,至今未有经机器检查的性质证明.本文在交互式定理证明器Isabelle/HOL 中对Miller和Myers在1985年提出的基于行的文件比较算法fcomp作了形式化,改正了算法关于边界变量迭代的一个小错误,证明了改正后算法的可终止性和正确性;对算法时间复杂性作了完全形式化的分析,印证了算法作者的非形式化分析结论.本文为今后更多文件比较算法的形式验证提供了可供借鉴的经验. 相似文献
8.
9.
形式化推导是在程序正确性证明理论下所进行的程序开发,最终得到完全正确的算法程序。针对序列折半划分问题,现有的形式化推导方法将推导与证明交替进行,推导过程繁琐且大多无法直接获得可执行程序。为解决上述问题,提出了一种新的序列折半划分问题的形式化推导方法。该方法基于分划递推的核心思想,应用规约变换技术对问题规约进行变换并严格保证一致性,使得在推导过程中无需交替证明,进而导出递推关系式并得到高可靠性抽象算法程序Apla,最终通过转换工具自动生成可执行程序。实现了从程序规约到具体可执行程序的完整程序求精过程。以2个序列算法为例,验证了该方法的有效性和可行性,对相关问题的形式化推导具有指导意义。 相似文献
10.
采用形式化方法证明软件的正确性是保障软件可靠性的有效方法,而对循环语句的分析与验证是形式化证明中的关键,对循环语句的处理一直是程序分析与验证中的一个难点问题.本文提出使用循环语句修改的内存和这些内存中存放的新值来描述循环语句的执行效果,并将该执行效果定义为循环摘要.同时,本文提出了一种自动生成循环摘要的方法,可以为操作常用数据结构的循环自动生成循环摘要,包含嵌套循环.此外,基于循环摘要,我们可以自动生成循环语句的规约,包括循环不变式、循环的前置条件以及循环的后置条件.我们已经实现了自动生成循环摘要以及循环规约的方法,并将它们集成到验证工具Accumulator中,实验表明,我们的方法可以有效地生成循环摘要,并生成多种类型的规约,从而辅助软件程序的形式化证明,提高验证的自动化程度和效率,减轻验证人员的负担. 相似文献
11.
Filip Mari? 《Theoretical computer science》2010,411(50):4333-4356
We present a formalization and a formal total correctness proof of a MiniSAT-like SAT solver within the system Isabelle/HOL. The solver is based on the DPLL procedure and employs most state-of-the-art SAT solving techniques, including the conflict-guided backjumping, clause learning, and the two-watched unit propagation scheme. A shallow embedding into Isabelle/HOL is used and the solver is expressed as a set of recursive HOL functions. Based on this specification, the Isabelle’s built-in code generator can be used to generate executable code in several supported functional languages (Haskell, SML, and OCaml). The SAT solver implemented in this way is, to our knowledge, the first fully formally and mechanically verified modern SAT solver. 相似文献
12.
We present a principled modular approach to the development of construction and verification tools for imperative programs, in which the control flow and the data flow are cleanly separated. Our simplest verification tool uses Kleene algebra with tests for the control flow of while-programs and their standard relational semantics for the data flow. It is expanded to a basic program construction tool by adding an operation for the specification statement and one single axiom. To include recursive procedures, Kleene algebras with tests are expanded further to quantales with tests. In this more expressive setting, iteration and the specification statement can be defined explicitly and stronger program transformation rules can be derived. Programming our approach in the Isabelle/HOL interactive theorem prover yields simple lightweight mathematical components as well as program construction and verification tools that are correct by construction themselves. Verification condition generation and program construction rules are based on equational reasoning and supported by powerful Isabelle tactics and automated theorem proving. A number of examples shows our tools at work. 相似文献
13.
Sascha Böhme Michał Moskal Wolfram Schulte Burkhart Wolff 《Journal of Automated Reasoning》2010,44(1-2):111-144
Boogie is a verification condition generator for an imperative core language. It has front-ends for the programming languages C# and C enriched by annotations in first-order logic, i.e. pre- and postconditions, assertions, and loop invariants. Moreover, concepts like ghost fields, ghost variables, ghost code and specification functions have been introduced to support a specific modeling methodology. Boogie’s verification conditions—constructed via a wp calculus from annotated programs—are usually transferred to automated theorem provers such as Simplify or Z3. This also comprises the expansion of language-specific modeling constructs in terms of a theory describing memory and elementary operations on it; this theory is called a machine/memory model. In this paper, we present a proof environment, HOL-Boogie, that combines Boogie with the interactive theorem prover Isabelle/HOL, for a specific C front-end and a machine/memory model. In particular, we present specific techniques combining automated and interactive proof methods for code verification. The main goal of our environment is to help program verification engineers in their task to “debug” annotations and to find combined proofs where purely automatic proof attempts fail. 相似文献
14.
Jan Olaf Blech Sabine Glesner Johannes Leitner Steffen Mülling 《Electronic Notes in Theoretical Computer Science》2005,141(2):33-49
Correctness of compilers is a vital precondition for the correctness of the software translated by them. In this paper, we present two approaches for the formalization of static single assignment (SSA) form together with two corresponding formal proofs in the Isabelle/HOL system, each showing the correctness of code generation. Our comparison between the two proofs shows that it is very important to find adequate formalizations in formal proofs since they can simplify the verification task considerably. Our formal correctness proofs do not only verify the correctness of a certain class of code generation algorithms but also give us sufficient, easily checkable correctness criteria characterizing correct compilation results obtained from implementations (compilers) of these algorithms. These correctness criteria can be used in a compiler result checker. 相似文献
15.
Christian Sternagel 《Journal of Automated Reasoning》2013,51(4):357-370
We present our Isabelle/HOL formalization of GHC’s sorting algorithm for lists, proving its correctness and stability. This constitutes another example of applying a state-of-the-art proof assistant to real-world code. Furthermore, it allows users to take advantage of the formalized algorithm in generated code. 相似文献
16.
Ralph-Johan Back 《Formal Aspects of Computing》2009,21(3):227-244
Program verification is usually done by adding specifications and invariants to the program and then proving that the verification
conditions are all true. This makes program verification an alternative to or a complement to testing. We describe here another
approach to program construction, which we refer to as invariant based programming, where we start by formulating the specifications and the internal loop invariants for the program, before we write the program
code itself. The correctness of the code is then easy to check at the same time as one is constructing it. In this approach,
program verification becomes a complement to coding rather than to testing. The purpose is to produce programs and software
that are correct by construction. We present a new kind of diagrams, nested invariant diagrams, where program specifications and invariants (rather than the control) provide the main organizing structure. Nesting of
invariants provide an extension hierarchy that allows us to express the invariants in a very compact manner. We have studied
the feasibility of formulating specifications and loop invariants before the code itself has been written in a number of case
studies. Our experience is that a systematic use of figures, in combination with a rough idea of the intended behavior of
the algorithm, makes it rather straightforward to formulate the invariants needed for the program, to construct the code around
these invariants and to check that the resulting program is indeed correct. We describe our experiences from using invariant
based programming in practice, both from teaching programmers how to construct programs that they prove correct themselves,
and from teaching invariant based programming for CS students in class.
D. A. Duce, J. Oliveira, P. Boca and R. Boute 相似文献
17.
TrustZone作为ARM处理器上的可信执行环境技术,为设备上安全敏感的程序和数据提供一个隔离的独立执行环境.然而,可信操作系统与所有可信应用运行在同一个可信环境中,任意组件上的漏洞被利用都会波及系统中的其他组件.虽然ARM提出了S-EL2虚拟化技术,支持在安全世界建立多个隔离分区来缓解这个问题,但实际分区管理器中仍可能存在分区间信息泄漏等安全威胁.当前的分区管理器设计及实现缺乏严格的数学证明来保证隔离分区的安全性.详细研究了ARM TrustZone多隔离分区架构,提出一种基于精化的TrustZone多安全分区建模与安全性分析方法,并基于定理证明器Isabelle/HOL完成了分区管理器的建模和形式化验证.首先,基于逐层精化的方法构建了多安全分区模型RMTEE,使用抽象状态机描述系统运行过程和安全策略要求,建立多安全分区的抽象模型并实例化实现分区管理器的具体模型,遵循FF-A规范在具体模型中实现了事件规约;其次,针对现有分区管理器设计无法满足信息流安全性验证的不足,设计了基于DAC的分区间通信访问控制,并将其应用到TrustZone安全分区管理器的建模与验证中;再次,证明了具体模型... 相似文献
18.
Proving pointer programs in higher-order logic 总被引:2,自引:0,他引:2
Building on the work of Burstall, this paper develops sound modelling and reasoning methods for imperative programs with pointers: heaps are modelled as mappings from addresses to values, and pointer structures are mapped to higher-level data types for verification. The programming language is embedded in higher-order logic. Its Hoare logic is derived. The whole development is purely definitional and thus sound. Apart from some smaller examples, the viability of this approach is demonstrated with a non-trivial case study. We show the correctness of the Schorr–Waite graph marking algorithm and present part of its readable proof in Isabelle/HOL. 相似文献
19.
基于Event-B方法的安全协议设计、建模与验证 总被引:1,自引:0,他引:1
随着软件精化验证方法以及Isabella/HOL、VCC等验证工具不断取得进展,研究者们开始采用精化方法和验证工具设计、建模安全协议和验证安全协议源程序的正确性.在介绍Event-B方法和验证工具Isabella/HOL、VCC的基础上,综述了基于Event-B方法的安全协议形式化设计、建模与源程序验证的典型研究工作,主要包括从需求规范到消息传递形式协议的安全协议精化设计、基于TPM(trusted platform module)的安全协议应用的精化建模以及从消息传递形式协议到代码的源程序精化验证. 相似文献
20.
智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台(Ethereum)上的智能合约暴露出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程序语言的形式化必不可少.本工作对以太坊中间语言Yul进行形式化,首次给出了其类型系统和小步操作语义的形式化定义.该语义为可执行语义(executable semantics),由120个Yul语言程序组成的测试集进行测试.本工作在Isabelle/HOL证明辅助工具中完成,为基于定理证明的智能合约正确性、安全性验证奠定了基础. 相似文献