Overview
I’m a University Distinguished Professor and Lucas-Rathbone Professor of Engineering (brief bio sketch,full CV) in the Computer Science Department at Kansas State University, and (along with Professor Robby) I lead the laboratory for Specification, Analysis, and Transformation of Software (SAnToS). SAnToS aims to develop and mature technologies and tools for effective construction of high-confidence software systems.
SAnToS Laboratory emphasizes a research methodology in which research advances are achieved by building robust tools that can be applied to and evaluated against real systems in the context of realistic development practices, and then using insights gained in these evaluations to guide future research directions and priorities. In these efforts, we rely on extensive interaction with our industrial partners to gain insight into particular foundational advances and tool capabilities that will be necessary to affect practice. SAnToS tools have been used in a number of academic research groups world-wide and in projects by engineers at Boeing (Phantom Works, St. Louis), Lockheed Martin, Collins Aerospace, and Galois, Inc.
Here are some notable achievements of the group across the years:
- members of the NASA Java Pathfinder Team that in 2003 received NASA’s Turning Goals Into Reality (TGIR) Award – one of fifteen awards given to NASA projects in 2003 that best demonstrated progress toward NASA’s mission objectives,
- members received two major professional society awards – ACM SIGSOFT’s prestigious Impact Paper Award, and International Conference of Software Engineering (ICSE) Most Influential Paper Award for their original paper on the Bandera software model checking framework. Both of these awards are retrospective awards given by the world’s primary professional organization of software engineers and the world’s largest software engineering conference to the paper that has had the greatest impact on the theory and practice of software engineering in the ten years since its publication,
- team member (with PI Julian Goldman (Mass General Hospital, Harvard Medical School) and others from industry and academia) on “Development of a Prototype Healthcare Intranet for Improved Health Outcomes” on $9.8 million US National Institutes of Health (NIH) / National Institute of Biomedical Imaging and Bioengineering (NIBIB) – Quantum Grant. The NIH Quantum program funds projects that are viewed as “medical moonshoots” that can potentially achieve a profound (quantum) improvement in health care.
- from 2015-2019, I was the technical lead on the AAMI/UL 2800 standards committee that developed a collection of standards for safety and security of interoperable medical systems,
- over $20 million in funding through agencies and companies such as the National Science Foundation, Army Research Office, DARPA, NASA, Department of Homeland Security, Air Force Research Labs, US Army, Lockheed Martin, Collins Aerospace, IBM, Intel, Galois, Software Engineering Institute. (list of funded projects).
Current Research and Teaching Emphases
My general interests include: usable formal methods, software and system verification, software architectures, foundations of model-driven for component middleware frameworks, static and dynamic analysis of programs, security and information flow analysis, hazard analysis, assurance cases, standards development for safety-critical systems, and developing example artifacts illustrating end-to-end development of safety-critical systems.
I’m working on several projects involving developing tools and techniques for development and verification of high-assurance software systems.
-
HAMR - lead architect of HAMR (High-Assurance Modeling and Rapid engineering) - a model-driven development framework for high-assurance systems. HAMR is being used in several of US Department of Defense research projects (AFRL, US Army, DARPA). See one of my overview talks on HAMR
-
Slang and Logika - I support my colleague Professor Robby, in the use and application of Slang (a high-assurance of Scala) and Logika (a highly automated and user-friendly code contract verification tool for Slang). See Professor Robby’s overview talk on Slang
-
Course Materials for High-Assurance Model-driven Development
-
Course Materials for Software Correctness - using highly-automated deduction frameworks for program verification and testing
Current/Recent Community Activities
-
Invited tutorial on HAMR at US Air Force-sponsored Trusted Computing Center of Excellence (TCCoE) in January 2022
-
Co-organizer of 5-day conference (Dagstuhl Seminar) on “Integrated Rigorous Analysis in Cyber-Physical Systems Engineering” (Warden, Germany)