Predicate transformers for local description units

Predicate transformers are symbolic functions used for computing transitions of system models with states represented by means of logic formulas. They are widely used for symbolic evaluation of programs, verification, abstract interpretation, and symbolic modeling of software. The models of software systems considered in this paper are represented by means of systems of local description units and their states are represented by means of first order logic formulas. Our goal is to develop an algorithm for computing the strongest predicate transformer for local description units considered as operators over formulas.