Papers

Security by Default - CHERI ISA Extensions coupled with a security-enhanced Ada runtime
Memory Safety in Ada, SPARK, and Rust
Should I choose Ada, SPARK, or Rust over C/C++?
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