GLOBAN 2006 - The Global Computing Approach to Analysis of Systems

Computing with relations using Horn clauses

Lectures by Helmut Seidl, Technical University of Munich, Germany

Abstract

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.