Papers

Elevate Security Confidence with Memory Safe Hardware and Software

Co-Developing Programs and Their Proof of Correctness

Application of SMT in a Meta-Complier

NVIDIA: Using RecordFlux and SPARK to Implement SPDM for Secure Computing

The Work of Proof in SPARK

Dynamic Memory Management in Critical Embedded Software

Making Proofs of Floating-Point Programs Accessible to Regular Developers

Making FACETM Units of Conformance Fully Portable: Coding Guidance for Ada

Layered Formal Verification of a TCP Stack

Classification for Avionics Capabilities Enabled by Artificial Intelligence

How the Analyzer can Help the User Help the Analyzer

SPARK 2014 Reference Manual - Release 2020

Recursive Data Structures in SPARK

ParaSail: A Pointer-Free Pervasively-Parallel Language for Irregular Computations

Practical Application of SPARK to OpenUxAS

Lady Ada Mediates Peace Treaty in Endianness War

Safe Dynamic Memory Management in Ada and SPARK

Lightweight Interactive Proving inside an Automatic Program Verifier

Climbing the Software Assurance Ladder

SPARK 2014 User's Guide (Japanese)

A Comparison of SPARK with MISRA C and Frama-C

Towards Testing Model Transformation Chains Using Precondition Construction in Algebraic Graph Trans

SPARKSkein: A Formal and Fast Reference Implementation of Skein

Ada 2012 Rationale

Testing or Formal Verification: DO-178C Alternatives and Industrial Experience

High-Integrity Object-Oriented Programming in Ada

Compilation of Heterogeneous Models: Motivations and Challenges

Integrating Formal Program Verification with Testing

Formalization and Comparison of MCDC and Object Branch Coverage Criteria

The use of value numbers in static analysis.

Towards Certification of Object-Oriented Code with the GNAT Compiler

Couverture paper presented at ERTS² 2010

A principled approach to software engineering

Conflict-detection technology takes to the skies

Coverage and Free Software

Abstract Interface Types in GNAT: Conversions, Discriminants, and C++

Multi-Language Programming: The Challenge and Promise of Class-Level Interfacing

Exposing Uninitialized Variables: Strengthening and Extending Run-Time Checks in Ada

The Implementation of Ada 2005 Interface Types in the GNAT Compiler

Safety, Security, and Object-Oriented Programming

Certification & Object Orientation: The New Ada Answer

Safe and Secure Software - An invitation to Ada 2005

Ada 2005 Rationale

Ada 2005 for Mission-Critical Systems

Safety-Critical Design Techniques for Secure and Reliable Systems

Ada 2005 – Ready to Roll

Ada 2005 for High-Integrity Systems

The Implementation of Ada 2005 Synchronized Interfaces in the GNAT Compiler

Mission-Critical On-Board Software Using the Ada 95 Ravenscar Profile

The ESA Ravenscar Benchmark

Compile-time stack requirements analysis with GCC

GNAT Pro for On-Board Mission-Critical Space Applications

Dynamic Plug-in Loading with Ada

The Application of Compile-Time Reflection to Software Fault Tolerance using Ada 95

Ada 2005 Abstract Interfaces in GNAT

A Comparison of the Mutual Exclusion Features in Ada and the Real-Time Specification for Java

Vector Processing in Ada

Multilanguage Programming on the JVM: The Ada 95 Benefits

Exposing Memory Corruption and Finding Leaks: Advanced Mechanisms in Ada

A Comparison of the Asynchronous Transfer of Control Features in Ada and the Real-Time Specification

Real-Time Convergence of Ada and Java

High-Integrity Systems Development for Integrated Modular Avionics using VxWorks and GNAT

Quality Control in a Multi-Platform Multi-Product Software Company

The GNAT Implementation of Controlled Types

GtkAda: Design and Implementation of a High Level Binding in Ada

A Comparison of the Concurrency and Real-Time Features of Ada 95 and Java

A Comparison of the Object-Oriented Features of Ada 95 and Java