Due to the difficulty of obtaining formal proofs, there is increasing interest in partially or completely automating proof search in interactive theorem provers. Despite being a theorem prover with an active community and plentiful corpus of 170,000+ theorems, no deep learning system currently exists to help automate theorem proving in ACL2. We have developed a machine learning system that generates recommendations to automatically complete proofs. We show that our system benefits from the copy mechanism introduced in the context of program repair. We make our system directly accessible from within ACL2 and use this interface to evaluate our system in a realistic theorem proving environment.

No description available.

The invention of Hardware Description Languages has given hardware designers access to powerful methods of abstraction and organization, previously only available to software developers. A high-powered means of examining properties such as reliability, correctness and safety is the creation of formal, mathematical proofs of correctness. One approach to this is the modelling of the artifact in the logic of some deductive system, such as the higher order logic of the Prototype Verification System (PVS). The ambition of this work is to demonstrate a mechanism by which a class of hardware descriptions may be used to generate such models automatically. We further demonstrate the utility of said models, using them to demonstrate non-trivial correctness properties. We also present a method of generating hardware descriptions, logical models, and proofs from a class of tabular specifications. The language on which this method operates is Bluespec SystemVerilog (BSV), a high-level hardware description language notable for its elegant semantics. The target platform of our translation is the Prototype Verification System (PVS), which features a highly automatic theorem-proving system. The translation algorithm is discussed at length, including the reconciliation of BSV's action-oriented semantic and the Kripke semantics employed by our chosen model in PVS. Five case studies demonstrate our methodology. In studies one and two, function blocks of the IEC 61131-3 Annex F library are verified against tabular specifications, or generated from the same. The remaining case studies are based on the Shakti RISC-V implementation of the RapidIO subsystem. Our final case study demonstrates progress towards the verification of highly abstract and complex properties over the entire translatable subset of the RapidIO library. / Thesis / Doctor of Philosophy (PhD) / The invention of Hardware Description Languages has given hardware designers access to powerful methods of abstraction and organization, previously only available to software developers. A high-powered means of examining properties such as reliability, correctness and safety is the creation of formal, mathematical proofs of correctness. One approach to this is the modelling of the artifact in the logic of some deductive system, such as the higher order logic of the Prototype Verification System (PVS). The ambition of this work is to demonstrate a mechanism by which a class of hardware descriptions may be used to generate such models automatically. We further demonstrate the utility of said models, using them to demonstrate non-trivial correctness properties. We also present a method of generating hardware descriptions, logical models, and proofs from a class of tabular specifications. The language on which this method operates is Bluespec SystemVerilog (BSV), a high-level hardware description language notable for its elegant semantics. The target platform of our translation is the Prototype Verification System (PVS), which features a highly automatic theorem-proving system. The translation algorithm is discussed at length, including the reconciliation of BSV's action-oriented semantic and the Kripke semantics employed by our chosen model in PVS. Five case studies demonstrate our methodology. In studies one and two, function blocks of the IEC 61131-3 Annex F library are verified against tabular specifications, or generated from the same. The remaining case studies are based on the Shakti RISC-V implementation of the RapidIO subsystem. Our final case study demonstrates progress towards the verification of highly abstract and complex properties over the entire translatable subset of the RapidIO library.

There is a great number of programming languages and they follow various paradigms such as imperative, functional, or logic programming among the major ones and various methodologies such as structured approach or object-oriented or object-centered approach. A memory management design of a programming language is one of the most important features to help facilitate reliable design. There are two wide-spread approaches in memory management: manual memory management and automatic memory management, known as Garbage Collection (GC for short). Recently, a third approach to memory management called Ownership has emerged. Ownership management is adapted in two recent languages Rust and Swift. Rust follows a deterministic syntax-driven memory management depending on static ownership rules implemented and enforced by the rustc compiler. Though the Rust approach eliminates to a high degree memory problems such as memory leak, dangling pointer and use after free, it has a steep learning costs. Swift also implements ownership concept in Automatic Reference Counting ARC. Though the ownership concept is adapted in Swift, it is not a memory safe language because of possibility of strong reference cycles. In this research, a demonstration of the ownership in Rust and Swift will be discussed and illustrated, followed by analysis of the consequences of memory issues related to each design. The comparison of Rust and Swift is based on ownership, memory safety, usability and programming paradigm in each language. As an illustration, an experiment to compare the elapsed times of two different structures and their algorithms, Binary Tree and Array are presented. The results illustrate and compare the performances of the same programs written in Rust, Swift, C, C++, and Java. / Thesis / Master of Science (MSc)

<p> </p> <p>Distributed agreement-based systems use common distributed agreement protocols such as leader election and consensus as building blocks for their target functionality—processes in these systems may need to agree on a leader, on the members of a group, on owners of locks, or on updates to replicated data. Such distributed agreement-based systems are common and potentially permit modular, scalable verification approaches that mimic their modular design. Interestingly, while there are many verification efforts that target agreement protocols themselves, little attention has been given to distributed agreement-based systems that build on top of these protocols. </p> <p>In this work, we aim to develop a fully-automated, modular, and usable parameterized verification approach for distributed agreement-based systems. To do so, we need to overcome the following challenges. First, the fully automated parameterized verification problem, i.e, the problem of algorithmically checking if the system is correct for any number of processes, is a well-known <em>undecidable </em>problem. Second, to enable modular verification that leverages the inherently-modular nature of these agreement-based systems, we need to be able to support <em>abstractions </em>of agreement protocols. Such abstractions can replace the agreement protocols’ implementations when verifying the overall system; enabling modular reasoning. Finally, even when the verification is fully automated, a system designer still needs assistance in <em>modeling </em>their distributed agreement-based systems. </p> <p>We systematically tackle these challenges through the following contributions. </p> <p>First, we support efficient, decidable verification of distributed agreement-based systems by developing a computational model—the GSP model—for reasoning about distributed (agreement-based) systems that admits decidability and <em>cutoff </em>results. Cutoff results enable practical verification by reducing the parameterized verification problem to the verification problem of a system with a fixed, finite number of processes. The GSP model supports generalized communication primitives and global guards, both of which are essential to enable abstractions of agreement protocols. </p> <p>Then, we address the usability and modularity aspects by developing a framework, QuickSilver, tailored for modeling and modular parameterized verification of distributed agreement-based systems. QuickSilver provides an intuitive domain-specific language, called Mercury, that is equipped with two agreement primitives capable of abstracting away agreement protocols when modeling agreement-based systems; enabling modular verification. QuickSilver extends the decidability and cutoff results of the GSP model to provide fully automated, efficient parameterized verification for a large class of systems modeled in Mercury. </p> <p>Finally, we leverage synthesis techniques to further enhance the usability of our approach and propose Cinnabar, a tool that supports synthesis of distributed agreement-based systems with efficiently-decidable parameterized verification. Cinnabar allows a system de- signer to provide a sketch of their Mercury model and uses a counterexample-guided synthesis procedure to search for model completions that both belong to the efficiently-decidable fragment of Mercury and are correct. </p> <p>We evaluate our contributions on various interesting distributed agreement-based systems adapted from real-world applications, such as a data store, a lock service, a surveillance system, a pathfinding algorithm for mobile robots, and more. </p>

The rise of parallel programming languages, as a result of processors' flattening clock frequencies, has lead to further use of high-level parallel pattern-based programming framework such as SkePU. SkePU provides a sequential high-level interface connected to different back-ends, or a hybrid of several, which reduces the time required to learn several new programming languages. Although this high-level interface introduces a new problem, an abstraction layer from the user to what code is being executed. To make SkePU programs easier to analyze this thesis implements a performance visualization tool for SkePU. The conducted literature study found that there currently exists very few performance visualization tools that cater specifically towards skeleton programming languages. This thesis evaluates usability of the implemented tool by conducting a survey and a user study with participants whom are very familiar with SkePU. The choice of evaluation method is in itself critically evaluated, as is the design choices made, and results are presented with an accompanying discussion as to how those results were derived.

