:: John Hatcliff's Homepage

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
Awas - my Ph.D. student Hariharan Thiagarajan developed Awas – an information flow analysis and visualization tool for the AADL modeling language. This builds on a history of work that our research has done on programming slicing for Java and Spark Ada.

Bandera – a software model checker for concurrent Java programs
Bogor – a software model checking framework built by Robby for his Ph.D. work
Cadena – an Eclipse-based extensible integrated modeling and development framework for component-based systems
MDCF - a medical device coordination framework that was one of the first open-source projects to illustrate the idea of a “medical application platform”