Search

A recent trend in object-oriented programming languages is the use of access permissions (APs) as an abstraction for controlling concurrent executions of programs. The use of AP source code annotations defines a protocol specifying how object references can access the mutable state of objects. Although the use of APs simplifies the task of writing concurrent code, an unsystematic use of them can lead to subtle problems. This paper presents a declarative interpretation of APs as linear concurrent constraint programs (lcc). We represent APs as constraints (i.e., formulas in logic) in an underlying constraint system whose entailment relation models the transformation rules of APs. Moreover, we use processes in lcc to model the dependencies imposed by APs, thus allowing the faithful representation of their flow in the program. We verify relevant properties about AP programs by taking advantage of the interpretation of lcc processes as formulas in Girard's intuitionistic linear logic (ILL). Properties include deadlock detection, program correctness (whether programs adhere to their AP specifications or not), and the ability of methods to run concurrently. By relying on a focusing discipline for ILL, we provide a complexity measure for proofs of the above-mentioned properties. The effectiveness of our verification techniques is demonstrated by implementing the Alcove tool that includes an animator and a verifier. The former executes the lcc model, observing the flow of APs, and quickly finding inconsistencies of the APs vis-à-vis the implementation. The latter is an automatic theorem prover based on ILL. [ABSTRACT FROM AUTHOR]

This paper is a tutorial on how to model hybrid systems as hybrid programs in differential dynamic logic and how to prove complex properties about these complex hybrid systems in KeYmaera, an automatic and interactive formal verification tool for hybrid systems. Hybrid systems can model highly nontrivial controllers of physical plants, whose behaviors are often safety critical such as trains, cars, airplanes, or medical devices. Formal methods can help design systems that work correctly. This paper illustrates how KeYmaera can be used to systematically model, validate, and verify hybrid systems. We develop tutorial examples that illustrate challenges arising in many real-world systems. In the context of this tutorial, we identify the impact that modeling decisions have on the suitability of the model for verification purposes. We show how the interactive features of KeYmaera can help users understand their system designs better and prove complex properties for which the automatic prover of KeYmaera still takes an impractical amount of time. We hope this paper is a helpful resource for designers of embedded and cyber-physical systems and that it illustrates how to master common practical challenges in hybrid systems verification. [ABSTRACT FROM AUTHOR]

ABSTRACT This article describes the experience and results obtained from teaching computational logic in an introductory course for undergraduates. The proposed teaching approach helps students to reach a deeper level of understanding in first order logic representation, computational logic procedures and automated theorem proving. The article includes the description of SLI, a theorem prover with a graphical output and the results of a survey to assess the acceptance of the tool. © 2015 Wiley Periodicals, Inc. Comput Appl Eng Educ 23:837-845, 2015; View this article online at ; DOI [ABSTRACT FROM AUTHOR]

GeoGebra is an open-source educational mathematics software tool, with millions of users worldwide. It has a number of features (integration of computer algebra, dynamic geometry, spreadsheet, etc.), primarily focused on facilitating student experiments, and not on formal reasoning. Since including automated deduction tools in GeoGebra could bring a whole new range of teaching and learning scenarios, and since automated theorem proving and discovery in geometry has reached a rather mature stage, we embarked on a project of incorporating and testing a number of different automated provers for geometry in GeoGebra. In this paper, we present the current achievements and status of this project, and discuss various relevant challenges that this project raises in the educational, mathematical and software contexts. We will describe, first, the recent and forthcoming changes demanded by our project, regarding the implementation and the user interface of GeoGebra. Then we present our vision of the educational scenarios that could be supported by automated reasoning features, and how teachers and students could benefit from the present work. In fact, current performance of GeoGebra, extended with automated deduction tools, is already very promising-many complex theorems can be proved in less than 1 second. Thus, we believe that many new and exciting ways of using GeoGebra in the classroom are on their way. [ABSTRACT FROM AUTHOR]

