Master Thesis MSTR-2016-62

BibliographyNiethammer, Philipp: Syntax-directed Incremental Verification of Java Modeling Language Contracts.
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology, Master Thesis No. 62 (2016).
55 pages, english.
Abstract

Java has evolved to the most popular programming language and is more and more used in reliability critical systems, increasing the demand for automatic software verification tools. But automatic verification of software is a complex and slow process so that it often is conceived as bothersome intrusion into the programming workflow. There are several projects that integrate software verification into the development environment and display results in a comprehensible way, but little work has be done to increase the performance of the verification process during active development. In this thesis, the SiDECAR approach for incremental verification procedures is applied to the verification of Java Modeling Language constraints to reduce the computation and evaluation of correctness to the minimal context of a change. A tool is implemented that translates JML annotated Java7 code into verification conditions that are then checked by an SMT solver, updates outdated verification conditions after an incoming change and uses several techniques to minimize the need of computation by the SMT solver to establish a check result accordingly and benchmarks are executed to validated the approach. By reducing the needed verification time to a minimum, the developer can be presented live updates on the program correctness, ultimately reducing the costs of software verification and improve its acceptance.

Department(s)University of Stuttgart, Institute of Software Technology, Software Reliability and Security
Superviser(s)Filieri, Dr. Antonio
Entry dateJune 5, 2019
   Publ. Computer Science