The problem of this study was to develop and fieldtest a microcomputer assisted instruction program to teach simple microcomputer language acquisition. Four instruments were designed and pilot tested for use in the research. The first instrument was a survey designed to determine the complexity of the Applesoft BASIC commands. The second instrument was a survey to determine the frequency with which the Applesoft BASIC commands are used by Intermediate Microcomputer Users. The third instrument was an Exit Interview to determine how the Beginning Microcomputer Users felt about the instructional program and the presentation of the instruction. The fourth instrument, a Criterion Performance Test, was used to determine how well the instruction in the MAI program was transmitted to Beginning Microcomputer Users. The subjects involved in this study included three Expert Microcomputer Users, thirty Intermediate Microcomputer Users, and 24 Beginning Microcomputer Users. The experts were used to identify the Applesoft BASIC commands which are essential to Beginning Users, and to prioritize the commands. The intermediates were used to identify the frequency of use of each of the BASIC commands. Five of the intermediates were also used to test the instructional program for sequencing and appropriateness of instruction. The beginners were used for two separate purposes. Three sets of three subjects each were used to point out weaknesses in the instructional program so that they could be overcome. Fifteen beginners were used to test the final instructional program to determine whether it transmitted the desired information. Four research questions were posed in this study. These questions were answered based upon the findings. Fifteen BASIC commands and special characters were identified as essential to beginners in order for them to use the microcomputer adequately. Nine programmed instruction techniques were identified as suitable for use in microcomputer assisted instruction. One hundred and eighty-eight of the 257 revision suggestions were incorporated into program changes. Upon completion of the formative evaluation process, the instructional program was improved so that all subjects in the field test were able to demonstrate mastery of at least 70 percent of the behaviors which the program taught. / Ed. D.

The overall objective of this research is the development of a set of guidelines, or constructs, which will assist in the formulation of a simulation language for bulk material transportation systems. The formulation of these guidelines necessitated a thorough analysis of two particular areas; these being the simulation analysis procedure and bulk material transportation systems. For comprehension of the nature of simulation languages, Part II presents each step of the analysis procedure as examined from the language's perspective. Supporting this analysis, Part III presents a detailed review of selected simulation languages which are currently available to the systems analyst. Bulk material transportation systems are presented in Part IV. These systems are discussed in detail from the viewpoint of the mode of transportation, the transportation medium, and the type of bulk materials transported. The functional specifications, or constructs, for a bulk material transportation simulation language are presented in Part V. These specifications are categorized according to the following areas; the system being described, the language form, and computer considerations. Utilizing these constructs a simulation language may be developed for subsequent use by bulk material transportation systems analysts which shall be a more appropriate choice for simulating their systems than any language currently available to them. / M.S.

Expert systems are very useful and probably the most fruitful products of applied artificial intelligence. Expert systems, however, are very· expensive to develop. Powerful construction tools are indispensable to construct, modify and maintain a practical expert system. GUESS/l is a domain-independent expert systems shell that captures and enhances the strengths of its predecessors while at the same time overcoming.their limitations. GUESS/l gives a strong emphasis on human engineering, language generality, diversity of data representation and control structures, programming and run-time environment, database construction facilities and security, and many other aspects that are related to the ease of development and maintenance of expert systems. / Master of Science

This thesis describes the design and implementation of a system to extract meaning from natural language specifications of digital systems. This research is part of the ASPIN project which has the long-term goal of providing an automated system for digital system synthesis from informal specifications. This work makes several contributions, one being the application of artificial intelligence techniques to specifications writing. Also, the work deals with the subset of the English language used to describe digital systems, and the concepts within this domain have been classified into a type hierarchy. Finally, a set of relations has been defined to represent the interrelationships between the concepts of the sublanguage. This work centers around the modeling of information found in natural language specifications of digital systems. The target know ledge representation for the work is the conceptual graph, developed by John Sowa. Conceptual graphs provide a sound theoretical base as well as enough versatility to model the information found in digital system specifications. The transformation from natural language to conceptual graphs is done in two stages. In the first stage, a previously developed context-free English language parser is used to create trees of sentence structure. In the second stage, the trees are processed by a semantic analyzer which uses a conceptual type hierarchy and a database of rules to extract the meaning from the English sentence and create the conceptual graph. The main work of this thesis centers around the semantic analyzer which is written in Quintus Prolog. The semantic analyzer currently contains approximately 380 canonical conceptual graphs that cover usage of over 680 words consisting of over 240 nouns and over 460 verbs. / Master of Science