Search

We present a solution to the P oplM ark challenge designed by Aydemir et al., which has as a goal the formalization of the meta-theory of System $\hbox{F}_{<:}$. The formalization is carried out in the theorem prover Isabelle/HOL using an encoding based on de Bruijn indices. We start with a relatively simple formalization covering only the basic features of System $\hbox{F}_{<:}$, and explain how it can be extended to also cover records and more advanced binding constructs. We also discuss different styles of formalizing the evaluation relation, and how this choice influences executability of the specification. [ABSTRACT FROM AUTHOR]

This paper is a report about the use of Matita, an interactive theorem prover under development at the University of Bologna, for the solution of the POPLmark Challenge, part 1a. We provide three different formalizations, including two direct solutions using pure de Bruijn and locally nameless encodings of bound variables, and a formalization using named variables, obtained by means of a sound translation to the locally nameless encoding. According to this experience, we also discuss some of the proof principles used in our solutions, which have led to the development of a generalized inversion tactic for Matita. [ABSTRACT FROM AUTHOR]

It is well known that many relevant aspects of everyday reasoning based on natural language cannot be adequately expressed in classical first-order logic. In this paper we address two of the problems, firstly that of so-calledpresuppositions, expressions from which it is possible to draw implicit conclusions, which classical logic normally does not warrant, and secondly the problem ofpartialityand the adequate treatment of undefined expressions. In natural language, presuppositions are quite common; however, they cannot be sufficiently modelled in classical first-order logic. For instance, in the case of universal restricted quantification in natural language it is typically presupposed that these restrictions are non-empty, whereas in classical logic it is only assumed that the whole universe is non-empty. Conversely, all constants mentioned in classical logic are presupposed to denote something, while it creates no problems to speak about hypothetical objects in everyday language. Similarly, undefined expressions can be handled in natural language discourses, and utterances are not only classified into the two categories ‘true’ and ‘false’. This has led to the development of various better-suited many-valued logics. By combining different approaches we can now give astaticdescription of presuppositions and undefinedness within the same framework. Additionally, we have developed an efficient mechanisation of the induced consequence relation by combining methods from many-valued truth-functional logics and sort techniques developed for search control in automated theorem proving. [ABSTRACT FROM AUTHOR]

This note discusses P. Oppenheimer and E. Zalta's ‘A Computationally-Discovered Simplification of the Ontological Argument’ [this journal, 2011]. I try to explain why the simplification presented there was successful and comment on the technical aspects of the method they applied. [ABSTRACT FROM PUBLISHER]

Administrative Role Based Access Control (ARBAC) is one of the most widespread framework for the management of access-control policies. Several automated analysis techniques have been proposed to help maintaining desirable security properties of ARBAC policies. One of the main limitation of available analysis techniques is that the set of users is bounded. In this paper, we propose a symbolic framework to overcome this limitation. We design an automated analysis technique that can handle both a bounded and an unbounded number of users by adapting recent methods for the symbolic model checking of infinite state systems that use first-order logic and SMT solving techniques. An extensive experimental evaluation confirms the scalability of the proposed technique. [ABSTRACT FROM AUTHOR]

Copyright of Revista Educación en Ingeniería is the property of Asociacion Colombiana de Facultades de Ingenieria and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)

We study the extension of public announcement logic PAL by public assignments, which we call PALA. Just as in the case of PAL, the standard procedure for deciding PALA validity, i.e. the use of so-called reduction axioms to translate PALA formulae into formulae in epistemic logic EL, may lead to exponential growth. In this paper, we show that such a price is not mandatory, for we provide a polynomial translation of PALA into EL. This is based on abbreviations of subformulae by new propositional letters. Such optimal translation also enables us to show the computational complexity of the problem of deciding PALA validity, which turns out to be coNP-complete in the single-agent case and PSPACE-complete in the multiagent case. [ABSTRACT FROM AUTHOR]

Abstract: Theorems offer a rarity in biology, a guarantee that something will always be true if certain conditions are met. We show that modeling and theorem proving are distinct while playing mutually supporting roles in understanding cellular phenomena. Using two recently proven theorems from systems biology as examples, we demonstrate that theorems are not an alternative to mechanistic models. Rather, theorem proving, in conjunction with conventional mathematical (mechanistic) modeling, is an essential tool for a deeper understanding in systems biology. [Copyright &y& Elsevier]

