MoNoC: A monitored network on chip with path adaptation mechanism

Complex systems on chip containing dozens of processing resources with critical communication requirements usually rely on the use of networks on chip (NoCs) as communication infrastructure. NoCs provide significant advantages over simpler infrastructures such as shared busses or point to point communication, including higher scalability, more efficient energy management, higher bandwidth and lower average latency. Applications running on NoCs with more than 10% of bandwidth usage attest that the most significant portion of message latencies refers to buffered packets waiting to enter the NoC, whereas the latency portion that depends on the packet traversing the NoC is sometimes negligible. This work presents an adaptive routing architecture, named Monitored NoC (MoNoC), which is based on a traffic monitoring mechanism and the exchange of high priority control packets. This method enables to adapt paths by choosing less congested routes. Practical experiments show that the proposed path adaptation is a fast process, enabling to transmit packets with smaller latencies, up to 9 times smaller, by using non-congested NoC regions.     

The formalization and analysis of a communications protocol

The MSMIE protocol [SBC89] allows processors in a distributed system to communicate via shared memory. It was designed to meet the reliability and efficiency needs of applications such as nuclear safety systems. We present a formal model of the MSMIE protocol expressed in the notation CCS. Desirable properties of the protocol are expressed in the modal mu-calculus, an expressive modal logic. We show that the protocol lacks an important liveness property. In actual operation, additional operating constraints are checked to avoid potential problems. We present a modified protocol and show that it possesses the liveness property even without checking operating constraints. We also show how parts of the analysis were automated with the Concurrency Workbench.     

Easy intruder deduction problems with homomorphisms

We present complexity results for the verification of security protocols. Since the perfect cryptography assumption is unrealistic for cryptographic primitives with visible algebraic properties, we extend the classical Dolev-Yao model by permitting the intruder to exploit these properties. More precisely, we are interested in theories such as Exclusive or and Abelian groups in combination with the homomorphism axiom. We show that the intruder deduction problem is in PTIME in both cases, improving the EXPTIME complexity results of Lafourcade, Lugiez and Treinen.     

Theorem proving in technology transfer: the user’s point of view

The aim of this paper is to discuss the potentials, problems and critical factors for the industrial usage of mechanized theorem proving. The approach followed in this paper is somehow unusual. The starting point is the results of an industrial project whose goal was the assessment of the state of the art of provers (and of tools supporting formal methods in general). We describe the project results in terms of evaluation criteria, classification of technologies and tools and critical factors for industrial take-up. We present the results of the assessment in the same spirit, the same kind of analysis and even the same terminology which were used in the presentations and in the deliverables of the project. This should result in a presentation of a “different view” of the problem of technology transfer in theorem proving, that we call the “user’s point of view”. In this way, we hope to give a new perspective in the discussion of the industrial take-up of the theorem proving technology.     

Automated proofs of equality problems in Overbeek's competition

This paper reports the detailed computer proofs of nine equality problems in Overbeek's competition obtained by Herky, a completion-based theorem prover developed by the author. Advanced techniques implemented in Herky made it a high-performance theorem prover for equational reasoning. Herky is able to prove the first nine of the ten equality problems in the competition (the tenth is an open problem). These equality problems are likely to serve as good exercises for theorem provers based on different approaches, and the proofs of these problems may help people to solve them using their own theorem provers.     

A verification tool for ERLANG

