Three-Valued Bounded Model Checking with Cause-Guided Abstraction Refinement: PROOFS

Loading...
Thumbnail Image

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Department of Computer Science: University of Pretoria

Abstract

In this Technical Report we provide the proof to Theorem 1 which appears in our forthcoming article "Three-Valued Bounded Model Checking with Cause-Guided Abstraction Refinement", to appear in the journal: Science of Computer Programming. Due to shortage of page-space the proof cannot be printed in the journal article itself. In the forthcoming journal article, wherein Theorem 1 will appear, a literature reference will point the readers to this Technical Report for the proof.

Description

Keywords

Model Checking, Bounded Model Checking, Theorem, Proof

Sustainable Development Goals

Citation

Nils Timm and Stefan Gruner, Three-Valued Bounded Model Checking with Cause-Guided Abstraction Refinement: PROOFS. Technical Report TR-SSFM-01-08-2018, Research Group for System Specifications and Formal Methods, Department of Computer Science, University of Pretoria, 2018.