The area method for Euclidean constructive geometry was proposed by Chou, Gao and Zhang in the early 1990's. The method can efficiently prove many non-trivial geometry theorems and is one of the most interesting and most successful methods for automated theorem proving in geometry. The method produces proofs that are often very concise and human-readable. In this paper, we provide a first complete presentation of the method. We provide both algorithmic and implementation details that were omitted in the original presentations. We also give a variant of Chou, Gao and Zhang's axiom system. Based on this axiom system, we proved formally all the lemmas needed by the method and its soundness using the Coq proof assistant. To our knowledge, apart from the original implementation by the authors who first proposed the method, there are only three implementations more. Although the basic idea of the method is simple, implementing it is a very challenging task because of a number of details that has to be dealt with. With the description of the method given in this paper, implementing the method should be still complex, but a straightforward task. In the paper we describe all these implementations and also some of their applications. [ABSTRACT FROM AUTHOR]

An abstract file system is defined here as a partial function from (absolute) paths to data. Such a file system determines the set of valid paths. It allows the file system to be read and written at a valid path, and it allows the system to be modified by the Unix operations for creation, removal, and moving of files and directories. We present abstract definitions (axioms) for these operations. This specification is refined towards a pointer implementation. The challenge is to have a natural abstraction function from the implementation to the specification, to define operations on the concrete store that behave exactly in the same way as the corresponding functions on the abstract store, and to prove these facts. To mitigate the problems attached to partial functions, we do this in two steps: first a refinement towards a pointer implementation with total functions, followed by one that allows partial functions. These two refinements are proved correct by means of a number of invariants. Indeed, the insights gained consist, on the one hand, of the invariants of the pointer implementation that are needed for the refinement functions, and on the other hand of the precise enabling conditions of the operations on the different levels of abstraction. Each of the three specification levels is enriched with a permission system for reading, writing, or executing, and the refinement relations between these permission systems are explored. Files and directories are distinguished from the outset, but this rarely affects our part of the specifications. All results have been verified with the proof assistant PVS, in particular, that the invariants are preserved by the operations, and that, where the invariants hold, the operations commute with the refinement functions. [ABSTRACT FROM AUTHOR]

Invariant based programming is an approach where we start to construct a program by first identifying the basic situations (pre- and post-conditions as well as invariants) that could arise during the execution of the algorithm. These situations are identified before any code is written. After that, we identify the transitions between the situations, which will give us the flow of control in the program. Data refinement is a technique of building correct programs working on concrete data structures as refinements of more abstract programs working on abstract data types. We study in this paper data refinement for invariant based programs and we apply it to the construction of the classical Deutsch-Schorr-Waite graph marking algorithm. Our results are formalized and mechanically proved in the Isabelle/HOL theorem prover. [ABSTRACT FROM AUTHOR]

The CADE ATP System Competition (CASC) is an annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-23 was the sixteenth competition in the CASC series. Thirty-six ATP systems and system variants competed in the various competition and demonstration divisions. An outline of the competition design, and a commentated summary of the results, are presented. [ABSTRACT FROM AUTHOR]

I continue the discussion initiated in part I (published in this journal in 2007) of whether or not computer-assisted proofs are a promising approach to preventing errors in reductionist security arguments. I examine some recent papers that describe automated security proofs for hashed ElGamal encryption, Boneh-Franklin identity-based encryption, and OAEP. [ABSTRACT FROM AUTHOR]

The first-order theory of a string automatic structure is known to be decidable, but there are examples of string automatic structures with nonelementary first-order theories. We prove that the first-order theory of a string automatic structure of bounded degree is decidable in doubly exponential space (for injective automatic presentations, this holds even uniformly). This result is shown to be optimal since we also present a string automatic structure of bounded degree whose first-order theory is hard for 2EXPSPACE. We prove similar results also for tree automatic structures. These findings close the gaps left open in [28] by improving both the lower and the upper bounds. [ABSTRACT FROM AUTHOR]