Automated theorem proving is the use of computers to prove or disprove mathematical or logical statements. Such statements can express properties of hardware or software systems, or facts about the world that are relevant for applications such as natural language processing and planning. A brief introduction to propositional and first-order logic is given, along with some of the main methods of automated theorem proving in these logics. These methods of theorem proving include resolution, Davis and Putnam-style approaches, and others. Methods for handling the equality axioms are also presented. Methods of theorem proving in propositional logic are presented first, and then methods for first-order logic. WIREs Cogn Sci 2014, 5:115-128. doi: 10.1002/wcs.1269 Conflict of interest: The authors has declared no conflicts of interest for this article. For further resources related to this article, please visit the . [ABSTRACT FROM AUTHOR]

Abstract: Sledgehammer is a tool that harnesses external first-order automatic theorem provers (ATPs) to discharge interactive proof obligations arising in Isabelle/HOL. We extended it with LEO-II and Satallax, the two most prominent higher-order ATPs, improving its performance on higher-order problems. To explore their usefulness, these ATPs are measured against first-order ATPs and built-in Isabelle tactics on a variety of benchmarks from Isabelle and the TPTP library. Sledgehammer provides an ideal test bench for individual features of LEO-II and Satallax, revealing areas for improvements. [Copyright &y& Elsevier]

This paper presents an original dynamic subsumption technique for Boolean CNF formulae. It exploits simple and sufficient conditions to detect, during conflict analysis, clauses from the formula that can be reduced by subsumption. During the learnt clause derivation, and at each step of the associated resolution process, checks for backward subsumption between the current resolvent and clauses from the original formula are efficiently performed. The resulting method allows the dynamic removal of literals from the original clauses. Experimental results show that the integration of our dynamic subsumption technique within the state-of-the-art SAT solvers Minisat and Rsat particularly benefits to crafted problems. [ABSTRACT FROM AUTHOR]

Improving software reliability of mission-critical systems is widely recognised as one of the major challenges. Early detection of errors in software requirements, designs and implementation, need rigorous verification and validation techniques. Several techniques comprising static and dynamic testing approaches are used to improve reliability of mission critical software; however it is hard to balance development time and budget with software reliability. Particularly using dynamic testing techniques, it is hard to ensure software reliability, as exhaustive testing is not possible. On the other hand, formal verification techniques utilise mathematical logic to prove correctness of the software based on given specifications, which in turn improves the reliability of the software. Theorem proving is a powerful formal verification technique that enhances the software reliability for mission-critical aerospace applications. This paper discusses the issues related to software reliability and theorem proving used to enhance software reliability through formal verification technique, based on the experiences with STeP tool, using the conventional and internationally accepted methodologies, models, theorem proving techniques available in the tool without proposing a new model. [ABSTRACT FROM AUTHOR]

The paper describes the new kernel for the Calculus of Inductive Constructions (CIC) implemented inside the Matita Interactive Theorem Prover. The design of the newkernel has been completely revisited since the first release, resulting in a remarkably compact implementation of about 2300 lines of OCaml code. The work is meant for people interested in implementation aspects of Interactive Provers, and is not self contained. In particular, it requires good acquaintance with Type Theory and functional programming languages. [ABSTRACT FROM AUTHOR]

In the paper is described Baselog system for the deductive databases as an extension of ATP (Automatic Theorem Proving) resolution system. Flexible binding of the Opened-world concept in ATP system and Closed-world reasoning in Datalog and Prolog has been realized by means of introducing the Cwa--rule and implementing Cwa--controller into ATP system. The system management has been realized on the predicate level depending on the semantic completeness of the database contents. Prolog and Datalog defects related to semantically incomplete bases connected with the negation problem and the Cwa--principle have been eliminated. The predicates, whose base is semantically complete are being treated as in Datalog or Prolog systems, while the predicate, whose base is incomplete, is being treated as in ATP system. The examples, illustrating Baselog system advantages, especially about, are quoted: mathematical induction in deductive systems of logic programming, using remote databases and simbolical execution of Pascal programs. [ABSTRACT FROM AUTHOR]

The CADE ATP system competition (CASC) is an annual evaluation of fully automatic, first order Automated Theorem Proving (ATP) systems. CASC-21 was the twelfth competition in the CASC series. Twenty 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]

