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, and Rockwell-Collins.
SAnToS Researchers were 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. In May 2005, SAnToS' Cadena environment was used by Boeing engineers to develop the avionics software flown on the Scan Eagle Unmanned Air Vehicle (UAV) platform for the DARPA PCES capstone demo at White Sands Missile Range.
In 2010, SAnToS Researchers 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.
SAnToS Laboratory has been funded through agencies and companies such as the National Science Foundation, Army Research Office, DARPA, NASA, Lockheed Martin, Rockwell Collins, IBM, and Intel (list of funded projects).
Current Research Emphases My general interests include:software model checking, software architectures, foundations of model-driven for component middleware frameworks, static and dynamic analysis of programs, program slicing, partial evaluation and program specialization, and program logics.
I'm working on several other projects involving developing tools and techniques for Java program analysis/verification, model driven development of distributed systems, and applying these techniques to construct high-assurance software systems.
- Medical Device Coordination Framework -- an open-source platform for integrating medical devices and coordinating their actions to support "system of systems" engineering in care-giving contexts.
- Bogor --- a customizable/extensible model-checker for object-oriented software emphasizing the notion of domain-specific model-checking
- Cadena --- a robust tool environment for modeling, analysis, and model-driven development of large-scale distributed systems built using component middleware frameworks such as the CORBA Component Model (CCM) or Enterprise Java Beans (EJB)
- Bandera --- a tool suite for detecting hard-to-find defects in concurrent Java software using model-checking techniques
- Indus --- a featureful program slicer and static analysis framework for Java
All of the tools above are implemented in IBM's Eclipse platform, and they've been used by a number of different academic and industrial research groups.
Current Service Projects I'm involved (currently or recently) in organizing the following meetings/events:
- I'm co-organizer of a Dagstuhl Seminar on Software Certification: Methods and Tools -- January 27 to February 1, 2013, Dagstuhl Seminar 13051, Warden, Germany.
- I'm the program committee co-chair (with Ruth Breu, University of Innsbruck, Austria) of the 2012 Workshop on Software Engineering in Health Care (co-located with ICSE 2012) Zurich, Switzerland, June 4-5, 2012.
My current and recent service activities are listed below (click here for past program committee and other service efforts within the international research community).
- UL / AAMI 2800 standards committee on Interoperable Medical Device Interface Safety.
- NASA Formal Methods 2012
- Verified Software: Theories, Tools, Experiments (VSTTE) 2012
- 2011 IFIP Conferences on Formal Methods for Open Object-based Distributed Systems (FMOODS) and International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) Reykjavik, Iceland, June 6-9, 2011.
- High Confidence Medical Device Systems and Software (HCMDSS 2011), Chicago, Illinois, April 11, 2011.
- International Conference on Software Engineering (ICSE 2011), Waikiki, Hawaii
- Workshop on Software Engineering in Health Care (SEHC 2011),Waikiki, Hawaii, May 2011
- NASA Formal Methods 2011
- Workshop on Software Engineering in Health Care (SEHC 2010), Cape Town, South Africa, May 2010
- Verified Software: Theories, Tools, Experiments (VSTTE) 2010
- International Conference on Run-time Verification (RV 2010), Malta
- Program committee co-chair (with Elena Zucca, University of Genoa, Italy) of the 2010 IFIP Conferences on Formal Methods for Open Object-based Distributed Systems (FMOODS) and International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) Amsterdam, The Netherlands, June 7-9, 2010.
Invited Talks Upcoming and recent invited talks:
- Tenth International Conference on Formal Engineering Methods (ICFEM 2008) -- keynote talk, Kitakyushu, Japan, October 27-31, 2008. (slides)
Click here for previous invited talks and tutorials.