This paper presents an overview of the main results of the project Verification of ERLANG Programs , which is funded by the Swedish Business Development Agency (NUTEK) and by Ericsson within the ASTEC (Advanced Software TEChnology) initiative. Its main outcome is the ERLANG Verification Tool (EVT), a theorem prover which assists in obtaining proofs that ERLANG applications satisfy their correctness requirements formulated as behavioural properties in a modal logic with recursion. We give a summary of the verification framework as supported by EVT, discuss reasoning principles essential for successful proofs such as inductive and compositional reasoning, and an efficient treatment of side-effect-free code. The experiences of applying the tool in an industrial case study are summarised, and an approach for supporting verification in the presence of program libraries is outlined.EVT is essentially a classical proof assistant, or theorem-proving tool, requiring users to intervene in the proof process at crucial steps such as stating program invariants. However, the tool offers considerable support for automatic proof discovery through higher-level tactics tailored to the particular task of the verification of ERLANG programs. In addition, a graphical interface permits easy navigation through proof tableaux, proof reuse, and meaningful feedback about the current proof state, to assist users in taking informed proof decisions.     

A prolog technology theorem prover: Implementation by an extended prolog compiler

A Prolog technology theorem prover (PTTP) is an extension of Prolog that is complete for the full first-order predicate calculus. It differs from Prolog in its use of unification with the occurs check for soundness, the model-elimination reduction rule that is added to Prolog inferences to make the inference system complete, and depth-first iterative-deepening search instead of unbounded depthfirst search to make the search strategy complete. A Prolog technology theorem prover has been implemented by an extended Prolog-to-LISP compiler that supports these additional features. It is capable of proving theorems in the full first-order predicate calculus at a rate of thousands of inferences per second.This is a revised and expanded version of a paper presented at the 8th International Conference on Automated Deduction, Oxford, England, July 1986.This research was supported by the Defense Advanced Research Projects Agency under Contract N00039-84-K-0078 with the Naval Electronic Systems Command and by the National Science Foundation under Grant CCR-8611116. The views and conclusions contained herein are those of the author and should not be interpreted as necessarily representing the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency, the National Science Foundation, or the United States government. Approved for public release. Distribution unlimited.     

Condensed detachment is complete for relevance logic: A computer-aided proof

The condensed detachment ruleD is a combination of modus ponens with a minimal amount of substitution. EarlierD has been shown to be complete for intuitionistic and classical implicational logic but incomplete forBCK andBCI logic. We show thatD is complete for the relevance logic. One of the main steps is the proof of the formula ((a a) a) a found in interaction with our resolution theorem prover. Various strategies of generating consequences of the axioms and choosing best ones for the next iteration were tried until the proof was found.     

An integral theorem prover and the role of proof planning

An investigation is made into the ways proof planning can enhance the capability of a rule based prover for the theory of integration. The integrals are of the Riemann type and are defined in a way to maximize the theorem proving methods of predicate calculus. Approximately fifty theorems have been proved and several examples are discussed. A major shortcoming was found to be the inability of the system to work with or produce a proof plan. As a result, a planning scheme based on the idea of subgoals or milestones was considered. With user defined plans, there was a substantial increase in performance and capability of the system and, in some cases, proofs which were previously unsuccessful were completed.     

A new reduction rule for the connection graph proof procedure

A new reduction rule is introduced for the connection graph proof procedure proposed by Kowalski in 1975. The new rule considers sets of values which clause variables may take. Application of the rule often leads to massive removals of links. A proof system in which the new rule is included has successfully been implemented in PROLOG. The performance of this system is compared to other resolution based proof systems. Also, the new rule is related to order-sorted logic.     

Formalizing non-interference for a simple bytecode language in Coq

In this paper, we describe the application of the interactive theorem prover Coq to the security analysis of bytecode as used in Java. We provide a generic specification and proof of non-interference for bytecode languages using the Coq module system. We illustrate the use of this formalization by applying it to a small subset of Java bytecode. The emphasis of the paper is on modularity of a language formalization and its analysis in a machine proof. C. B. Jones     

Productive use of failure in inductive proof

Proof by mathematical induction gives rise to various kinds of eureka steps, e.g., missing lemmata and generalization. Most inductive theorem provers rely upon user intervention in supplying the required eureka steps. In contrast, we present a novel theorem-proving architecture for supporting the automatic discovery of eureka steps. We build upon rippling, a search control heuristic designed for inductive reasoning. We show how the failure if rippling can be used in bridging gaps in the search for inductive proofs. The research reported in this paper was supported by EPSRC grant GR/J/80702 and ARC grant 438.     

