A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle

We use the interactive theorem prover Isabelle to prove that the algebraic axiomatization of bisimulation equivalence in the pi-calculus is sound and complete. This is the first proof of its kind to be wholly machine checked. Although the result has been known for some time the proof had parts which needed careful attention to detail to become completely formal. It is not that the result was ever in doubt; rather, our contribution lies in the methodology to prove completeness and get absolute certainty that the proof is correct, while at the same time following the intuitive lines of reasoning of the original proof. Completeness of axiomatizations is relevant for many variants of the calculus, so our method has applications beyond this single result. We build on our previous effort of implementing a framework for the pi-calculus in Isabelle using the nominal data type package, and strengthen our claim that this framework is well suited to represent the theory of the pi-calculus, especially in the smooth treatment of bound names.     

A formal hierarchy of weak memory models

We present in this paper a formal generic framework, implemented in the Coq proof assistant, for defining and reasoning about weak memory models. We first present the three axioms of our framework, with several examples as illustration and justification. Then we show how to implement several existing weak memory models in our framework, and prove formally that our implementation is equivalent to the native definition for each of these models.     

The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective)

We show how to mechanise equational proofs about higher-order languages by using the primitive proof principles of first-order abstract syntax over one-sorted variable names. We illustrate the method here by proving (in Isabelle/HOL) a technical property which makes the method widely applicable for the λ-calculus: the residual theory of β is renaming-free up-to an initiality condition akin to the so-called Barendregt Variable Convention. We use our results to give a new diagram-based proof of the development part of the strong finite development property for the λ-calculus. The proof has the same equational implications (e.g., confluence) as the proof of the full property but without the need to prove SN. We account for two other uses of the proof method, as presented elsewhere. One has been mechanised in full in Isabelle/HOL.     

Strong normalization property for second order linear logic

The paper contains the first complete proof of strong normalization (SN) for full second order linear logic (LL): Girard’s original proof uses a standardization theorem which is not proven. We introduce sliced pure structures (sps), a very general version of Girard’s proof-nets, and we apply to sps Gandy’s method to infer SN from weak normalization (WN). We prove a standardization theorem for sps: if WN without erasing steps holds for an sps, then it enjoys SN. A key step in our proof of standardization is a confluence theorem for sps obtained by using only a very weak form of correctness, namely acyclicity slice by slice. We conclude by showing how standardization for sps allows to prove SN of LL, using as usual Girard’s reducibility candidates.     

Proving program inclusion using Hoare's logic

We explore conservative refinements of specifications. These form a quite appropriate framework for a proof theory for program inclusion based on a proof theory for program correctness.We propose two formalized proof methods for program inclusion and prove these to be sound. Both methods are incomplete but seem to cover most natural cases.     

An Observational Theory for Mobile Ad Hoc Networks (full version)

We propose a process calculus to study the behavioural theory of Mobile Ad Hoc Networks. The operational semantics of our calculus is given both in terms of a Reduction Semantics and in terms of a Labelled Transition Semantics. We prove that the two semantics coincide. The labelled transition system is then used to derive the notions of (weak) simulation and bisimulation for ad hoc networks. The labelled bisimilarity completely characterises reduction barbed congruence, a standard branching-time and contextually-defined program equivalence. We then use our (bi)simulation proof method to formally prove a number of non-trivial properties of ad hoc networks.     

Register allocation by proof transformation

This paper presents a proof-theoretical framework that accounts for the entire process of register allocation—liveness analysis is proof reconstruction (similar to type inference), and register allocation is proof transformation from a proof system with unrestricted variable accesses to a proof system with restricted variable access. In our framework, the set of registers acts as a “working set” of the live variables at each instruction step, which changes during the execution of the code. This eliminates the ad hoc notion of “spilling”. Memory–register moves are systematically incorporated in our proof transformation process. Its correctness is a direct corollary of our construction; the resulting proof is equivalent to the proof of the original code modulo treatment of structural rules. The framework serves as a basis for reasoning about formal properties of register allocation process, and it also yields a clean and systematic register allocation algorithm. The algorithm has been implemented, demonstrating the feasibility of the framework.     

Coloured Petri net refinement specification and correctness proof with Coq

