# Program Faults and Verification

[Fault detection](https://en.wikipedia.org/wiki/Fault_detection_and_isolation), and [program validation](https://en.wikipedia.org/wiki/Software_verification_and_validation), and [formal validation](https://en.wikipedia.org/wiki/Formal_verification) are highly interrelated topics.  Each deal with proving or disproving the correctness of systems as intended, and the classification of incorrect behavior.


## Program Verification

* [Coq: The world’s best macro assembler?](https://research.microsoft.com/en-us/um/people/nick/coqasm.pdf)
* :scroll: [Epitaxis: a system for syntactic and semantic software queries](epitaxis-a-system-for-syntactic-and-semantic-software-queries.pdf)

## Fault Protection

* [GN&C Fault Protection Fundamentals](https://trs.jpl.nasa.gov/bitstream/handle/2014/41696/08-0125.pdf)
> As software becomes more and more integrated in our daily lives, we
> need, more than ever, for the software we write to work reliably in a
> wide range of conditions--even, and especially, in unexpected
> conditions. This paper, written by Robert Rasmussen from the Jet
> Propulsion Laboratory in 2008, documents and explains some fundamental
> principles about designing fault tolerant systems as learned through
> the hard-won experience of designing Guidance, Navigation, and Control
> (GN&C) systems for spacecraft. This paper is rich in principles,
> examples, and advice, and has a lot to offer to our industry
> generally--even for those of us who don't actively work on software for
> spaceships!