Abstract: ZigBee is a specification that enhances the IEEE 802.15.4 standard by adding network and security layers and an application framework for high level communication in Wireless Sensor Networks (WSN). Since ZigBee is essential in the operation of WSN; it is imperative to verify the correctness of its design. Formal methods can be used efficiently to verify a wide range of systems, including ZigBee protocol stack specification. In this paper we use Event-B formal verification method to model and verify ZigBee protocol stack by providing embedding of the protocol primitives in Event-B. Our approach takes advantage of the Event-B method capabilities to model designs at different levels of abstraction which fits the layered nature of the protocol. [Copyright &y& Elsevier]

In this article we use the decreasing diagrams technique to show that a left-linear and locally confluent term rewrite system $\mathcal{R}$ is confluent if the critical pair steps are relatively terminating with respect to $\mathcal{R}$. We further show how to encode the rule-labeling heuristic for decreasing diagrams as a satisfiability problem. Experimental data for both methods are presented. [ABSTRACT FROM AUTHOR]

While many higher-order interactive theorem provers include a choice operator, higher-order automated theorem provers so far have not. In order to support automated reasoning in the presence of a choice operator, we present a cut-free ground tableau calculus for Church's simple type theory with choice. The tableau calculus is designed with automated search in mind. In particular, the rules only operate on the top level structure of formulas. Additionally, we restrict the instantiation terms for quantifiers to a universe that depends on the current branch. At base types the universe of instantiations is finite. Both of these restrictions are intended to minimize the number of rules a corresponding search procedure is obligated to consider. We prove completeness of the tableau calculus relative to Henkin models. [ABSTRACT FROM AUTHOR]

There are obvious similarities between the cognitive constructs of A. 1. Beck's (1976) cognitive theory and the response style theory (S. Nolen-Hoeksema & J. Morrow, 1991). Different propositions of J. A. Ciesla and J. E. Roberts (2007) and S. Lyubomirsky and S. Nolen-Hoeksema (1993, 1995) concerning associations of 2 response styles, brooding and reflection, with constructs of Beck's cognitive theory (schemata, cognitive errors, cognitive triad, automatic thoughts) were tested. Model comparisons were based on a 4-week study in which 397 participants completed self-report instruments at 2 time points. A model allowing schemata to influence brooding and reflection that influence the other cognitive variables of Beck's cognitive theory fits the data better than the other integrated models. However, although schemata were significant predictors of both response styles, neither response style did significantly predict other cognitive variables. A comparison of the integrated model with Beck's original cognitive theory revealed that Beck's original theory fits the data better than the integrated model, whereas both models explain about the same amount of variance. Thus, an integration of Beck's theory and the response style theory are not supported. [ABSTRACT FROM AUTHOR]

We present functional dependencies, a convenient, formal, but high-level, specification format for a piece of procedural software (function). Functional dependencies specify the set of memory locations, which may be modified by the function, and for each modified location, the set of memory locations that influence its final value. Verifying that a function respects pre-defined functional dependencies can be tricky: the embedded world uses C and Ada, which have arrays and pointers. Existing systems we know of that manipulate functional dependencies, Caveat and SPARK, are restricted to pointer-free subsets of these languages. This article deals with the functional dependencies in a programming language with full aliasing. We show how to use a weakest pre-condition calculus to generate a verification condition for pre-existing functional dependencies requirements. This verification condition can then be checked using automated theorem provers or proof assistants. With our approach, it is possible to verify the specification as it was written beforehand. We assume little about the implementation of the verification condition generator itself. Our study takes place inside the C analysis framework Frama-C, where an experimental implementation of the technique described here has been implemented on top of the WP plug-in in the development version of the tool. [ABSTRACT FROM AUTHOR]

This paper presents a formal executable semantics of object-oriented models. We made it possible to conduct both simulation and theorem proving on the semantics by implementing it within the expressive intersection of the functional programming language ML and the theorem prover HOL. In this paper, we present the definition and implementation of the semantics. We also present a prototype verification tool ObjectLogic which supports simulation and theorem proving on the semantics. As a case study, we show the verification of a practical firewall system. [ABSTRACT FROM AUTHOR]

