Flexible Static Semantic Checking using First-Order Logic
Shimon Rura
Barbara Staudt Lerner
Computer Science Department
Williams College
Abstract
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.