Lucas Wagner is a Senior Research Scientist with Rockwell Collins’ Advanced Technology Center. His principal area of expertise is applying formal analysis techniques, particularly model checking, to industrial problems. His background includes developing methods and tools to integrate formal methods into industrial development processes, and design of real-time embedded systems for safety-critical applications.
Most recently he led the Formal Methods Tool Qualification (FMTQ) project that investigated issues surrounding the use of formal methods tools within the DO-178C framework. This research fully explored issues regarding the qualification of theorem proving, model checking, and abstract interpretation tools. Further it investigated the concept of using proofs of correctness to enable independent verification of model checking results on the Kind 2 model checking tool.
He is the lead developer of two formal methods based analysis tools, SpeAR and SIMPAL. SpeAR is a requirements capture and analysis tool. It features a specification language useful for capturing requirements formally and analyses to determine the accuracy and consistency of the requirements set. SIMPAL is a tool for performing compositional reasoning on imperative programs. It is able to perform assume-guarantee reasoning about programs composed of pre-existing components.