76
76
Oct 7, 2015
10/15
by
Shimeall, Timothy J.
texts
eye 76
favorite 0
comment 0
Title from cover
Topic: COMPUTER PROGRAM VERIFICATION.,LIBRARIES.
Title from cover
Topics: COMPUTER PROGRAM VERIFICATION., LIBRARIES.
Naval Postgraduate School
144
144
Jan 15, 2013
01/13
by
Shimeall, Timothy J.;Bolchoz, John Manning.;Griffin, Rachel.
texts
eye 144
favorite 0
comment 0
Title from cover
Topics: COMPUTER PROGRAM RELIABILITY., COMPUTER PROGRAM VERIFICATION.
88
88
Oct 8, 2015
10/15
by
Shimeall, Timothy J.;Bolchoz, John Manning.;Griffin, Rachel.
texts
eye 88
favorite 0
comment 0
Title from cover
Topic: COMPUTER PROGRAM RELIABILITY.,COMPUTER PROGRAM VERIFICATION.
82
82
Oct 8, 2015
10/15
by
Luqi.;Shing, Man-Tak.;Berzins, Valdis Andris.;Chmura, Lou.
texts
eye 82
favorite 0
comment 0
Title from cover
Topic: COMPUTER PROGRAM RELIABILITY.,COMPUTER PROGRAM VERIFICATION.
Naval Postgraduate School
220
220
Jan 24, 2013
01/13
by
Luqi.;Shing, Man-Tak.;Berzins, Valdis Andris.;Chmura, Lou.
texts
eye 220
favorite 0
comment 0
Title from cover
Topics: COMPUTER PROGRAM RELIABILITY., COMPUTER PROGRAM VERIFICATION.
Cover title
Topics: PROTOTYPES., SOFTWARE ENGINEERING., COMPUTER PROGRAMS., COMPUTER PROGRAM VERIFICATION.,...
78
78
Oct 6, 2015
10/15
by
Dampier, David A.;Luqi.
texts
eye 78
favorite 0
comment 0
Cover title
Topic: PROTOTYPES.,SOFTWARE ENGINEERING.,COMPUTER PROGRAMS.,COMPUTER PROGRAM VERIFICATION.,ASSIMILATION.
The purpose of this Validation Summary Report is to present the results and conclusions of performing standardized tests on the Verdix Ada compiler (VADS). The VADS is hosted on the VAX-11/785 computer operating under ULTRIX 1.0. The suite of tests known as the Ada Compiler Validation Capability (ACVC), Version 1.5, was used. The ACVC suite of tests is used to validate conformance of the compiler to ANSI/MIL-STD-1815A (ADA). The purpose of the testing is to ensure that the compiler properly...
Topics: DTIC Archive, SOFTECH INC FAIRBORN OH, *COMPILERS, VALIDATION, COMPUTER PROGRAM VERIFICATION, LABELS
The dependencies in complex software systems are stretching industry software test capabilities such that schedules and budgets are constantly being compromised at the risk of producing software with more defects and reliability issues. STAT technologies are being integrating within our production code to facilitate improved testability and reliability. Modeled from techniques utilized in hardware systems commonly titled Built-in Test (BIT), STAT is used to develop applications that support...
Topics: DTIC Archive, CRAFT DESIGNS INC HUNTSVILLE AL, *COMPUTER PROGRAM RELIABILITY, *COMPUTER PROGRAM...
Deciding equivalence between two programs (called a source and a target program) is often reduced to finding a simulation relation between them. This is computationally expensive and often requires a manual guidance. In this paper, we propose an abstraction-refinement-guided approach, called SimAbs, to automatically construct a simulation relation between the source program and an abstraction of the target program. In our approach both the abstraction and the simulation relation are discovered...
Topics: DTIC Archive, CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST, *COMPUTER PROGRAM...
We describe several techniques for verifying infinite-state systems via finite-state abstractions. Diagrams are top-down property-driven abstractions, which are especially suited for compositional, assume-guarantee reasoning. Predicate abstraction uses a bottom-up approach for generating abstractions; invariant generation techniques are applied to automatically generate the required predicates. Extended finite-state abstractions allow inclusion of extra information produced by the deductive...
Topics: DTIC Archive, Manna, Zohar, STANFORD UNIV CA DEPT OF COMPUTER SCIENCE, *COMPUTER PROGRAM...
As computers have become a pivotal component of daily lives, computer safety, reliability, and security issues have become enormously important. A considerable amount of recent research in program analysis and software engineering has been carried out on techniques and tools for finding software bugs and security vulnerabilities, and on checking computer-safety properties. Most of this research has focused on analyzing source code. Recently, machine-code analysis has begun to receive great...
Topics: DTIC Archive, WISCONSIN UNIV MADISON, *COMPUTER PROGRAM VERIFICATION, COMPILERS, COMPUTER...
As the DoD continues to become software reliant, rigorous techniques to assure the correct behavior of programs are in great demand. Software model checking (SMC) is a promising candidate, but its scalability remains unsatisfactory. Recent years have seen the emergence of HPC technologies, e.g., multi-core processors and clusters. Yet, few software model checkers are designed to use this cheap and abundant computing power. A key reason is that model checking is at its core a graph search --...
Topics: DTIC Archive, CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST, *COMPUTER PROGRAM...
The military relies heavily on computer systems. Without a strong method of authentication to access these systems, threats to confidentiality,integrity, and availability of government information are likely to be more successful. A recent method of authentication forthe Windows 8 and Windows 10 operating systems is picture gesture authentication (PGA), a new approach to entering a password toauthenticate a user during system login. Each PGA password is composed of three gestures that are drawn...
Topics: DTIC Archive, Monroy,Pauline, Naval Postgraduate School Monterey United States, COMPUTER PROGRAMS,...
While the last decade has witnessed great advances in assuring high software quality through static verification against software hazards and unexpected behavior, the field has pretty much focused on statically verifying software applications against common properties to detect common programming problems such as incorrect usage of memory pointers. But most quality issues such as correctness, security, and robustness violations are caused by the incorrect usage of application programming...
Topics: DTIC Archive, NORTH CAROLINA STATE UNIV AT RALEIGH, *COMPUTER PROGRAM VERIFICATION, COMPUTER...
Software has a huge and negative impact on the economy. Formal verification is an effective method to check whether a piece of software contains certain kinds of errors. Defense Advanced Research Projects Agency (DARPA) started the Crowd Sourced Formal Verification (CSFV) program to propose a new model for formal verification by using five online games. CSFV aims to explore whether an online game player with no formal verification expertise can achieve formal verification more efficiently than...
Topics: DTIC Archive, Yilmaz,Mehmet, Naval Postgraduate School Monterey United States, computer program...
This paper describes how formal methods were used to produce evidence in a certification, based on the Common Criteria, of a security-critical software system. The evidence included a top level specification (TLS) of the security-relevant software behavior, a formal statement of the required security properties, proofs that the specification satisfied the properties, and a demonstration that the source code, which had been annotated with preconditions and postconditions, was a refinement of the...
Topics: DTIC Archive, NAVAL RESEARCH LAB WASHINGTON DC, *COMPUTER PROGRAM VERIFICATION, SPECIFICATIONS,...
The increasing complexity of current uninhabited aerial vehicle (UAV) missions is overwhelming human mission developers, and automated mission planning systems and simulation environments. The objective of this project was to enhance the dependability of complex UAV missions with the application of modern automated program analysis techniques. The key insight supporting this project was the treatment of a mission plan as a type of software or software representation, which could be analyzed...
Topics: DTIC Archive, UNIVERSITY COLL LONDON (UNITED KINGDOM), *DRONES, AUTOMATION, COMPUTER PROGRAM...
This report presents the findings of a study to evaluate the maturity of the software development process and its accompanying standards, project future development in the field, and to identify areas needing standards and the means for achieving the required standardization. The report examines development as a generic process to provide a perspective for describing the evolution and present state of software engineering. The purpose and contributions of standards in development are defined...
Topics: DTIC Archive, SCIENCE APPLICATIONS INC MCLEAN VA, *COMPUTER PROGRAMS, *COMPUTER ARCHITECTURE,...
FORMED integrates formal verification into software design and development by precisely defining semantics for a restricted subset of the Unified Modeling Language and transforming application models into both an ACL2s formal specification for analysis and Java code for deployment. Correspondence testing verifies consistent translation and executable behavior between the formal and deployed implementations. Key properties addressed include termination, input-output contract satisfaction and...
Topics: DTIC Archive, Reubenstein,Howard, BAE SYSTEMS Burlington United States, COMPUTER PROGRAM...
In a Multi-Variant Execution Environment (MVEE), several slightly different versions of the same program are executed in lockstep. While this is done, a monitor compares the behavior of the versions at certain synchronization points with the aim of detecting discrepancies which may indicate attacks. A fully functions MVEE has been built and evaluated. The implemented system can successfully detect previously unknown attacks in real time, in exchange for a small runtime penalty.
Topics: DTIC Archive, CALIFORNIA UNIV IRVINE, *COMPUTER PROGRAMMING, *COMPUTER PROGRAM VERIFICATION,...
Topics: DTIC Archive, CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST, *COMPUTER PROGRAM...
Formal verification (FV) ensures that mission-essential software is free from disruptive errors and security vulnerabilities, but requires human experts that can be quickly overwhelmed by the increasing number, size, and complexity of software systems. DARPAs Crowd Sourced Formal Verification (CSFV) program built games that recast FV problems into puzzles to make these problems more accessible, increasing the manpower to construct FV proofs. This effort supported the CSFV program by hosting the...
Topics: DTIC Archive, Guarino,Sean, Charles River Analytics, Inc. Cambridge United States, Computer program...
The purpose of this Validation Summary Report is to present the results and conclusions of performing standardized tests on the Verdix Ada compiler. On-site testing was performed 28-30 APR 85 at Verdix Western Operations in Aloha, Oregon, under the auspices of the Ada Validation Facility, according to the Ada Validation Office policies and procedures. The Verdix Ada compiler (Verdix Ada Development System (VADS), VAda-010-1010) is hosted on the Sun Microsystems Model 2/120 computer operating...
Topics: DTIC Archive, SOFTECH INC FAIRBORN OH, *COMPUTER PROGRAM VERIFICATION, *COMPILERS, POLICIES,...
Testing software applications on OS/2 Warp was my major job responsibility. This included receiving applications from independent vendors and testing them in a laboratory with other members on the test team. If the application passed, it would receive a seal to be placed on the application when it is placed on the market; however, if it failed, we would try to work with the vendor to correct the bug(s) and enable it to run on IBM's platforms. The other area of concentration was with HTML...
Topics: DTIC Archive, Wall, Yolanda, GRAMBLING STATE UNIV LA, *SOFTWARE ENGINEERING, *HYPERTEXT, OPERATING...
Initially, the primary goal of the project was to develop techniques for making systems safe from mobile programs. During the course of the project, several important results were achieved in security, resource scheduling, runtime system design, and distributed programming environments. These results include an access control specification language, novel tools and techniques for enforcing security policies, safe threads package, resource scheduling algorithms for protecting against denial of...
Topics: DTIC Archive, Pandey, Raju, CALIFORNIA UNIV DAVIS, *SOFTWARE ENGINEERING, *COMPUTER PROGRAM...
Mature engineering fields have methods of construction that have high likelihoods of success, and that guarantee the proper functioning of systems, even within hostile environments. These methods relate behavior to structure and have underlying notions of composition related to the implementation domain. Unfortunately, the construction of computer systems has not yet reached the same level of maturity. While many mathematical theories have been developed, they have in yet been brought into...
Topics: DTIC Archive, Zhou, Dan, SYRACUSE UNIV NY, *SOFTWARE ENGINEERING, *COMPUTER PROGRAM VERIFICATION,...
The goal of the Havoc project was to explore new proof techniques and methodologies that would enable scalable and modular verification of modern concurrent programming languages like Java or C# . The efforts undertaken during the lifetime of this effort focused on (a) new proof techniques, specifically the use of refinement methods and tactics to simplify reasoning about interferences in proving invariants about concurrent code; (b) incorporating precise notions of memory models, both at the...
Topics: DTIC Archive, Jagannathan,Suresh, Purdue University West Lafayette United States, COMPUTER PROGRAM...
The Ada implementation described above was tested according to the Ada Validation Procedures Pro90 against the Ada Standard Ada83 using the current Ada Compiler Validation Capability (ACVC). This Validation Summary Report (VSR) gives an account of the testing of this Ada implementation.
Topics: DTIC Archive, NATIONAL INST OF STANDARDS AND TECHNOLOGY GAITHERSBURG MD, *ADA PROGRAMMING LANGUAGE,...
This final report summarizes the work completed for the project entitled Porting m-EVES to Common Lisp. Section 2 places the contracted work within the context of the m-EVES project. Section 3 outlines the project, the statement of work, and amendments to the initial contract. The approach used to meet the contractual obligations are summarized in Section 4. The difficulties encountered during the project are discussed in Section 5. Section 6 lists the documents and software delivered at the...
Topics: DTIC Archive, Pase, Bill, SHARP (I P) ASSOCIATES LTD OTTAWA (ONTARIO), *COMPUTER PROGRAM...
The goal of this brief effort was to determine the feasibility of developing a process that verifies if critical information system software patches behave as intended and introduce only the specific functionality identified for the patch. Based on our research, examination and experimentation, we have not only determined that it would be feasible to develop such a process, but also that this process and associated technology and standards are desperately needed.
Topics: DTIC Archive, Hosmer, Chester, WETSTONE TECHNOLOGIES CORTLAND NY, *COMPUTER PROGRAM VERIFICATION,...
Most standard approaches to the static analysis of programs, such as the popular worklist method, are first-order methods that inductively annotate program points with abstract values. In [6] we introduced a second-order approach based on Kleene algebra. In this approach, the primary objects of interest are not the abstract data values, but the transfer functions that manipulate them. These elements form a left-handed Kleene algebra. The data flow labeling is not achieved by inductively...
Topics: DTIC Archive, Kozen,Dexter, Cornell University Ithaca United States, COMPUTER PROGRAM VERIFICATION,...
Formal software verification methods and tools have made significant progress in their ability to model software designs and prove correctness theorems about the systems modeled. General adoption of these techniques has had limited penetration in the software development community. Two interrelated causes may account for barriers to adoption. First, many tools prove properties about models of the system as opposed to the actual implementation. Software engineers ultimately need to produce...
Topics: DTIC Archive, Reubenstein,Howard, BAE Systems Burlington United States, SOFTWARE ENGINEERING,...
The paper presents a minimal proof theory which is adequate for proving the main important temporal properties of reactive programs. The properties we consider consist of the classes of invariance, response, and precedence properties. For each of these classes we present a small set of rules that is complete for verifying properties belonging to this class. We illustrate the application of these rules by analyzing and verifying the properties of a new algorithm for mutual exclusion.
Topics: DTIC Archive, Manna, Zohar, STANFORD UNIV CA DEPT OF COMPUTER SCIENCE, *COMPUTER PROGRAM...
RTware is working on a proposal for an SBIR Phase II software research and development project for distributed control systems (DCS) using Module Interconnect Frameworks (MIF). SBIR Phase I work includes research into the feasibility, design and benefits of such a system, resulting in a detailed Phase II proposal. The proposed software package will be based on RTware's ControlCalc real-time spreadsheet control system and the Polylith MIF system from the University of Maryland. The prior...
Topics: DTIC Archive, Clarke, Richard, RTWARE INC DURHAM NC, *SOFTWARE ENGINEERING, *REAL TIME, *COMPUTER...
Existing formal verification methods do not handle systems that combine state machines and data paths very well. Model checking deals with finite-state machines efficiently, but model checking full designs is infeasible because of the large amount of state in the data path. Theorem-proving methods may be effective for verifying data path operations, but verifying the control requires finding and proving inductive invariants that characterize the reachable states of the system. We present a new...
Topics: DTIC Archive, Su, Jeffrey, STANFORD UNIV CA COMPUTER SYSTEMS LAB, *PATTERN RECOGNITION, *COMPUTER...
The purpose of this Technical Report is to review the Final Software Test Description, CDRL A009-03, which was produced for the Government by Evaluation Research Corporation. The results are provided in the form of Data Item Discrepancy worksheets as requested by the CMOS Program Office. (kr)
Topics: DTIC Archive, SCIENCE APPLICATIONS INTERNATIONAL CORP O'FALLON IL, *COMPUTER PROGRAM VERIFICATION,...
This report presents a basic set of guidelines to facilitate the generation of expected properties in the context of Model-Based Verification. Expected properties are natural language statements that express characteristics of the behavior of a system-characteristics that are consistent with user expectations. Through model checking, expected properties of a system, formally expressed as claims, are analyzed against the model. This analysis can detect inconsistencies between models of the...
Topics: DTIC Archive, Gluch, David P, CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST,...
The goal of this project was the development of formal methods for the specification and verification of concurrent programs to help avoid software errors in concurrent systems. This involved research in three areas: Specification; Verification; and Semantics. Contents: What It Means for a Concurrent Program to Satisfy a Specification; An Axiomatic Semantics of Concurrent Programming Languages; Constraints - A Uniform Approach to Aliasing and Typing.
Topics: DTIC Archive, Lamport,L, SRI INTERNATIONAL MENLO PARK CA, *COMPUTER PROGRAM VERIFICATION,...
Three variants of multi-threaded ic3 are presented. Each variant has a fixed number of ic3s running in parallel, and communicating by sharing lemmas. They differ in the degree of synchronization between threads, and the aggressiveness with which proofs are checked. The correctness of all three variants is shown. The variants have unpredictable runtime. On the same input, the time to find the solution over different runs varies randomly depending on the thread interleaving. The use of a...
Topics: DTIC Archive, CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST, *ALGORITHMS, COMPUTER...
The goal of the project was to augment PVS with features that simplified the construction and management of proofs, and to document the PVS functions needed for writing proof strategies. The extensions to PVS developed in this project include: (1) Multiple-proof maintenance, (2) Comments in proofs, (3) Labeling and accessing sequent formulas, (4) Rerunning proofs with checkpoints, (5) Deconstructing EXPAND, and (6) Saved SKIP command.
Topics: DTIC Archive, Shankar, Natarajan, SRI INTERNATIONAL MENLO PARK CA, *COMPUTER PROGRAMMING, *COMPUTER...
The primary goal of this project has been to improve the degree of automation in the ACL2 when proving theorems about computer programs. We have paid particular attention to fixed-width integer arithmetic and the Java Virtual Machine (JVM). Our work has proceeded on three fronts. We have begun developing an approach for automating much of the detail work involved in applying the ACL2 method for proving theorems about low-level programs. Work completed includes a prototype tool targeting the...
Topics: DTIC Archive, Golden, Jeff, TEXAS UNIV AT AUSTIN, *AUTOMATION, *COMPUTER PROGRAM VERIFICATION,...
This report documents the development of the Advanced Unified Electromagnetic (EM) Design software, including verification and validation. This briefing looks at the software tools available through the program.
Topics: DTIC Archive, ATK MISSION RESEARCH NEWINGTON VA, *COMPUTER PROGRAM VERIFICATION, *DESIGN CRITERIA,...
Using the notion of progress measures, we give a complete verification method for proving that a program satisfies a property specified by an automaton having bounded nondeterminism. Such automata can express any safety property. Previous methods, which can be derived from the method presented here, either rely on transforming the program or are not complete. (kr)
Topics: DTIC Archive, Klarlund, Nils, CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE, *COMPUTER PROGRAM...
This tutorial introduces program verification with Penelope and Penelope's proof editor. Penelope incrementally generates verification conditions for a program, and the proof of those verification conditions implies that the program meets its specifications. Penelope's proof editor supports proofs of the verification conditions in ordinary first-order logic. We present the proof rules for Penelope, and discuss specification and proof strategies by means of examples. Ada, Larch, Larch/Ada,...
Topics: DTIC Archive, Hird, Geoffrey, ORA CORP ITHACA NY, *COMPUTER PROGRAM VERIFICATION, *ADA PROGRAMMING...
Formal software verification methods and tools have made significant progress in their ability to model software designs and prove correctness theorems about the systems modeled. General adoption of these techniques has had limited penetration in the software development community. Two interrelated causes may account for barriers to adoption. First, many tools prove properties about models of the system as opposed to the actual implementation. Software engineers ultimately need to produce...
Topics: DTIC Archive, Reubenstein,Howard, BAE SYSTEMS Burlington United States, COMPUTER PROGRAM...
Traditional methods for proving program correctness the implementation-dependent specification methods. If abstract specifications are also used, these methods require a leap of faith to bridge the gap between an abstract specification and a program correctness statement. In this report the trace method of software specification is extended to provide a natural semantics for procedural programming languages. This extension is compared with other approaches for the giving program semantics and...
Topics: DTIC Archive, McLean,John, NAVAL RESEARCH LAB WASHINGTON DC, *COMPUTER PROGRAM VERIFICATION,...
This Validation Summary Report describes the extent to which a specific Ada compiler conforms to the Ada Standard, ANSI/MIL-STD-1815A. This report explains all technical terms used within it and thoroughly reports the results of testing this compiler using the Ada Compiler Validation Capability. An Ada compiler must be implemented according to the Ada Standard, and any implementation-dependent features must conform to the requirements of the Ada Standard. The Ada Standard must be implemented in...
Topics: DTIC Archive, INDUSTRIEANLAGEN-BETRIEBSGESELLSCHAFT M B H OTTOBRUNN (GERMANY F R), *COMPILERS, *ADA...
Critical missions require the guarantees provided through formal verification and functional programming. This provides a strong basis for decisions that must be assured in a contested cyber environment. We present a framework for educating future cyber leaders on these important concepts and tools.
Topics: DTIC Archive, AIR FORCE RESEARCH LAB ROME NY INFORMATION DIRECTORATE, *COMPUTER PROGRAM...
