Explore the vast range of titles available.

The ACL2 theorem prover has seen sustained industrial use since the mid-1990s. Companies that have used ACL2 regularly include AMD, Centaur Technology, IBM, Intel, Kestrel Institute, Motorola/Freescale, Oracle and Rockwell Collins. This paper introduces ACL2 and focuses on how and why ACL2 is used in industry. ACL2 is well-suited to its industrial application to numerous software and hardware systems, because it is an integrated programming/proof environment supporting a subset of the ANSI standard Common Lisp programming language. As a programming language ACL2 permits the coding of efficient and robust programs; as a prover ACL2 can be fully automatic but provides many features permitting domain-specific human-supplied guidance at various levels of abstraction. ACL2 specifications and models often serve as efficient execution engines for the modelled artefacts while permitting formal analysis and proof of properties. Crucially, ACL2 also provides support for the development and verification of other formal analysis tools. However, ACL2 did not find its way into industrial use merely because of its technical features. The core ACL2 user/development community has a shared vision of making mechanized verification routine when appropriate and has been committed to this vision for the quarter century since the Computational Logic, Inc., Verified Stack. The community has focused on demonstrating the viability of the tool by taking on industrial projects (often at the expense of not being able to publish much). This article is part of the themed issue ‘Verified trustworthy software systems’.

For more than 25 years Ford Motor Company has been utilizing an AI‐based system to manage process planning for vehicle assembly at its assembly plants around the world. The scope of the AI system, known originally as the Direct Labor Management System and now as the Global Study Process Allocation System (GSPAS), has increased over the years to include additional functionality on ergonomics and powertrain assembly (engines and transmission plants). The knowledge about Ford's manufacturing processes is contained in an ontology originally developed using the KL‐ONE representation language and methodology. To preserve the viability of the GSPAS ontology and to make it easily usable for other applications within Ford, we needed to reengineer and convert the KL‐ONE ontology into a semantic web OWL/RDF format. In this article, we will discuss the process by which we reengineered the existing GSPAS KL‐ONE ontology and deployed semantic web technology in our application.

In view of the fact that web applications are significantly large, complex, highly dynamic & critical software systems, it is desirable that processes of web design and development be systematic & be automated as far as possible. The task of automating an engineering activity is quite complex because it involves two types of contrasting intelligences: (i) Human intelligence which is rooted in informal expression, judgmental evaluation, inductive reasoning and commonsense, and (ii) The machine intelligence which is essentially based on formal expression, formal rule-based evaluation & deductive reasoning etc. Human intelligence is required for understanding the problem domains & their environments, and then for using the understanding for designing & developing solutions in such a form that it is understood and executed by the contrasting intelligence, viz. the machine intelligence. The proposed approach takes care of the facts of human capabilities being rooted in informality & of machine capabilities being purely formal. For this purpose, solutions conceived by human experts-which are generally expressed in some natural language-are, first of all, translated to semi-formal mathematical entities: recursive lists. These recursive lists then are easily translated to fully formal entities in some functional programming language like LISP or Haskell. In this communication, the approach is applied to structural aspects of web and is explained through sufficient exemplars. The dynamics of web will be discussed subsequently.

Out of the four main programming paradigms, it is widely considered that functional programming is the most promising. The programming languages that implement the functional paradigm generally do so either in a pure manner, such as Haskell, or by providing a multi-paradigm programming solution, such as most Lisp dialects, in order to allow side effects, which are proscribed under the former (pure) model. Nevertheless, tracking the execution steps of such a functional program remains challenging for the programmer. In this paper, the author addresses this issue by proposing a novel programming paradigm that combines the imperative programming approach based on a sequence of instructions with the pure function approach of functional programming, the objective being to retain the advantages of both strategies. This proposal is named “sequence of functions” (SOF), and its applicability and novelty are shown hereinafter throughout various examples and experiments.

The Universality, Parameter, and Recursion Theorems are three foundational results of classical computability theory. We show how these theorems can be programmatically illustrated and partially validated in Lisp. Our programs can be used as supplementary materials to texts on theoretical computer science, mathematical logic, or metamathematics.

