scholarly journals Industrial hardware and software verification with ACL2

2017 ◽  
Vol 375 (2104) ◽  
pp. 20150399 ◽  
Author(s):  
Warren A. Hunt ◽  
Matt Kaufmann ◽  
J Strother Moore ◽  
Anna Slobodova
Keyword(s):  
Programming Language ◽  
Software Verification ◽  
Formal Analysis ◽  
Shared Vision ◽  
Theorem Prover ◽  
Software Systems ◽  
Levels Of Abstraction ◽  
Quarter Century ◽  
Industrial Use ◽  
Technical Features

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’.

An Open Architecture Framework for the Integration of Virtual Prototyping Software Tools

1997 ◽  
Author(s):  
Uma Jayaram ◽  
Sankar Jayaram ◽  
Donald Tilton ◽  
Kevin Seaney
Keyword(s):  
Virtual Prototyping ◽  
Integrated Design ◽  
Open Architecture ◽  
Design Solution ◽  
Software Systems ◽  
Levels Of Abstraction ◽  
Code Generator ◽  
Nc Code ◽  
Systems Research ◽  
Architecture Framework

Abstract The use of virtual prototyping tools typically results in products with lower costs, better quality, and shorter development cycles. However, there are many interface/configuration problems that occur in the process of obtaining a design solution using the typical gamut of virtual prototyping tools. This paper presents the architecture, design, and implementation of a framework to support the integration of the multiple software systems used in the virtual prototyping of mechanical components. Some of the virtual prototyping software systems considered in the implementation of this framework were customer input systems, solid modeling systems, finite-element systems, knowledge-based systems, NC code generator systems, and virtual assembly systems. There is a pressing need for the different software systems to talk to each other while transferring the required data at varying levels of abstraction without compromising data integrity. Of special significance is the fact that the philosophy of the framework is widely applicable to any mechanical system, and is almost independent of specific software utilities. Thus, this design incorporates a clear path towards expansion to encompass other independent tools/systems. The architecture was designed using object-oriented methods. The framework was very successfully demonstrated for a well-defined subset of software systems being used at Isothermal Systems Research (ISR) Inc., a leader in proprietary spray cooling systems for multi-chip modules. This framework effectively supports the strong industry push towards integrated design, manufacturing, and virtual prototyping. The work presented in this paper was supported by an SBIR grant from the Department of Commerce, DOC contract 50-DKNB-5-00117.

Formal Approaches to Systems Analysis Using UML

2002 ◽  
pp. 324-341
Author(s):  
Jonathan Whittle
Keyword(s):  
Formal Methods ◽  
Development Strategy ◽  
Ad Hoc ◽  
Formal Analysis ◽  
Daily Basis ◽  
Software Systems ◽  
Industry Standard ◽  
Mathematical Techniques ◽  
Software Lifecycle ◽  
Modeling Level

Formal methods, whereby a system is described and/or analyzed using precise mathematical techniques, is a well-established and yet, under-used approach for developing software systems. One of the reasons for this is that project deadlines often impose an unsatisfactory development strategy in which code is produced on an ad hoc basis without proper thought about the requirements and design of the piece of software in mind. The result is a large, often poorly documented and un-modular monolith of code that does not lend itself to formal analysis. Because of their complexity, formal methods work best when code is well structured, e.g., when they are applied at the modeling level. UML is a modeling language that is easily learned by system developers and, more importantly, an industry standard, which supports communication between the various project stakeholders. The increased popularity of UML provides a real opportunity for formal methods to be used on a daily basis within the software lifecycle. Unfortunately, the lack of precision of UML means that many formal techniques cannot be applied directly. If formal methods are to be given the place they deserve within UML, a more precise description of UML must be developed. This chapter surveys recent attempts to provide such a description, as well as techniques for analyzing UML models formally.

scholarly journals Higher-order theorem proving and its applications