Short proofs of the pigeonhole formulas based on the connection method

Quadratic proofs of pigeonhole formulas are presented using connection method proof techniques. The interest of this result derives from the fact that for this class of formulas exponential lower bounds are known for the length of resolution refutations.     

Energy reduction through crosstalk avoidance coding in networks on chip

Commercial designs are currently integrating from 10 to 100 embedded processors in a single system on chip (SoC) and the number is likely to increase significantly in the near future. With this ever increasing degree of integration, design of communication architectures for large, multi-core SoCs is a challenge. Traditional bus-based systems will no longer be able to meet the clock cycle requirements of these big SoCs. Instead, the communication requirements of these large multi processor SoCs (MP-SoCs) are convened by the emerging network-on-chip (NoC) paradigm. Crosstalk between adjacent wires is an important signal integrity issue in NoC communication fabrics and it can cause timing violations and extra energy dissipation. Crosstalk avoidance codes (CACs) can be used to improve the signal integrity by reducing the effective coupling capacitance, lowering the energy dissipation of wire segments. As NoCs are built on packet-switching, it is advantageous to modify data packets by including coded bits to protect against the negative effects of crosstalk. By incorporating crosstalk avoidance coding in NoC data streams and organizing the CAC-encoded data packets in an efficient manner, so that total number of encoding/decoding operations can be reduced over the communication channel, we are able to achieve lower communication energy, which in turn will help to decrease the overall energy dissipation.     

A Complete Mechanization of Correctness of a String-Preprocessing Algorithm

We report on mechanization of a correctness proof of a string-preprocessing algorithm. This preprocessing algorithm is employed in Boyer-Moore’s pattern matching algorithm. The mechanization is carried out using the PVS system. The correctness proof being mechanized has been formulated in Linear Time Temporal Logic. It consists of fourteen lemmata which are related to safety properties and two additional lemmata dealing with liveness properties. The entire mechanization of the safety and liveness parts has been completed. Several small errors and omissions were found in the handwritten proof and corrected. Yet, the manual correctness proof of the string-preprocessing algorithm was found to satisfy the usual mathematical validity. We conclude that the string-preprocessing algorithm in Boyer-Moore’s pattern matching algorithm, corrected a number of times because of flaws, does not contain any more undiscovered errors. An extended abstract of this work appears in the Proceedings of the 8^th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS ‘02).     

片上网络

对片上网络的发展趋势进行了探讨,总结了它的技术特点,并着重分析了片上网络的体系结构。片上网络将继片上系统之后引发微电子领域的又一次革命。     

函数矩阵及其微积分的高阶逻辑形式化

函数矩阵广泛应用于动态系统的建模与分析。传统的函数矩阵分析主要采用纸笔演算、数值计算和符号推导的方法,这些方法不能保证提供精确或正确的结果。高阶逻辑定理证明作为一种高可靠的形式化验证方法,可以克服以上不足。在高阶逻辑定理证明器HOL4中对函数向量和函数矩阵相关理论进行形式化,内容包括函数向量和函数矩阵及其连续性、微分、积分的形式化定义和相关性质的逻辑推理证明。为示范函数矩阵形式化的应用,最后给出机器人运动学中旋转矩阵微分公式的形式化验证。     

A note on assumptions about Skolem functions

Skolemization is not an equivalence preserving transformation. For the purposes of refutational theorem proving it is sufficient that skolemization preserves satisfiability and unsatisfiability. Therefore there is sometimes some freedom in interpreting Skolem functions in a particular way. We show that in certain cases it is possible to exploit this freedom for simplifying formulae considerably. Examples for cases where this occurs systematically are the relational translation from modal logics to predicate logic and the relativization of first-order logics with sorts.