Overview

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.

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).

SAnToS Researchers collaborate extensively with researchers from the ESQuaReD Lab at University of Nebraska, Lincoln.

Current Research Emphases

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.

• 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 co-chair (with Frank Tip from IBM T.J. Watson) of the ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation (PEPM '06) Charleston, South Carolina, January 9-10, 2006.
• I'm co-chair (with Oleg Sokolsky and Insup Lee from U Penn) of the RTAS Workshop on Innovative Techniques for Certification of Embedded Systems (ITCES '06)San Jose, California, April 4, 2006.
• I'm co-chair (with Bernhard Steffen, University of Dortmund) of the International Summer School on Tool for Rigorous Engineering of Software Systems (STRESS), Dortmund, Germany, May 18-24, 2006. The theme of this incarnation of the summer school is model-driven development.

I'm currently serving on the following program committees (click here for past program committee and other service efforts within the international research community).

• 2007 ACM Symposium on Principles of Programming Languages (POPL 2007)
• 2007 Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2007) -- part of the ETAPS 2007 Joint Conference, Braga, Portugal
• National Workshop on High Confidence Software Platforms for Cyber Physical Systems (November 30-December 1, 2006)
• 2006 TAIC PART -- Testing: Academia and Industrial Conference - Practice and Research Techniques. Cumberland Lodge, Windsor, UK, 29th-31st August, 2006
• 2005 Conference on Computer-Aided Verification (CAV'05), July 7-10, Edinburgh, Scotland.
• 2005 Workshop on High Confidence Medical Device Software and Systems (HCMDSS), June 2-3, Philadelphia, PA.
• 2005 International Workshop on Leveraging Applications of Formal Methods (ISoLA 2005), Sept. 24-25, Columbia, Maryland, USA.
• 2005 Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2005) -- part of the ETAPS 2005 Joint Conference, April 4-8 in Edinburgh, Scotland.
• 2005 International Workshop on Formal Techniques for Java-like Programs (FTfJP'2005). July 26, 2005. Glasgow, Scotland.
• Model Driven and Real-Time Embedded Systems track at 11th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2005), San Francisco, March 7-10, 2005.

Invited Talks

• 2006 TAIC PART -- Testing: Academia and Industrial Conference - Practice and Research Techniques. Cumberland Lodge, Windsor, UK, 29th-31st August, 2006. Talk topic: Model-checking concurrent software systems with Bogor.
• Sixth IEEE International Workshop on Source Code Analysis and Manipulation, Philadelphia, PA, USA, 27th-29th September 2006. Talk topic: Slicing concurrent Java programs with Indus.

Click here for previous invited talks and tutorials.