The aim of program verification is to prove the correctness of a program S with respect to a formal specification, that consists of a pre- and a postcondition V and N. In other words: are program S and specification (V, N) consistent? -- V S -- N Program S is correct, if S starts in a state that fulfills V and terminates in state that fulfills N. The form al definition of correctness is S is correct wrt. (V, N) if [V => wp(S, N)]. wp(S, N) is the wea kest precondition, that guarantees termination in a state fulfilling N. For the purpose of program verification the axiomatic or relational semantics is necessary. These two kinds of formal semantics are equivalent. Axiomatic semantics uses the wp-function, that works on the complete lattice of predicates. Relational semantics uses the LP (largest preset)-function, that works on the complete lattice of state sets. These two lattices are isomorph thru the characteristic predicate function of a set. In order to work efficiently with the wp-function some properties of that function are necessary and useful. Two new properties are shown: strong disjunctivity for comparable predicates and the substitution lemma for wp. Furthermore it turns out, t hat all properties of the wp-function are easily provable in the lattice of state sets with elementary set theory. A VC is defined to be a condition that implies correctness, formally [VC => [V => wp(S, N)]. A distinction is made between exact and ap proximate VCs. The major results of the thesis are verifying loops without an invariant and falsification conditions. In order to verify loops without a given invariant, two strategies are possible: 1. generate the invariant or 2. compute the wp-function for the loop Strategy 1 is used to compute invariants for for-loops. The invariant is generated by substituting a constant in the postcondition by a variable, more exactly the upper limit of the loop is substituted by the loop variable. In gener al the upper limit is not a variable. Therefore the loop is transformed into a semantically equivalent loop. Strategy 2 is used to compute the wp of while-loops by a new method that uses E-unification. Falsification conditions (FCs) are very useful i n practical program verification. They explicitly prove the incorrectness of a program and facilitate a localization of program errors. FCs are defined in an analog way as VCs: an FC implies the incorrectness of a program, formally [FC => not [V => w p(S, N)]. FCs are reduced to constraint programming problems (cpp) or, in the case of integer types, to integer programming problems (ipp). ipp also arise in data dependence analysis. Therefore similar methods can be applied.