2015
Shield Synthesis: Runtime Enforcement for Reactive Systems
. Scalability issues may prevent users from verifying critical proper- ties of a complex hardware design. In this situation, we propose to synthesize a “safety shield” that is attached to the design to enforce the properties at run time. Shield synthesis can succeed where model c...