2019 ◽  
Vol 61 (4) ◽  
pp. 187-191
Author(s):  
Alexander Steen
Keyword(s):  
Theorem Proving ◽  
Formal Analysis ◽  
Logical Consequence ◽  
Effective Means ◽  
Industrial Applications ◽  
Higher Order ◽  
Hardware Verification ◽  
Theorem Prover ◽  
Computer Assisted ◽  
Higher Order Logic

Abstract Automated theorem proving systems validate or refute whether a conjecture is a logical consequence of a given set of assumptions. Higher-order provers have been successfully applied in academic and industrial applications, such as planning, software and hardware verification, or knowledge-based systems. Recent studies moreover suggest that automation of higher-order logic, in particular, yields effective means for reasoning within expressive non-classical logics, enabling a whole new range of applications, including computer-assisted formal analysis of arguments in metaphysics. My work focuses on the theoretical foundations, effective implementation and practical application of higher-order theorem proving systems. This article briefly introduces higher-order reasoning in general and presents an overview of the design and implementation of the higher-order theorem prover Leo-III. In the second part, some example applications of Leo-III are discussed.

Occam in the specification and verification of microprocessors

1992 ◽  
Vol 339 (1652) ◽  
pp. 137-151 ◽  
Keyword(s):  
Programming Language ◽  
Vlsi Circuits ◽  
Hardware Verification ◽  
Floating Point ◽  
Algebraic Semantics ◽  
Levels Of Abstraction ◽  
Close Relationship ◽  
Floating Point Unit ◽  
Implementation Level ◽  
Formal Techniques

Occam is a parallel programming language which can be used to describe VLSI circuits at several levels of abstraction. For a given piece of hardware one might have one Occam description which is close to the implementation level and another which is close to a specification in a notation such as Z or CSP. Thus a design can be substantially verified by a proof of equivalence of such descriptions. This can sometimes be achieved by using transformations based on the algebraic semantics of Occam and, even where this is not possible, the clean design and semantics of Occam make other formal techniques either easier or more reliable. We discuss several case studies: the floating point unit of the IMS T800 transputer and various aspects of its successor, the IMS T9000. Despite the close relationship, on the surface, of these cases studies, radically different techniques were required for them. Based on this and other evidence, the author believes that one of the most important possessions when starting to tackle problems in hardware verification, at least at current levels of knowledge and technology, is an open mind.

scholarly journals CRITERIA FOR ACCEPTING SOFTWARE REQUIREMENTS NEGOTIATION TOOLS IN THE SOFTWARE INDUSTRY

2020 ◽  
Vol 2 (1) ◽  
pp. 39-45
Author(s):  
Shamsu Abdullahi ◽  
Abubakar Zakari ◽  
Amina Nura ◽  
Abdulfatah Samaila Mashasha ◽  
Haruna Abdu ◽  
...  
Keyword(s):  
Software Industry ◽  
Shared Vision ◽  
Negotiation Process ◽  
Ease Of Use ◽  
Perceived Usefulness ◽  
Process Models ◽  
Software Requirements ◽  
Software Systems ◽  
Perceived Ease Of Use ◽  
Requirements Negotiation

Requirements negotiation is a centralized process of making a decision in order to resolve conflicts in the requirements of the stakeholder. The negotiation will enable the shared vision of software to be developed among the heterogeneous stakeholder in the software industry to be achieved. Many process models used for the negotiation of stakeholder’s requirements have been proposed for the software industry by the research community, yet the acceptance of these process models is discouraging. This study tends to investigate the inadequate adoption of requirements negotiation process models. Further, it finds the acceptance criteria for the software industry to adopt requirements negotiation models. Finding shows that the software industries do not adopt the process models. The perceived usefulness, perceived ease of use and many more criteria have been identified through the literature review on the general criteria of software systems acceptance.

scholarly journals Implementing type theory in higher order constraint logic programming

