Challenges in Decomposing Encodings of Verification Problems

Modern program verifiers use logic-based encodings of the verification problem that are discharged by a back end reasoning engine. However, instances of such encodings for large programs can quickly overwhelm these back end solvers. Hence, we need techniques to make the solving process scale to la...

Full description

Bibliographic Details
Main Author: Peter Schrammel
Format: Article
Language:English
Published: Open Publishing Association 2016-07-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1607.04458v1