1 SymPLFIED: Symbolic Program Level Fault Injection and Error Detection Framework

This paper introduces SymPLFIED, a program-level framework which allows specification of arbitrary error detectors and the verification of their efficacy against hardware errors. SymPLFIED comprehensively enu-merates all transient hardware errors in registers, memory and computation (expressed symbolically as value errors) that potentially evade detection and cause program failure. The framework uses symbolic execu-tion to abstract the state of erroneous values in the pro-gram and model checking to comprehensively find all errors that evade detection. We demonstrate the use of SymPLFIED on a widely deployed aircraft collision avoidance application, tcas. Our results show that the SymPLFIED framework can be used to uncover hard-to-detect corner cases caused by transient errors in programs that may not be exposed by random fault-injection based validation.