Model based analyses of definite logic programs are discussed in detail. A model of a program captures its properties. Analyzing different models one obtains a flexible approach for verification and optimization of logic-based systems. A uniform implementation of the core algorithms, which exploits deductive database technology, is investigated. In particular, novel algorithms for generating large models and for extracting properties from models are presented.