Integration and Analysis of Alternative SMT Solvers for Software Verification
Frederik Rothenberger · Repository for Publications and Research Data (ETH Zurich) · 2016
SMT solvers are commonly used in software verication.Software verication often requires undecidable theories, which are only unreliably solved by SMT solvers.In this thesis, two SMT solvers are compared in order to decide whether the reliability of software veriers can be increased by opportunistically switching the underlying solver.The evaluation shows that, for the particular comparison made, this is not the case.Therefore another approach to alleviate the reliability problems is pursued: Improvement of tools to understand the problematic behaviour of SMT solvers.In particular, an existing tool to analyse the proving behaviour of the SMT solver, Z3, is improved and extended.The focus of the extension is on features designed to explain a class of problems which cause innite runtimes, called matching loops.