Software is widely used and hard to make reliable. Researchers have been exploring new ways to ensure software reliability including software verification, i.e., mathematical reasoning about software. The current technology for software verification is not sufficiently efficient to be used for industrial software. In the thesis, we present novel constraint based verification methods and algorithms for constraint solving that increase the efficiency of software verification. In the direction of constraint based verification methods, we first present an algorithm that improves the efficiency of an important verification method, namely template based invariant generation. Then, we extend this method to compute bounds on consumption of a resource by a program. In the direction of algorithms for constraint solving, we present a simplex based proof production algorithm that is compatible with CLP(Q) and an algorithm for solving recursion-free Horn clauses over LI+UIF.     «

Software is widely used and hard to make reliable. Researchers have been exploring new ways to ensure software reliability including software verification, i.e., mathematical reasoning about software. The current technology for software verification is not sufficiently efficient to be used for industrial software. In the thesis, we present novel constraint based verification methods and algorithms for constraint solving that increase the efficiency of software verification. In the direction of...     »

Zuverlässigkeit von Software lässt sich nur sehr schwer erreichen, weswegen schon lange nach Möglichkeiten gesucht wird, die Zuverlässigkeit von Software zu überprüfen bzw. zu verifizieren. Die gegenwärtig zur Verfügung stehenden Techniken sind jedoch nicht effizient genug für den industriellen Einsatz. In der Arbeit werden neuartige Constraint basierte Verifikationsmethoden und Lösungsverfahren für Constraint-Probleme vorgestellt, welche eine effizientere Verifikation von Programmen erlauben. Im Bereich der Verifikationsverfahren wird zunächst ein effizienterer Algorithmus für die Invariantengenerierung basierend auf Templates vorgestellt. Darauf aufbauend wird die Berechnung von Schranken für den Ressourcenverbrauch eines Programms betrachtet. Im Bereich der Lösungsverfahren werden ein auf dem Simplex-Algorithmus basierender, zu CLP(Q) kompatibler Algorithmus zur Gewinnung von Beweisen und ein Algorithmus zum Lösen von rekursionsfreien Hornklauseln über LI+UIF vorgestellt.      «

Zuverlässigkeit von Software lässt sich nur sehr schwer erreichen, weswegen schon lange nach Möglichkeiten gesucht wird, die Zuverlässigkeit von Software zu überprüfen bzw. zu verifizieren. Die gegenwärtig zur Verfügung stehenden Techniken sind jedoch nicht effizient genug für den industriellen Einsatz. In der Arbeit werden neuartige Constraint basierte Verifikationsmethoden und Lösungsverfahren für Constraint-Probleme vorgestellt, welche eine effizientere Verifikation von Programmen erlauben....     »