The paper documents an application of the finite state model checker SPIN to formally analyze a multithreaded plan execution module. The plan execution module is one component of NASA's New Millennium Remote Agent, an artificial intelligence-based spacecraft control system architecture which launched in October of 1998 as part of the DEEP SPACE 1 mission. The bottom layer of the plan execution module architecture is a domain specific language, named ESL (Executive Support Language), implemented as an extension to multithreaded COMMON LISP. ESL supports the construction of reactive control mechanisms for autonomous robots and spacecraft. For the case study, we translated the ESL services for managing interacting parallel goal-and-event driven processes into the PROMELA input language of SPIN. A total of five previously undiscovered concurrency errors were identified within the implementation of ESL. According to the Remote Agent programming team, the effort has had a major impact, locating errors that would not have been located otherwise and, in one case, identifying a major design flaw. In fact, in a different part of the system, a concurrency bug identical to one discovered by this study escaped testing and caused a deadlock during an in-flight experiment, 96 million kilometers from Earth. The work additionally motivated the introduction of procedural abstraction in terms of inline procedures into SPIN.

An important and recurring security scenario involves the need to carry out trusted computations in the context of untrusted environments. It is shown how a tamper-resistant interpreter for a programming language-currently Lisp 1.5-combined with the use of a secure coprocessor can address this problem. This solution executes the interpreter on the secure coprocessor while the code and data of the program reside in the larger memory of an associated untrusted host. This allows the coprocessor to utilize the host's memory without fear of tampering even by a hostile host. This approach has several advantages including ease of use, and the ability to provide tamper-resistance for any program that can be constructed using the language. The language approach enabled the development of two novel mechanisms for implementing tamper resistance. These mechanisms provide alternatives to pure Merkle hash trees. Simulated relative performance of the various mechanisms is provided and shows the relative merits of each mechanism.

This paper presents how the manufacturing technologies are designed for the assembly of a single-cylinder engine block, four strokes, air-cooled. It is presented, from the constructive and technological point of view, the design stages of the main element of the core of an engine, respectively, the engine block. This engine is currently used on light vehicle categories such as ATVs, quads, and motorcycles. In the researches, activities are developed such as the following: designing of various digital technologies to achieve virtual prototype, obtaining a prototype using additive manufacturing technologies, and manufacturing the engine block using CNC technologies, under a range of unique products or small series. Many of the designing activities are materialized in an original software system, named GENgine, developed by authors using Open DCL and Visual LISP programming environments.

In recent years, wireless sensor network (WSN) is employed in many application areas such as monitoring, tracking, and controlling. For many applications of WSN, security is an important requirement. However, security solutions in WSN differ from traditional networks due to resource limitation and computational constraints. This paper analyzes security solutions: TinySec, IEEE 802.15.4, SPINS, MiniSEC, LSec, LLSP, LISA, and LISP in WSN. The paper also presents characteristics, security requirements, attacks, encryption algorithms, and operation modes. This paper is considered to be useful for security designers in WSNs.

Library learning is the process of building a library of common functionalities from a given set of programs. Typically, this process is applied in the context of aiding program synthesis: concise functions can help the synthesizer produce modularized code that is smaller in size. Previous work has focused on functional Lisp-like languages, as their regularity makes them more amenable to extracting repetitive structures. Our work introduces Leroy, which extends existing library learning techniques to imperative higher-level programming languages, with the goal of facilitating reusability and ease of maintenance. Leroy wraps the existing Stitch framework for library learning and converts imperative programs into a Lisp-like format using the AST. Our solution uses Stitch to do a top-down, corpus-guided extraction of repetitive expressions. Further, we prune abstractions that cannot be implemented in the programming language and convert the best abstractions back to the original language. We implement our technique in a tool for a subset of the Python programming language and evaluate it on a large corpus of programs. Leroy achieves a compression ratio of 1.04x of the original code base, with a slight expansion when the library is included. Additionally, we show that our technique prunes invalid abstractions.