Constraint solving for verification [Elektronische Ressource] / Ashutosh Kumar Gupta. Gutachter: Andrey Rybalchenko ; Rupak Majumdar. Betreuer: Andrey Rybalchenko

TECHNISCHE UNIVERSITAT MUNCHENLehrstuhl fur Informatik 7Constraint Solving for Veri cationAshutosh Kumar GuptaVollst andiger Abdruck der von der Fakult at fur Informatik der Technischen Universit at Munc hen zurErlangung des akademischen Grades einesDoktors der Naturwissenschaften (Dr. rer. nat.)genehmigten Dissertation.Vorsitzender: Univ.-Prof. Dr. Helmut SeidlPrufer der Dissertation: 1. Univ.-Prof. Dr. Andrey Rybalchenko2. Full Prof. Dr. Rupak Majumdar,University of California/ USADie Dissertation wurde am 30.05.2011 bei der Technischen Universit at Munc hen eingereicht und durchdie Fakult at fur Informatik am 12.07.2011 angenommen.12AbstractSoftware is widely used and hard to make reliable. Researchers have been exploring new waysto ensure software reliability including software veri cation, i.e., mathematical reasoning aboutsoftware. The current technology for software veri cation is not su ciently e cient to be usedin industrial software production. In this thesis, we present novel constraint based veri cationmethods and algorithms for constraint solving that increase the e ciency of software veri cation.In the direction of constraint based veri cation methods, we rst present an algorithm thatimproves the e ciency of an important vd, namely template based invariantgeneration [16]. Then, we extend the template based invariant generation method to computebounds on consumption of a resource by a program.