Formal Verification of Real-Time Function Blocks Using PVS. - Linna Pang; Chen-Wei Wang; Mark Lawford; Alan Wassyng; Josh Newell; Vera Chow; David Tremaine (ESSS, 2015)

Formal Translation of IEC 61131-3 Function Block Diagrams to PVS with Nuclear Application. - Josh Newell; Linna Pang; David Tremaine; Alan Wassyng; Mark Lawford (NFM, 2016)

Translation of IEC 61131-3 Function Block Diagrams to PVS for Formal Verification with Real-Time Nuclear Application. - Josh Newell; Linna Pang; David Tremaine; Alan Wassyng; Mark Lawford (J. Autom. Reason., 2018)