A practical approach to partial functions in CVC lite

Sergey Berezin, Clark Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, David L. Dill

Research output: Contribution to journalArticle

Abstract

Most verification approaches assume a mathematical formalism in which functions are total, even though partial functions occur naturally in many applications. Furthermore, although there have been various proposals for logics of partial functions, there is no consensus on which is "the right" logic to use for verification applications. In this paper, we propose using a three-valued Kleene logic, where partial functions return the "undefined" value when applied outside of their domains. The particular semantics are chosen according to the principle of least surprise to the user; if there is disagreement among the various approaches on what the value of the formula should be, its evaluation is undefined. We show that the problem of checking validity in the three-valued logic can be reduced to checking validity in a standard two-valued logic, and describe how this approach has been successfully implemented in our tool, CVC Lite.

Original languageEnglish (US)
Pages (from-to)13-23
Number of pages11
JournalElectronic Notes in Theoretical Computer Science
Volume125
Issue number3
DOIs
StatePublished - Jul 18 2005

Fingerprint

Logic
Partial
Semantics
Evaluation

Keywords

  • CVC
  • Kleene
  • Partial functions
  • Three-valued logic

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

Berezin, S., Barrett, C., Shikanian, I., Chechik, M., Gurfinkel, A., & Dill, D. L. (2005). A practical approach to partial functions in CVC lite. Electronic Notes in Theoretical Computer Science, 125(3), 13-23. https://doi.org/10.1016/j.entcs.2004.06.064

A practical approach to partial functions in CVC lite. / Berezin, Sergey; Barrett, Clark; Shikanian, Igor; Chechik, Marsha; Gurfinkel, Arie; Dill, David L.

In: Electronic Notes in Theoretical Computer Science, Vol. 125, No. 3, 18.07.2005, p. 13-23.

Research output: Contribution to journalArticle

Berezin, S, Barrett, C, Shikanian, I, Chechik, M, Gurfinkel, A & Dill, DL 2005, 'A practical approach to partial functions in CVC lite', Electronic Notes in Theoretical Computer Science, vol. 125, no. 3, pp. 13-23. https://doi.org/10.1016/j.entcs.2004.06.064
Berezin S, Barrett C, Shikanian I, Chechik M, Gurfinkel A, Dill DL. A practical approach to partial functions in CVC lite. Electronic Notes in Theoretical Computer Science. 2005 Jul 18;125(3):13-23. https://doi.org/10.1016/j.entcs.2004.06.064
Berezin, Sergey ; Barrett, Clark ; Shikanian, Igor ; Chechik, Marsha ; Gurfinkel, Arie ; Dill, David L. / A practical approach to partial functions in CVC lite. In: Electronic Notes in Theoretical Computer Science. 2005 ; Vol. 125, No. 3. pp. 13-23.
@article{a0b1cc26be8640ab9973138de35b4234,
title = "A practical approach to partial functions in CVC lite",
abstract = "Most verification approaches assume a mathematical formalism in which functions are total, even though partial functions occur naturally in many applications. Furthermore, although there have been various proposals for logics of partial functions, there is no consensus on which is {"}the right{"} logic to use for verification applications. In this paper, we propose using a three-valued Kleene logic, where partial functions return the {"}undefined{"} value when applied outside of their domains. The particular semantics are chosen according to the principle of least surprise to the user; if there is disagreement among the various approaches on what the value of the formula should be, its evaluation is undefined. We show that the problem of checking validity in the three-valued logic can be reduced to checking validity in a standard two-valued logic, and describe how this approach has been successfully implemented in our tool, CVC Lite.",
keywords = "CVC, Kleene, Partial functions, Three-valued logic",
author = "Sergey Berezin and Clark Barrett and Igor Shikanian and Marsha Chechik and Arie Gurfinkel and Dill, {David L.}",
year = "2005",
month = "7",
day = "18",
doi = "10.1016/j.entcs.2004.06.064",
language = "English (US)",
volume = "125",
pages = "13--23",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "3",

}

TY - JOUR

T1 - A practical approach to partial functions in CVC lite

AU - Berezin, Sergey

AU - Barrett, Clark

AU - Shikanian, Igor

AU - Chechik, Marsha

AU - Gurfinkel, Arie

AU - Dill, David L.

PY - 2005/7/18

Y1 - 2005/7/18

N2 - Most verification approaches assume a mathematical formalism in which functions are total, even though partial functions occur naturally in many applications. Furthermore, although there have been various proposals for logics of partial functions, there is no consensus on which is "the right" logic to use for verification applications. In this paper, we propose using a three-valued Kleene logic, where partial functions return the "undefined" value when applied outside of their domains. The particular semantics are chosen according to the principle of least surprise to the user; if there is disagreement among the various approaches on what the value of the formula should be, its evaluation is undefined. We show that the problem of checking validity in the three-valued logic can be reduced to checking validity in a standard two-valued logic, and describe how this approach has been successfully implemented in our tool, CVC Lite.

AB - Most verification approaches assume a mathematical formalism in which functions are total, even though partial functions occur naturally in many applications. Furthermore, although there have been various proposals for logics of partial functions, there is no consensus on which is "the right" logic to use for verification applications. In this paper, we propose using a three-valued Kleene logic, where partial functions return the "undefined" value when applied outside of their domains. The particular semantics are chosen according to the principle of least surprise to the user; if there is disagreement among the various approaches on what the value of the formula should be, its evaluation is undefined. We show that the problem of checking validity in the three-valued logic can be reduced to checking validity in a standard two-valued logic, and describe how this approach has been successfully implemented in our tool, CVC Lite.

KW - CVC

KW - Kleene

KW - Partial functions

KW - Three-valued logic

UR - http://www.scopus.com/inward/record.url?scp=21644465814&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=21644465814&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2004.06.064

DO - 10.1016/j.entcs.2004.06.064

M3 - Article

VL - 125

SP - 13

EP - 23

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 3

ER -