Proving Refinement Using Transduction

Bengt Jonsson; Amir Pnueli; Camilla Østerberg Rump

doi:10.1007/s004460050062

Proving Refinement Using Transduction

Bengt Jonsson
, Amir Pnueli
, Camilla Østerberg Rump

Uppsala University
Weizmann Institute of Science

Research output: Contribution to journal › Journal article › Research › peer-review

Abstract

We present a verification method, in which refinement between two systems is proven by constructing a transducer that inputs a computation of a concrete system and outputs a matching computation of the abstract system.

Original language	English
Journal	Distributed Computing
Volume	12
Issue number	2-3
Pages (from-to)	129-149
ISSN	0178-2770
DOIs	https://doi.org/10.1007/s004460050062
Publication status	Published - 1999

Access to Document

10.1007/s004460050062

OpenUrl availability

Check availability in DTU Findit

Cite this

@article{57f8ea9b081f477bade206bf070261e8,

title = "Proving Refinement Using Transduction",

abstract = "We present a verification method, in which refinement between two systems is proven by constructing a transducer that inputs a computation of a concrete system and outputs a matching computation of the abstract system.",

author = "Bengt Jonsson and Amir Pnueli and Rump, \{Camilla {\O}sterberg\}",

year = "1999",

doi = "10.1007/s004460050062",

language = "English",

volume = "12",

pages = "129--149",

journal = "Distributed Computing",

issn = "0178-2770",

publisher = "Springer Verlag",

number = "2-3",

}

TY - JOUR

T1 - Proving Refinement Using Transduction

AU - Jonsson, Bengt

AU - Pnueli, Amir

AU - Rump, Camilla Østerberg

PY - 1999

Y1 - 1999

N2 - We present a verification method, in which refinement between two systems is proven by constructing a transducer that inputs a computation of a concrete system and outputs a matching computation of the abstract system.

AB - We present a verification method, in which refinement between two systems is proven by constructing a transducer that inputs a computation of a concrete system and outputs a matching computation of the abstract system.

U2 - 10.1007/s004460050062

DO - 10.1007/s004460050062

M3 - Journal article

SN - 0178-2770

VL - 12

SP - 129

EP - 149

JO - Distributed Computing

JF - Distributed Computing

IS - 2-3

ER -

Proving Refinement Using Transduction

Abstract

Access to Document

OpenUrl availability

Fingerprint

Cite this