US Food and Drug Administration Scholar in Residence at Kansas State
My research treats safety-critical programs, their specifications, and their executions as mathematical objects. Programs annotated with assertions as proof outlines can be transformed into complete proofs by my BLESS proof tool with human selection of tactics.