The efficiency of systems for constraint programming (CP) is currently highly affected by the actual formulation of the input problem. To this end, several choices have to be made by modelers in order to write efficient specifications and handle instances of realistic size, and this, of course, represents a major obstacle to reach full declarativeness. Several structural properties of problem specifications have been investigated in order to provide techniques that reformulate a constraint program into one which is more efficiently evaluable by the solver at hand. In this paper we consider two such properties, symmetries and functional dependencies among variables, and show that, by characterizing problem specifications as logical formulae, the task of deciding whether such properties hold, and consequently that of performing the relevant reformulations, can be practically mechanized by means of automated theorem proving (ATP) technology. In particular, we report the results on using ATP technology for checking the existence of symmetries, checking whether a given constraint is symmetry-breaking, and checking the existence of functional dependencies in a specification. The output of the reasoning phase is a transformed constraint program, consisting in a reformulated specification and, possibly, a search strategy. We show our techniques on problems such as graph coloring, Sailco inventory, and protein folding. [ABSTRACT FROM AUTHOR]

The article discusses the hybrid computer system verification process that combines theorem proving with model checking through predicate abstraction. The author contends that there is a gap in the complexity verification tools can handle and practical verification problems that can be lessened via theorem proving with model checking through predicate abstraction.

The article offers an overview of hybrid techniques for functional verification of computer hardware. The article discusses the taxonomy of hybrid methods, ATPG and formal techniques, methods combining formal techniques, trajectory evaluation and theorem proving, combining theorem provers and decision procedures, and composition of model-checking runs.

Automated Theorem Proving (ATP) systems are complex pieces of software, and thus may have bugs that make them unsound. In order to guard against unsoundness, the derivations output by an ATP system may be semantically verified by trusted ATP systems that check the required semantic properties of each inference step. Such verification needs to be augmented by structural verification that checks that inferences have been used correctly in the context of the overall derivation. This paper describes techniques for semantic verification of derivations, and reports on their implementation and testing in the GDV verifier. [ABSTRACT FROM AUTHOR]

This paper shows how classic inductive assertions can be used in conjunction with a formal operational semantics to prove partial correctness properties of programs. The method imposes only the proof obligations that would be produced by a verification condition generator – but does not require the definition of a verification condition generator. All that is required is a theorem prover, a formal operational semantics, and the object program with appropriate assertions at user-selected cut points. The verification conditions are generated in the course of the theorem-proving process by straightforward symbolic evaluation of the formal operational semantics. The technique is demonstrated by proving the partial correctness of simple bytecode programs with respect to a preexisting operational model of the Java Virtual Machine. [ABSTRACT FROM AUTHOR]

We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then processed by an automated first-order theorem prover (ATP). We discuss the unique requirements this application places on the ATPs, focusing on automation, proof checking, traceability, and usability, and describe the resulting system architecture, including a certification browser that maintains and displays links between obligations and source code locations. For full automation, the obligations must be aggressively preprocessed and simplified, and we demonstrate how the individual simplification stages, which are implemented by rewriting, influence the ability of the ATPs to solve the proof tasks. Our results are based on 13 comprehensive certification experiments that lead to 366 top-level safety obligations and ultimately to more than 25,000 proof tasks which have been used to determine the suitability of the high-performance provers DCTP, E-Setheo, E, Gandalf, Otter, Setheo, Spass, and Vampire, and our associated infrastructure. The proofs found by Otter have been checked by Ivy. [ABSTRACT FROM AUTHOR]

Deductive program synthesis systems based on automated theorem proving offer the promise of software that is correct by construction. However, the difficulty encountered in constructing usable deductive synthesis systems has prevented their widespread use. Amphion is a real-world, domain-independent, completely automated program synthesis system. It is specialized to specific applications through the creation of an operational domain theory and a specialized deductive engine. This paper describes an experiment aimed at making the construction of usable Amphion applications easier. The software system Theory Operationalization for Program Synthesis (TOPS) has a library of decision procedure templates with a theory schema for each procedure. TOPS identifies sets of axioms in the domain theory that are instances of theory schema associated with library procedures. For each procedure instance, TOPS uses iterated partial deduction to augment the procedure with the capability to construct ground terms for deductive synthesis. Synthesized procedures are interfaced to a resolution theorem prover. Axioms in the original domain theory that are implied by the synthesized procedures are removed. The inference rules of the theorem prover have been extended so that during deductive synthesis, each procedure is invoked to test conjunctions of literals in the language of the theory of that procedure. When possible, the procedure generates ground terms and binds them to variables in a problem specification. These terms are program fragments. Experiments show that the procedures synthesized by TOPS can reduce theorem proving search at least as much as hand tuning of the deductive synthesis system. [ABSTRACT FROM AUTHOR]

