Papers
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
Thoughts on Ada
High-Integrity Object-Oriented Programming in Ada
Compilation of Heterogeneous Models: Motivations and Challenges