Verification of clock synchronization algorithms: experiments on a combination of deductive tools

We report on an experiment in combining the theorem prover Isabelle with automatic first-order arithmetic provers to increase automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock synchronization algorithms. We present a formalization of Schneider’s generalized clock synchronization protocol [Sch87] in Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [LMS85] and the Fault-tolerant Midpoint algorithm of Lundelius–Lynch [LL84], satisfy Schneider’s general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be handled by automatic first-order provers with support for arithmetics.     

Predicate abstraction in a program logic calculus

Predicate abstraction is a form of abstract interpretation where the abstract domain is constructed from a finite set of predicates over the variables of the program. This paper explores a way to integrate predicate abstraction into a calculus for deductive program verification based on symbolic execution, where it allows us to infer loop invariants automatically that would otherwise have to be given interactively. The approach has been implemented as a part of the KeY verification system.     

Proof by analogy in mural

An important advantage of using a formal method of developing software is that one can prove that development steps are correct with respect to their specification. Conducting proofs by hand, however, can be time consuming to the extent that designers have to judge whether a proof of a particular obligation is worth conducting. Even if hand proofs are worth conducting, how do we know that they are correct? One approach to overcoming this problem is to use an automatic theorem proving system to develop and check our proofs. However, in order to enable present day theorem provers to check proofs, one has to conduct them in much more detail than hand proofs. Carrying out more detailed proofs is of course more time consuming. This paper describes the use of proof by analogy in an attempt to reduce the time spent on proofs. We develop and implement a proof follower based on analogy and present an example to illustrate its characteristics. The example shows that even when the follower fails to complete a proof, it can provide a hint that enables the user to complete a proof.     

Tractability through symmetries in propositional calculus

Many propositional calculus problems — for example the Ramsey or the pigeon-hole problems — can quite naturally be represented by a small set of first-order logical clauses which becomes a very large set of propositional clauses when we substitute the variables by the constants of the domainD. In many cases the set of clauses contains several symmetries, i.e. the set of clauses remains invariant under certain permutations of variable names. We show how we can shorten the proof of such problems. We first present an algorithm which detects the symmetries and then we explain how the symmetries are introduced and used in the following methods: SLRI, Davis and Putnam and semantic evaluation. Symmetries have been used to obtain results on many known problems, such as the pigeonhole, Schur's lemma, Ramsey's, the eight queen, etc. The most interesting one is that we have been able to prove for the first time the unsatisfiability of Ramsey's problem (17 vertices and three colors) which has been the subject of much research.     

A Graphical User Interface for Formal Proofs in Geometry

We present in this paper the design of a graphical user interface to deal with proofs in geometry. The software developed combines three tools: a dynamic geometry software to explore, measure, and invent conjectures; an automatic theorem prover to check facts; and an interactive proof system (Coq) to mechanically check proofs built interactively by the user.     

Completeness issues in RUE-NRF deduction: The undecidability of viability

We show that the algorithm directly induced by the viability definition in Ref. [4] does not terminate in general. As a consequence, RUE-resolution in strong form is not complete. Moreover, we show that ground query processing forcovered pure logic programs can be reduced to computing viability. Since the problem of ground query processing is strictly recursively enumerable even under the above restrictions, it follows that the notion of viability is undecidable. Finally, we present a modified viability check that solves the non-termination problem for ground terms.Work supported in part by NSF grants IRI-9015251 and IRI-9109755 and by Army Research office grant DAAL-03-92-G-0225.     

Using induction and rewriting to verify and complete parameterized specifications

In software engineering there is a growing demand for formal methods for the specification and validation of software systems. The formal development of a system might give rise to many proof obligations. We must prove the completeness of the specification and the validity of some inductive properties. In this framework, many provers have been developed. However they require much user interaction even for simple proof tasks. In this paper, we present new procedures to test sufficient completeness and to prove or disprove inductive properties automatically in para-meterized conditional specifications. The method has been implemented in the prover SPIKE. Computer experiments illustrate the improvements in length and structure of proofs, due to parameterization. Moreover, SPIKE offers facilities to check and complete specifications.     

Ant algorithms and simulated annealing for multicriteria dynamic programming

