Startseite › Forschung › Projekte › Analysis and Verification of Annotated Logic Programs
Analysis and Verification of Annotated Logic Programs
The concept of enriching programs with annotations for analysis and verification is applied to logic programs. Thus complex conditions like consistency constraints or correctness issues can be checked and many programming errors can be detected before execution time of a program. Different classes of annotations can be distinguished, e.g. type annotations, domain-specific annotations like arithmetic constraints, or annotations containing formulas in predicate logic. In order to promote the approach and to be able to exploit the runtime efficiency of commercial systems, the annotations will be applied to standard Prolog. The system Typical provides type-checking facilities for Prolog.
Funding
- Deutsche Forschungsgemeinschaft, Schwerpunktprogramm "Deduktion".