Proof systems for expressive type theories provide a foundation for the verification and synthesis of programs. But despite their successful application to numerous programming problems there remains an issue with scalability. Are proof environments capable of reasoning about large software systems? Can the support they offer be useful in practice? In this article we answer this question by showing how the NUPRL proof development system and its rich type theory have contributed to the design of reliable, high-performance networks by synthesizing optimized code for application configurations of the ENSEMBLE group communication toolkit. We present a type-theoretical semantics of OCAML, the implementation language of ENSEMBLE, and tools for automatically importing system code into the NUPRL system. We describe reasoning strategies for generating verifiably correct fast-path optimizations of application configurations that substantially reduce end-to-end latency in ENSEMBLE. We also discuss briefly how to use NUPRL for checking configurations against specifications and for the design of reliable adaptive network protocols. [ABSTRACT FROM AUTHOR]

In this article we describe VAMPIRE: a high-performance theorem prover for first-order logic. As our description is mostly targeted to the developers of such systems and specialists in automated reasoning, it focuses on the design of the system and some key implementation features. We also analyze the performance of the prover at CASC-JC. [ABSTRACT FROM AUTHOR]

The first-order theorem prover SCOTT has been through a series of versions over some ten years. The successive provers, while retaining the same underlying technology, have used radically different algorithms and shown wide differences of behaviour. The development process has depended heavily on experiments with problems from the TPTP library and has been sharpened by participation in CASC each year since 1997. In the present paper, we outline some of the difficulties inherent in designing and refining a theorem prover as complex as SCOTT, and explain our experimental methodology. While SCOTT is not one of the systems which have been highly optimised for CASC, it does help to illustrate the influence of both CASC and the TPTP library on contemporary theorem proving research. [ABSTRACT FROM AUTHOR]

The importance of effective requirements analysis techniques cannot be overemphasized when developing software requiring high levels of assurance. Requirements analysis can be largely classified as either structural or functional. The former investigates whether definitions and uses of variables and functions are consistent, while the latter addresses whether requirements accurately reflect users' needs. Verification of structural properties for large and complex software requirements is often repetitive, especially if requirements are subject to frequent changes. While inspection has been successfully applied to many industrial applications, the authors found inspection to be ineffective when reviewing requirements to find errors violating structural properties. Moreover, current tools used in requirements engineering provide only limited support in automatically enforcing structural correctness of the requirements. Such experience has motivated research to automate straightforward but tedious activities. This paper demonstrates that a theorem prover, PVS (Prototype Verification System), is useful in automatically verifying structural correctness of software requirements specifications written in SCR (Software Cost Reduction)-style. Requirements are automatically translated into a semantically equivalent PVS specification. Users need not be experts in formal methods or power users of PVS. Structural properties to be proved are expressed in PVS theorems, and the PVS proof commands are used to carry out the proof automatically. Since these properties are application independent, the same verification procedure can be applied to requirements of various software systems. Copyright © 2001 John Wiley & Sons, Ltd. [ABSTRACT FROM AUTHOR]

This paper describes the data type definition facilities of the AFFIRM system for program specification and verification. Following an overview of the system, we review the rewrite rule concepts that form the theoretical basis for its data type facilities. The main emphasis is on methods of ensuring convergence (finite and unique termination) of sets of rewrite rules and on the relation of this property to the equational and inductive proof theories of data types. [ABSTRACT FROM AUTHOR]

Focuses on Computer-Assisted Data Evaluation (CADE) Automated theorem proving System Competition (CASC) held each year at the International Conference on Automated Deduction. Aim of CASC; Topics included in the discussion; Introduction of several articles regarding computer programs.