Type system, rooted in a programming language, helps prevent programmers from introducing bugs while building systems. Model checking technique, external to building process, helps detect bugs in already constructed systems. How to combine these two techniques to facilitate the construction of verifiably correct software systems in a cost-effective manner is the central challenge that I want to address in my research.
ATS is a statically typed programming language equipped with highly expressive type system. In particular, both dependent types and linear types are available in ATS. We introduce into ATS various primitives for modeling concurrent systems with verification. Such primitives are easier and safer to use due to their well-designed interfaces (types) and provide an intuitive way to specify safety properties along side with models. We are creating two modeling languages. One has semantics strongly coupled with Promela and in turn is called ATS/PML. The other has its own semantics and is named ATS/Veri to indicate its support for system verification.