We present a formalization of the topological ring of formal power series in Isabelle/HOL. We also formalize formal derivatives, division, radicals, composition and reverses. As an application, we show how formal elementary and hyper-geometric series yield elegant proofs for some combinatorial identities. We easily derive a basic theory of polynomials. Then, using a generic formalization of the fraction field of an integral domain, we obtain formal Laurent series and rational functions for free. [ABSTRACT FROM AUTHOR]

Higman's lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. In this paper we present a formalization and proof of Higman's Lemma in the ACL2 theorem prover. Our formalization is based on a proof by Murthy and Russell, where the key termination argument is justified by the multiset relation induced by a well-founded relation. To our knowledge, this is the first mechanization of this proof. [ABSTRACT FROM AUTHOR]

We have developed a program for inductive theory formation, called IsaCoSy, which synthesises conjectures 'bottom-up' from the available constants and free variables. The synthesis process is made tractable by only generating irreducible terms, which are then filtered through counter-example checking and passed to the automatic inductive prover IsaPlanner. The main technical contribution is the presentation of a constraint mechanism for synthesis. As theorems are discovered, this generates additional constraints on the synthesis process. We evaluate IsaCoSy as a tool for automatically generating the background theories one would expect in a mature proof assistant, such as the Isabelle system. The results show that IsaCoSy produces most, and sometimes all, of the theorems in the Isabelle libraries. The number of additional un-interesting theorems are small enough to be easily pruned by hand. [ABSTRACT FROM AUTHOR]

During the 1970s and 1980s, a team of Automated Theorem Proving researchers at the Argonne National Laboratory near Chicago developed the Automated Reasoning Assistant, or AURA, to assist human users in the search for mathematical proofs. The resulting hybrid humansAURA system developed the capacity to make novel contributions to pure mathematics by very untraditional means. This essay traces how these unconventional contributions were made and made possible through negotiations between the humans and the AURA at Argonne and the transformation in mathematical intuition they produced. At play in these negotiations were experimental practices, nonhumans, and nonmathematical modes of knowing. This story invites an earnest engagement between historians of mathematics and scholars in the history of science and science studies interested in experimental practice, material culture, and the roles of nonhumans in knowledge making. [ABSTRACT FROM AUTHOR]

A central objective of the verifying compiler grand challenge is to develop a push-button verifier that generates proofs of correctness in a syntax-driven fashion similar to the way an ordinary compiler generates machine code. The software developer's role is then to provide suitable specifications and annotated code, but otherwise to have no direct involvement in the verification step. However, the general mathematical developments and results upon which software correctness is based may be established through a separate formal proof process in which proofs might be mechanically checked, but not necessarily automatically generated. While many ideas that could conceivably form the basis for software verification have been known 'in principle' for decades, and several tools to support an aspect of verification have been devised, practical fully automated verification of full software behavior remains a grand challenge. This paper explains how RESOLVE takes a step towards addressing this challenge by integrating foundational and practical elements of software engineering, programming languages, and mathematical logic into a coherent framework. Current versions of the RESOLVE verifier generate verification conditions (VCs) for the correctness of component-based software in a modular fashion-one component at a time. The VCs are currently verified using automated capabilities of the Isabelle proof assistant, the SMT solver Z3, a minimalist rewrite prover, and some specialized decision procedures. Initial experiments with the tools and further analytic considerations show both the progress that has been made and the challenges that remain. [ABSTRACT FROM AUTHOR]

This paper presents a formal theory to characterize symmetry in netlists and symmetry in properties. The inherent correlation between the two types of symmetry is formalized as a theorem, which provides the soundness of our symmetry reduction method. A practical tactic is introduced to effectively integrate the symmetry reduction approach in a hybrid verification environment which combines theorem proving and symbolic trajectory evaluation. Finally, the effecitveness of the symmetry reduction method is demonstrated by case studies. [ABSTRACT FROM AUTHOR]

Ecosystem constraints are both ontic and epistemic. They limit activity, and as problems to be solved they drive organization, which is our hypothesis: The driver of organization is constraint. Solutions proliferate further constraints in an unending spiral of problem (constraint) generation and solution. As constraints proliferate, behavior narrows, and species diversify to compensate (paradox of constraint). Resource enrichment reduces constraints, releases behavior, and reduction of challenges decreases diversity (paradox of enrichment)—high diversity is expressed in low-resource environments and low diversity in high-resource environments. A three-part model of constraints is formulated for non-living systems, and also for goal-directed, problem-solving biota. Mode 1: dynamical means behavior is co-determined by internal states and external inputs. Mode 2: cybernetic employs negative feedback to keep dynamics within goal-oriented operating limits. Mode 3: model-making entails ability to represent (model) physical reality and respond to both phenomenal (modeled) and physical inputs; this property distinguishes living from nonliving systems. Principal sections of the paper elaborate dynamical constraints (three classes), boundary constraints (expressed in edge effects and trophic dynamics), physical constraints (space, time, temperature), chemical constraints (environment fitness, ecological stoichiometry, chemical evolution, limiting factors), coding constraints (environmental vs. genetic coding), network and pathway constraints (connectivity), and natural selection constraints (fitting to the biosphere). Consideration of how the world would look without constraints suggests how fundamental these are in ecosystem emergence, and how the next property in this series, differentiation, would be unmotivated without them. We conclude that constraints as a category are under-studied in ecology, poorly understood in ecological phenomenology, and (our hypothesis) comprise a ubiquitous organizing force in nature. [Copyright &y& Elsevier]

This paper collects, with few minor formal changes, two of the latest scientific contributions () written by Prof. Enzo Tiezzi, where he introduced new concepts and tools to formalize and understand the role of thermodynamics in ecosystems theory. Particular attention is devoted to goal functions, to the relation of matter, energy, space and time and to the interdisciplinary approach connecting thermodynamics and biology. Entropy is discussed as a fundamental goal function in the far from equilibrium framework. The relationship between entropy, as a non-state function, and the state-function energy is stressed and discussed, at the light of the role of information. The theory of probability is also discussed in the light of new theoretical findings related to the role of events, also in terms of entropy and evolutionary thermodynamics. Confined Ontic Open Systems (COOS) represent the latest model proposed by Prof. Tiezzi based on his Ecodynamic theory, evolutionary thermodynamics, Ulanowicz's ontic. The model has a wide range of applications, including ecosystems, ecological economics, urban organization, the supra-molecular structure of water and global biosphere's models. The model is explained in terms of evolutionary thermodynamics and Jørgensen's ecosystems theory. [Copyright &y& Elsevier]

The physicist Walter M. Elsasser is mostly known for his work on the Earth's magnetism. Less attention has been paid to his efforts toward identifying what are the real differences between physical and biological systems. One essential distinction he recognized was that physical systems are largely homogenous while biological systems always revealed what he called ordered heterogeneity. Calculation of the possible configurations of such heterogeneous systems almost always leads to combinatorial explosions and to what Elsasser referred to as immense numbers. Such calculations have the consequence that any such systems are necessarily unique – mathematically speaking they represent one-sets. Another consequence is that immense numbers automatically introduce enormous uncertainty and indeterminacy into the system. Such systems are said to be ontically open. Applying this perspective to the genome and employing the notion of informational entropy reveals a common drive behind all development. This means that both conventional Darwinian evolution as well as the genomic mistakes that are believed to lie behind processes like aging and diseases can be interpreted against the background of one and the same process. At the same time the approach demonstrates how Darwinian evolution encompasses other notions such as Kauffman's “adjacent possible” () and Eldridge's and Gould's “evolution via punctuated equilibria” (e.g., ). [Copyright &y& Elsevier]

We provide sufficient conditions for the existence and uniqueness of normal forms of sequences of HNN extensions defined by Bokut'. Furthermore, we show that under an assumption, which holds for various applications, such normal forms always exist (but might not be unique). The conditions are amenable to be used in automatic theorem provers. We discuss also how to obtain a Grobner-Shirshov basis from the rewrite rules of Bokut' normal forms under certain assumptions. Finally, we provide an application drawn from a paper of Aanderaa and Cohen to illustrate the sufficiency conditions. [ABSTRACT FROM AUTHOR]

