GLOBAN 2006 - The Global Computing Approach to Analysis of Systems

International Summer School at DTU, August 21-25, 2006

Computing with relations using Horn clauses

Lectures by Helmut Seidl, Technical University of Munich, Germany


Many program analysis problems ranging from simple control-flow analysis to certification of cryptographic protocols, can be conveniently described by means Horn clauses where the clauses for different kinds of problems often have specific properties. Performing the analysis then amounts to computing or approximating least models or, to (approximatively) answering queries w.r.t. to the given clause set. The tutorial provides advanced technology which allows to construct efficient solvers for various practically relevant classes of Horn clauses.

Contact: globan@imm.dtu.dk