Combine Type Checking and Model Checking for System Verification

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.
  • For a detailed description of ATS/Veri and its usage in constructing and verifying concurrent programs, please refer to the documentation here.
  • The website for ATS/PML is heavily under construction and will be online before September 2016.