The paper presents a comparison of ant algorithms and simulated annealing as well as their applications in multicriteria discrete dynamic programming. The considered dynamic process consists of finite states and decision variables. In order to describe the effectiveness of multicriteria algorithms, four measures of the quality of the nondominated set approximations are used.     

Term rewriting and beyond — theorem proving in Isabelle

The subject of this paper is theorem proving based on rewriting and induction. Both principles are implemented as tactics within the generic theorem prover Isabelle. Isabelle's higher-order features enable us to go beyond first-order rewriting and express rewriting with conditionals, induction schemata, higher-order functions and program transformers. Applications include the verification and transformation of functional versions of insertion sort and quicksort.     

A class of deadlock-free Maekawa-type algorithms for mutual exclusion in distributed systems

Maekawa-type mutual exclusion algorithms use locking of a set of sites to achieve mutual exclusion. These algorithms are prone to deadlocks because a site is locked by other sites in exclusive mode and the timestamp of requests is not used to order requests while granting locks. These algorithms require additional rounds of message exchanges, like INQUIRE and FAILED, to recover from a possible deadlock. In this paper we present a class of Maekawa-type mutual exclusion algorithms which are free from deadlocks and do not exchange additional messages to resolve deadlocks. We systematically point out the reasons for deadlocks in Maekawa-type algorithms and eliminate them one by one to give a class of Maekawa-type algorithms which are free from deadlocks. It turns out that to prevent deadlocks in Maekawa-type algorithms, locks on sites must be mutable, timestamps must be used judiciously, and communication among sites must be increased. A deadlock-free Maekawa-type algorithm is optimal when the request sets of sites are the smallest possible such that a correctness condition is satisfied. We state the condition of optimality and present a method to construct optimal request sets. We also give a swap operation which allows us to derive an optimal configuration of request sets from another optimal configuration. There are large number of optimal configurations of request sets, which define a class of optimal deadlock-free Maekawa-type algorithms. Freedom from deadlocks is a desirable property because it dispenses with the need of cumbersome deadlock recovery scheme (e.g., exchange of INQUIRE, FAILED, and YIELD messages). Freedom from deadlock has another benefit: simplicity of the implementation. Mukesh Singhal was born in India on May 8, 1959. He received Bachelor of Engineering degree in Electronics and Communication Engineering with high distinction from University of Roorkee, Roorkee, India, in 1980. He jointed the Department of Computer Science, University of Maryland, College Park, in January 1981, where he obtained Ph.D. degree in May 1986 for his work in the design and analysis of concurrency control algorithms in distributed database systems. Since February 1986, he has been a faculty of Computer & Information Science at the Ohio State University, Columbus. From 1981 to 1985, he served as a Teaching/Research Assistant and Instructor at the Department of Computer Science, University of Maryland, College Park. His current research interests include distributed systems, distributed databases, and performance modeling.     

On subsumption in distributed derivations

In this paper we study the subsumption inference rule in the context of distributed deduction. It is well known that the unrestricted application of subsumption may destroy the fairness and thus the completeness of a deduction strategy. Solutions to this problem in sequential theorem proving are known. We observe that in distributed automated deduction, subsumption may also thwartmonotonicity, a dual property of soundness, in addition to completeness. Not only do the solutions for the sequential case not apply, even proper subsumption may destroy monotonicity in the distributed case.We present these problems and propose a general solution that treats subsumption as a composition of a replacement inference rule,replacement subsumption, and a deletion inference rule,variant subsumption. (Proper subsumption, in this case, becomes a derived inference rule.) We define a newdistributed subsumption inference rule, which has all the desirable properties: it allows subsumption, including subsumption of variants, in a distributed derivation, while preserving fairness and monotonicity. It also works in both sequential and distributed environments.We conclude the paper with some discussion of the different behavior of subsumption in different architectures.     

Multi-objective evolutionary algorithms for energy-aware scheduling on distributed computing systems

