|
Abstract:
The talk will explain how concurrency arises quite naturally in logic programming. In logic programming, concurrency is often often controlled with delay declarations that specify that a sub-goal is to suspend until some condition on its arguments is satisfied. Reasoning about delay declarations is notoriously tricky and it is not usual for a program and goal to accidentally reduce to a state that contains a sub-goal that suspends indefinitely.
The talk will present a tool, based on abstract interpretation, that can infer a class of goals that do not lead to suspension. This approach leads to a lightweight point-and-click form of program verification in which, after directing the analyser at a file, the user merely has to inspect the results inferred by the analysis. If
the results are not as expected, then the program is possibly buggy,and therefore warrants close scrutiny. The talk will explain how the tool can be used to locate several bugs in number of existing
programs.
|