In this work, we address the issue of the formal proof (using the proof assistant Coq) of refinement correctness for symmetric nets, a subclass of coloured Petri nets. We provide a formalisation of the net models, and of their type refinement in Coq. Then the Coq proof assistant is used to prove the refinement correctness lemma. An example adapted from a protocol example illustrates our work.     

UC安全性证明中模拟器构造方法研究

在UC模型(通用可组合安全分析模型)中密码协议安全性证明的难点是模拟器的构造,而目前模拟器的构造没有通用有效的方法可循,针对这一问题,提出了一种构造模拟器的通用有效的方法.研究了UC模型的构建原理,分析了UC安全性的本质要求,指出了符合UC安全性本质要求的模拟器存在条件以及模拟内容,在此基础上,阐述了构造模拟器的方法,并给出了该方法的正确性分析.为正确使用UC模型进行密码协议的UC安全性证明提供了切实可行的方法.     

Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks

Avoiding deadlock is crucial to interconnection networks. In ’87, Dally and Seitz proposed a necessary and sufficient condition for deadlock-free routing. This condition states that a routing function is deadlock-free if and only if its channel dependency graph is acyclic. We formally define and prove a slightly different condition from which the original condition of Dally and Seitz can be derived. Dally and Seitz prove that a deadlock situation induces cyclic dependencies by reductio ad absurdum. In contrast we introduce the notion of a waiting graph from which we explicitly construct a cyclic dependency from a deadlock situation. Moreover, our proof is structured in such a way that it only depends on a small set of proof obligations associated to arbitrary routing functions and switching policies. Discharging these proof obligations is sufficient to instantiate our condition for deadlock-free routing on particular networks. Our condition and its proof have been formalized using the ACL2 theorem proving system.     

Technology for testing nondeterministic client/server database applications

The execution of a client/server application involving database access requires a sequence of database transaction events (or, T-events), called a transaction sequence (or, T-sequence). A client/server database application may have nondeterministic behavior in that multiple executions thereof with the same input may produce different T-sequences. We present a framework for testing all possible T-sequences of a client/server database application. We first show how to define a T-sequence in order to provide sufficient information to detect race conditions between T-events. Second, we design algorithms to change the outcomes of race conditions in order to derive race variants, which are prefixes of other T-sequences. Third, we develop a prefix-based replay technique for race variants derived from T-sequences. We prove that our framework can derive all the possible T-sequences in cases where every execution of the application terminates. A formal proof and an analysis of the proposed framework are given. We describe a prototype implementation of the framework and present experimental results obtained from it.     

A Dichotomy for Real Weighted Holant Problems

Holant is a framework of counting characterized by local constraints. It is closely related to other well-studied frameworks such as the counting constraint satisfaction problem (#CSP) and graph homomorphism. An effective dichotomy for such frameworks can immediately settle the complexity of all combinatorial problems expressible in that framework. Both #CSP and graph homomorphism can be viewed as subfamilies of Holant with the additional assumption that the equality constraints are always available. Other subfamilies of Holant such as Holant^* and Holant ^c problems, in which we assume some specific sets of constraints to be freely available, were also studied. The Holant framework becomes more expressive and contains more interesting tractable cases with less or no freely available constraint functions, while, on the other hand, it also becomes more challenging to obtain a complete characterization of its time complexity. Recently, a complexity dichotomy for a variety of subfamilies of Holant such as #CSP, graph homomorphism, Holant^*, and Holant ^c for Boolean domain was proved. In this paper, we prove a dichotomy for the general Holant framework where all the constraints are real symmetric functions on Boolean inputs. This setting already captures most of the interesting combinatorial counting problems defined by local constraints, such as (perfect) matching. This is the first time a dichotomy is obtained for general Holant problems without any auxiliary functions. One benefit of working with the Holant framework is some powerful new reduction technique such as the holographic reduction. Along the proof of our dichotomy, we introduce a new reduction technique, namely realizing a constraint function by approximating it. This new technique is employed in our proof in a situation where it seems that all previous reduction techniques fail; thus, this new idea of reduction might also be of independent interest. Besides proving a dichotomy and developing a new technique, we also obtained some interesting by-products. We prove a dichotomy for #CSP, restricting to instances where each variable appears a multiple of d times for any d. We also prove that counting the number of Eulerian orientations on 2k-regular graphs is #P-hard for any \({k \geq 2}\).     

A Verified SAT Solver Framework with Learn,Forget, Restart,and Incrementality

We developed a formal framework for conflict-driven clause learning (CDCL) using the Isabelle/HOL proof assistant. Through a chain of refinements, an abstract CDCL calculus is connected first to a more concrete calculus, then to a SAT solver expressed in a functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis–Putnam–Logemann–Loveland (DPLL) calculus. The imperative program relies on the two-watched-literal data structure and other optimizations found in modern solvers. We used Isabelle’s Refinement Framework to automate the most tedious refinement steps. The most noteworthy aspects of our work are the inclusion of rules for forget, restart, and incremental solving and the application of stepwise refinement.     

Projective Visual Hulls

This article presents a novel method for computing the visual hull of a solid bounded by a smooth surface and observed by a finite set of cameras. The visual hull is the intersection of the visual cones formed by back-projecting the silhouettes found in the corresponding images. We characterize its surface as a generalized polyhedron whose faces are visual cone patches; edges are intersection curves between two viewing cones; and vertices are frontier points where the intersection of two cones is singular, or intersection points where triples of cones meet. We use the mathematical framework of oriented projective differential geometry to develop an image-based algorithm for computing the visual hull. This algorithm works in a weakly calibrated setting–-that is, it only requires projective camera matrices or, equivalently, fundamental matrices for each pair of cameras. The promise of the proposed algorithm is demonstrated with experiments on several challenging data sets and a comparison to another state-of-the-art method.     

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.     

A note on an identity-based ring signature scheme with signer verifiability

Recently, Herranz presented an identity-based ring signature scheme featuring signer verifiability where a signer can prove that he or she is the real signer by releasing an authorship proof. In this paper we show that this scheme is vulnerable to a key recovery attack in which a user’s secret signing key can be efficiently recovered through the use of two known ring signatures and their corresponding authorship proofs. In addition, we present a simple method to fix this security vulnerability by slightly modifying the authorship proof. Our modified scheme simplifies the original scheme and improves performance. To show that the modified scheme is unforgeable, we define two types of unforgeability notions for both signatures and authorship proofs. In these notions an adversary has opening capability to confirm the real signers of ring signatures and thus can manipulate authorship proofs in an adaptive way. We then prove that our modified scheme is secure in terms of these unforgeability notions.     

On the Comparison of Proof Planning Systems: , Ωmega and IsaPlanner

We present a framework for describing proof planners. This framework is based around a decomposition of proof planners into planning states, proof language, proof plans, proof methods, proof revision, proof control and planning algorithms.We use this framework to motivate the comparison of three recent proof planning systems, λCLaM, Ωmega and IsaPlanner, and demonstrate how the framework allows us to discuss and illustrate both their similarities and differences in a consistent fashion. This analysis reveals that proof control and the use of contextual information in planning states are key areas in need of further investigation.     

Concurrent Maintenance of Rings

A central problem for structured peer-to-peer networks is topology maintenance, that is, how to properly update neighbor variables when nodes join or leave the network, possibly concurrently. In this paper, we consider the maintenance of the ring topology, the basisof several peer-to-peer networks, in the fault-free environment. We design, and prove the correctness of, protocols that maintain a bidirectional ring under both joins and leaves. Our protocols update neighbor variables once a membership change occurs. We prove the correctness of our protocols using an assertional proof method, that is, we first identify a global invariant for a protocol and then show that every action of the protocol preserves the invariant. Our protocols are simple and our proofs are rigorous and explicit.Li and Plaxton are supported by the National Science Foundation Grant CCR–0310970. Misra is supported by the National Science Foundation Grant CCR–0204323     

Fundamentals of deductive program synthesis

An informal tutorial for program synthesis is presented, with an emphasis on deductive methods. According to this approach, to construct a program meeting a given specification, the authors prove the existence of an object meeting the specified conditions. The proof is restricted to be sufficiently constructive, in the sense that, in establishing the existence of the desired output, the proof is forced to indicate a computational method for finding it. That method becomes the basis for a program that can be extracted from the proof. The exposition is based on the deductive-tableau system, a theorem-proving framework particularly suitable for program synthesis. The system includes a nonclausal resolution rule, facilities for reasoning about equality, and a well-founded induction rule