The ongoing increase of energy consumption by IT infrastructures forces data center managers to find innovative ways to improve energy efficiency. The latter is also a focal point for different branches of computer science due to its financial, ecological, political, and technical consequences. One of the answers is given by scheduling combined with dynamic voltage scaling technique to optimize the energy consumption. The way of reasoning is based on the link between current semiconductor technologies and energy state management of processors, where sacrificing the performance can save energy.This paper is devoted to investigate and solve the multi-objective precedence constrained application scheduling problem on a distributed computing system, and it has two main aims: the creation of general algorithms to solve the problem and the examination of the problem by means of the thorough analysis of the results returned by the algorithms.The first aim was achieved in two steps: adaptation of state-of-the-art multi-objective evolutionary algorithms by designing new operators and their validation in terms of performance and energy. The second aim was accomplished by performing an extensive number of algorithms executions on a large and diverse benchmark and the further analysis of performance among the proposed algorithms. Finally, the study proves the validity of the proposed method, points out the best-compared multi-objective algorithm schema, and the most important factors for the algorithms performance.     

基于中间表示的可复用程序分析系统

采用一种语言独立AST中间格式以便把程序的分析算法同编译器内部表示分离,利用这种格式设计与实现了Compiler Auxiliary Toolkit(COA)系统框架。COA可同时应用于静态分析算法和动态分析算法。在介绍了COA框架之后,用实例说明了如何利用COA框架进行函数调用图生成算法的静态分析和循环不变量的动态分析。     

Effective homology of bicomplexes, formalized in Coq

In this paper, we present a complete formalization in the Coq theorem prover of an important algorithm in computational algebra, namely the calculation of the effective homology of a bicomplex. As a necessary tool, we encode a hierarchy of algebraic structures in constructive type theory, including graded and infinite data structures. The experience shows how some limitations of the Coq proof assistant to deal with this kind of algebraic data can be overcome by applying a separation of concerns principle; more concretely, we propose to distinguish in the representation of an algebraic structure (such as a group or a module) a behavioural part, containing operation signatures and axioms, and a structural part determining if the algebraic data is free, of finite type and so on.     

动静结合的攻击代码检测方法

缓冲区溢出攻击是近年来最主要的安全问题之一,攻击者利用缓冲区溢出漏洞执行远程代码,从而达到攻击的目的。Shelleode作为攻击的载体,是缓冲区攻击检测的主要对象。随着检测技术的发展,攻击者更倾向于使用多态技术对Shellcode进行加密来绕过IDS的检测。针对MS Windows操作系统下的Shellcode,提出了一种将静态检测和动态执行相结合的新的攻击代码检测方法。在判断依据上做了新的定义,既使用动态模拟技术提高了对使用多态技术的Shellcode的检侧率,也兼顾了检测的效率。基于该方法,设计和实现了一套原型系统,并进行了检测率、误报率和吞吐率等方面的测试。测试结果表明,该系统在检测Shellcode的准确率和性能方面都达到了令人满意的效果。     

基于模拟退火支持向量机的入侵检测系统

为了提高入侵检测系统在小样本集条件下的检测效率,将支持向量机用于网络入侵检测.支持向量机的参数决定了检测效率,然而难以选择合适的参数值,因此提出利用模拟退火算法来优化这些参数,并设计出基于参数优化的支持向量机用于入侵检测.通过对样本数据集中的样本进行实验性检测,并与原始支持向量机入侵检测系统进行比较,结果表明模拟退火支持向量机入侵检测系统检测率高、误报率低,并且缩短了训练时间和检测时间.     

Intelligent backtracking in deduction systems by means of extended unification graphs

A method for unification as the basis for intelligent backtracking in deduction systems is described. This method is based on the unification graphs introduced by Cox. In this paper, unification graphs are used in an extended form such that they represent all the information which can be gained from the unification constraints, i.e., the expression to be unified, their subterms which, as a consequence, are to be unified, the number of deduction steps which cause the unification of two terms, and the term-subterm relation as far as necessary. If a unification conflict occurs from this information, the deduction steps which have led to these conflicts can be determined and reset. This is done by searching for loop-free paths or loops with certain properties in the extended unification graph, according to the type of unification conflict. Algorithms for the handling of the unification graph and for the extraction information from it are described and proved as correct.     

基于二进制代码的缓冲区溢出检测研究

随着Internet 应用的广泛深入,计算机系统的安全问题日益引起人们的重视,其中,缓冲区溢出漏洞攻击的数量呈逐年上升之势。该文从缓冲区溢出的原理开始,描述了一种利用静态分析和动态分析相结合的基于二进制代码的缓冲区溢出分析检测技术及工具,比较和分析了该工具检测二进制代码的结果与传统工具检测对应源程序的结果,并提出了存在的不足和改进之处。