2019 ◽  
Vol 29 (8) ◽  
pp. 1125-1150
Author(s):  
FERRUCCIO GUIDI ◽  
CLAUDIO SACERDOTI COEN ◽  
ENRICO TASSI
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Type System ◽  
Theorem Prover ◽  
Type Checking ◽  
Language Extension ◽  
Order Constraint ◽  
Simple Implementation ◽  
Calculus Of Inductive Constructions ◽  
High Level

In this paper, we are interested in high-level programming languages to implement the core components of an interactive theorem prover for a dependently typed language: the kernel – responsible for type-checking closed terms – and the elaborator – that manipulates open terms, that is terms containing unresolved unification variables.In this paper, we confirm that λProlog, the language developed by Miller and Nadathur since the 80s, is extremely suitable for implementing the kernel. Indeed, we easily obtain a type checker for the Calculus of Inductive Constructions (CIC). Even more, we do so in an incremental way by escalating a checker for a pure type system to the full CIC.We then turn our attention to the elaborator with the objective to obtain a simple implementation thanks to the features of the programming language. In particular, we want to use λProlog’s unification variables to model the object language ones. In this way, scope checking, carrying of assignments and occur checking are handled by the programming language.We observe that the eager generative semantics inherited from Prolog clashes with this plan. We propose an extension to λProlog that allows to control the generative semantics, suspend goals over flexible terms turning them into constraints, and finally manipulate these constraints at the meta-meta level via constraint handling rules.We implement the proposed language extension in the Embedded Lambda Prolog Interpreter system and we discuss how it can be used to extend the kernel into an elaborator for CIC.

scholarly journals Abstracting Strings for Model Checking of C Programs

2020 ◽  
Vol 10 (21) ◽  
pp. 7853
Author(s):  
Henrich Lauko ◽  
Martina Olliaro ◽  
Agostino Cortesi ◽  
Petr Roc̆kai
Keyword(s):  
Programming Language ◽  
Software Verification ◽  
Model Checker ◽  
Shape Information ◽  
C Programs ◽  
C Programming Language ◽  
C Programming ◽  
Array Structure ◽  
Two Parameters ◽  
Selection Of

Data type abstraction plays a crucial role in software verification. In this paper, we introduce a domain for abstracting strings in the C programming language, where strings are managed as null-terminated arrays of characters. The new domain M-String is parametrized on an index (bound) domain and a character domain. By means of these different constituent domains, M-Strings captures shape information on the array structure as well as value information on the characters occurring in the string. By tuning these two parameters, M-String can be easily tailored for specific verification tasks, balancing precision against complexity. The concrete and the abstract semantics of basic operations on strings are carefully formalized, and soundness proofs are fully detailed. Moreover, for a selection of functions contained in the standard C library, we provide the semantics for character access and update, enabling an automatic lifting of arbitrary string-manipulating code into our new domain. An implementation of abstract operations is provided within a tool that automatically lifts existing programs into the M-String domain along with an explicit-state model checker. The accuracy of the proposed domain is experimentally evaluated on real-case test programs, showing that M-String can efficiently detect real-world bugs as well as to prove that program does not contain them after they are fixed.

Source Code Analysis: Current and Future Trends & Challenges

2016 ◽  
Vol 685 ◽  
pp. 877-880
Author(s):  
Alexey Ponomarev ◽  
Hitesh S. Nalamwar ◽  
Ragesh Jaiswal
Keyword(s):  
Programming Language ◽  
System Architecture ◽  
False Positive ◽  
Time Complexity ◽  
State Of The Art ◽  
Source Code ◽  
Software Systems ◽  
Future Trends ◽  
Source Code Analysis ◽  
Code Analysis

The increasing complexity of software systems is making source code analysis a more economic option to automate the identification of defects, vulnerabilities and inefficiencies. This paper initially outlines the general anatomy of automatic source code analyzers, dimensions of analysis that can be performed with today’s state-of-the-art tools, various limitations of automatic source code analysis in the areas of programming language coverage, quantity of false positive claims, system architecture breakdowns and code/time complexity. The paper is concluded by presenting future tentative trends of source code analysis.

Sign in / Sign up

Export Citation Format

Share Document