Abstract. INCA is a tool for analysis of concurrent systems. The system to be analyzed is modeled in the S-Expression Design Language (SEDL), and the properties of the system to be verified are written in the INCA Query Language. INCA takes these two items as input, and produces Integer Linear Programming problems, which can be analyzed by standard linear programming tools, such as CPLEX. In this document, we give a precise description of the syntax and semantics of the INCA Query Language, as well as several examples of INCA queries.This paper appeared as Technical Report CMPSCI TR 02-18, Department of Computer Science, University of Massachusetts, May 2002.
You may download the paper in one of the following formats: