Flexible static semantic checking using first-order logic

Static analysis of software processes is important in assessing the correctness of processes, particularly since their long duration and distributed execution make them difficult to test. We describe a novel approach to building a static analyzer that can detect programming errors and anomalies in processes written in Little-JIL. We describe semantic rules declaratively in first-order logic and use xlinkit, a constraint checker, to check the processes. We have used this approach to develop a checker that can find simple syntactic errors as well as more complex control and data flow anomalies.