pplications in software verification often require determining the satisfiability of first-order formulae with respect to background theories. During development, conjectures are usually false. Therefore, it is desirable to have a theorem prover that terminates on satisfiable instances. Satisfiability Modulo Theories (SMT) solvers have proven to be highly scalable, efficient and suitable for integrated theory reasoning. Inference systems with resolution and superposition are strong at reasoning with equalities, universally quantified variables, and Horn clauses. We describe a theorem-proving method that tightly integrates superposition-based inference system and SMT solver. The combination is refutationally complete if background theory symbols only occur in ground formulae, and non-ground clauses are variable-inactive. Termination is enforced by introducing additional axioms as hypotheses. The system detects any unsoundness introduced by these speculative inferences and recovers from it. [ABSTRACT FROM AUTHOR]

We present a new calculus for first-order theorem proving with equality, $ \mathcal{ME}+$ Sup, which generalizes both the Superposition calculus and the Model Evolution calculus (with equality) by integrating their inference rules and redundancy criteria in a non-trivial way. The main motivation is to combine the advantageous features of these two rather complementary calculi in a single framework. In particular, Model Evolution, as a lifted version of the propositional DPLL procedure, contributes a non-ground splitting rule that effectively permits to split a clause into non variable disjoint subclauses. In the paper we present the calculus in detail. Our main result is its completeness under semantically justified redundancy criteria and simplification rules. We also show how under certain assumptions the model representation computed by a (finite and fair) derivation can be queried in an effective way. [ABSTRACT FROM AUTHOR]

Abstract: Verification problems can often be encoded as first-order validity or satisfiability problems. The availability of efficient automated theorem provers is a crucial pre-requisite for automating various verification tasks as well as their cooperation with specialized decision procedures for selected theories, such as Presburger Arithmetic. In this paper, we investigate how automated provers based on a form of equational reasoning, called paramodulation, can be used in verification tools. More precisely, given a theory T axiomatizing some data structure, we devise a procedure to answer the following questions. Is the satisfiability problem of T decidable by paramodulation? Can a procedure based on paramodulation for T be efficiently combined with other specialized procedures by using the Nelson–Oppen schema? Finally, if paramodulation decides the satisfiability problem of two theories, does it decide satisfiability in their union? The procedure capable of answering all questions above is based on Schematic Saturation; an inference system capable of over-approximating the inferences of paramodulation when solving satisfiability problems in a given theory T. Clause schemas derived by Schematic Saturation describe all clauses derived by paramodulation so that the answers to the questions above are obtained by checking that only finitely many different clause schemas are derived or that certain clause schemas are not derived. [Copyright &y& Elsevier]

Abstract: This paper presents a formal symbolic trajectory evaluation (STE) theory based on a structural netlist circuit model, instead of an abstract next state function. We introduce an inductive definition for netlists, which gives an accurate and formal definition for netlist structures. A closure state function of netlists is formally introduced in terms of the formal netlist model. We refine the definition of the defining trajectory and the STE implementation to deal with the closure state function. The close correspondence between netlist structures and properties is discussed. We present a set of novel algebraic laws to characterize the relation between the structures and properties of netlists. Finally, the application of the new laws is demonstrated by parameterized verification of the properties of content-addressable memories. [Copyright &y& Elsevier]

We address the problem of Finite Model Computation (FMC) of first-order theories and show that FMC can efficiently and transparently be solved by taking advantage of a recent extension of Answer Set Programming (ASP), called incremental Answer Set Programming (iASP). The idea is to use the incremental parameter in iASP programs to account for the domain size of a model. The FMC problem is then successively addressed for increasing domain sizes until an answer set, representing a finite model of the original first-order theory, is found. We implemented a system based on the iASP solver iClingo and demonstrate its competitiveness by showing that it slightly outperforms the winner of the FNT division of CADE's 2009 Automated Theorem Proving (ATP) competition on the respective benchmark collection. [ABSTRACT FROM AUTHOR]

The article presents the methods of obtaining optimal conditions for the positivity of the density of an invariant measure. It provides the mathematical notation of elliptic equation of L*μ = 0 in which the conditions of the measure μ integrates with respect to Lebesgue measure. It notes the class of function and the probability measure of coefficients that satisfy conditions of continuously differential function. It also offers the mathematical proof to clarify the validity of the condition of the theorems.

In contrast to the widespread use of computer algebra systems in mathematics automated theorem provers have largely met with indifference. There are signs that this is at last beginning to change. We argue that it is inevitable that automated provers will be adopted as a practical tool for the working mathematician. Mathematical applications of automated provers raises profound challenges for their developers. [ABSTRACT FROM AUTHOR]

Abstract: 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. [Copyright &y& Elsevier]

There are many powerful techniques for automated termination analysis of term rewriting. However, up to now they have hardly been used for real programming languages.We present a new approach which permits the application of existing techniques from term rewriting to prove termination of most functions defined in Haskell programs. In particular, we show how termination techniques for ordinary rewriting can be used to handle those features of Haskell which are missing in term rewriting (e.g., lazy evaluation, polymorphic types, and higher-order functions).We implemented our results in the termination prover AProVE and successfully evaluated them on existing Haskell libraries. [ABSTRACT FROM AUTHOR]

Abstract: We propose a novel method to construct user-space internet protocol stacks whose security properties can be formally explored and verified. The proposed method allows construction of protocol stacks using a C++ subset. We define a formal state-transformer representation of protocol stacks in which the protocol stack is specified in terms of three primary operations, which are constructed from sub-operations, in a compositional manner. We also define a Kripke model that captures the sequencing and attributes of stack operations. We propose a novel approach, called split verification, which combines theorem-proving and model-checking to establish properties for a protocol stack specification. In split verification, properties to be established for the stack are expressed as a combination of properties for primitive operations to be established via theorem-proving as well as temporal properties on operation sequencing, called promotion conditions, to be established via model-checking on the stack operations model. We use abstract Z specifications to represent operation properties and computational tree logic (CTL) formulae to represent promotion conditions. Operation properties are established by checking whether the operation(s) under consideration are correct refinements of the abstract Z specification(s). Our conclusion is that split verification: (a) avoids scalability issues caused by state-space explosion in model-checking and long unwieldy proofs in theorem-proving, and, (b) lowers cost of proof maintenance for localized changes in the stack. [Copyright &y& Elsevier]

The CADE ATP System Competition (CASC) is an annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems. CASC-J5 was the fifteenth competition in the CASC series. Thirty-nine ATP systems and system variants competed in the various competition and demonstration divisions. An outline of the competition design, and a commentated summary of the results, are presented. [ABSTRACT FROM AUTHOR]

Abstract: New axioms for domain operations on semirings and Kleene algebras are proposed. They generalise the relational notion of domain–the set of all states that are related to some other state–to a wide range of models. They are internal since the algebras of state spaces are induced by the domain axioms. They are simpler and conceptually more appealing than previous two-sorted external approaches in which the domain algebra is determined through typing. They lead to a simple and natural algebraic approach to modal logics based on equational reasoning. The axiomatisations have been developed in a new style of computer-enhanced mathematics by automated theorem proving, and the approach itself is suitable for automated systems analysis and verification. This is demonstrated by a fully automated proof of a modal correspondence result for Löb’s formula that has applications in termination analysis. [ABSTRACT FROM AUTHOR]

Abstract: This paper presents a novel approach to automated geometric reasoning for 3D building models. Geometric constraints like orthogonality or parallelity play a prominent role in man-made objects such as buildings. Thus, constraint based modelling, that specifies buildings by their individual components and the constraints between them, is a common approach in 3D city models. Since prototyped building models allow one to incorporate a priori knowledge they support the 3D reconstruction of buildings from point clouds and allow the construction of virtual cities. However, high level building models have a high degree of complexity and consequently are not easily manageable. Interactive tools are needed which facilitate the development of consistent models that, for instance, do not entail internal logical contradictions. Furthermore, there is often an interest in a compact, redundancy-free representation. We propose an approach that uses algebraic methods to prove that a constraint is deducible from a set of premises. While automated reasoning in 2D models is practical, a substantial increase in complexity can be observed in the transition to the three-dimensional space. Apart from that, algebraic theorem provers are restricted to crisp constraints so far. Thus, they are unable to handle quality issues, which are, however, an important aspect of GIS data and models. In this article we present an approach to automatic 3D reasoning which explicitly addresses uncertainty. Hereby, our aim is to support the interactive modelling of 3D city models and the automatic reconstruction of buildings. Geometric constraints are represented by multivariate polynomials whereas algebraic reasoning is based on Wu’s method of pseudodivision and characteristic sets. The reasoning process is further supported by logical inference rules. In order to cope with uncertainty and to address quality issues the reasoner integrates uncertain projective geometry and statistical hypothesis tests. Consequently, it allows one to derive uncertain conclusions from uncertain premises. The quality of such conclusions is quantified in a way which is sound both from a logical and a statistical perspective. [Copyright &y& Elsevier]

Abstract: The classic readers–writers problem has been extensively studied. This holds to a lesser degree for the reentrant version, where it is allowed to nest locking actions. Such nesting is useful when a library is created with various procedures each starting and ending with a lock operation. Allowing nesting makes it possible for these procedures to call each other. We considered an existing widely used industrial implementation of the reentrant readers–writers problem. Staying close to the original code, we modelled and analyzed it using a model checker resulting in the detection of a serious error: a possible deadlock situation. The model was improved and checked satisfactorily for a fixed number of processes. To achieve a correctness result for an arbitrary number of processes the model was converted to a specification that was proven with a theorem prover. Furthermore, we studied starvation. Using model checking we found a starvation problem. We have fixed the problem and checked the solution. Combining model checking with theorem proving appeared to be very effective in reducing the time of the verification process. [Copyright &y& Elsevier]

Strong typicality, which is more powerful for theorem proving than weak typicality, can be applied to finite alphabets only, while weak typicality can be applied to countable alphabets. In this paper, the relation between typicality and information divergence measures is discussed. The new definition of information divergence measure in this paper leads to the definition of a unified typicality for finite or countably infinite alphabets which is stronger than both weak typicality and strong typicality. Unified typicality retains the asymptotic equipartition property and the structural properties of strong typicality, and it can potentially be used to generalize those theorems which are previously established by strong typicality to countable alphabets. The applications in rate-distortion theory and multisource network coding problems are discussed. [ABSTRACT FROM PUBLISHER]

This article introduces a new model-based method for incrementally constructing critical systems and illustrates its application to the development of fault-tolerant systems. The method relies on a special form of composition to combine software components and a set of proof rules to obtain high confidence of the correctness of the composed system. As in conventional component-based software development, two (or more) components are combined, but in contrast to many component-based approaches used in practice, which combine components consisting of code, our method combines components represented as state machine models. In the first phase of the method, a model is developed of the normal system behavior, and system properties are shown to hold in the model. In the second phase, a model of the required fault-handling behavior is developed and 'or-composed' with the original system model to create a fault-tolerant extension which is, by construction, 'fully faithful' (every execution possible in the normal system is possible in the fault-tolerant system). To model the fault-handling behavior, the set of states of the normal system model is extended through new state variables and new ranges for some existing state variables, and new fault-handling transitions are defined. Once constructed, the fault-tolerant extension is shown, using a set of property inheritance and compositional proof rules, to satisfy both the overall system properties, typically weakened, and selected fault-tolerance properties. These rules can often be used to verify the properties automatically. To provide a formal foundation for the method, formal notions of or-composition, partial refinement, fault-tolerant extension, and full faithfulness are introduced. To demonstrate and validate the method, we describe its application to a real-world, fault-tolerant avionics system. [ABSTRACT FROM AUTHOR]

In interactive theorem proving practice a significant amount of time is spent on unsuccessful proof attempts of wrong conjectures. An automatic method that reveals them by generating finite counter examples would offer an extremely valuable support for a proof engineer by saving his time and effort. In practice, such counter examples tend to be small, so usually there is no need to search for big instances. Most definitions of functions or predicates on infinite structures do not preserve the semantics if a transition to arbitrary finite substructures is made. We propose constraints which guarantee a correct axiomatization on finite structures and present an approach which uses the Alloy Analyzer to generate finite instances of theories in the theorem prover KIV. It is evaluated on the library of basic data types as well as on some challenging case studies in KIV. The technique is implemented using the Kodkod constraint solver which is a successor of Alloy. [ABSTRACT FROM AUTHOR]