Towards denotational semantics for verilog in PVS

Han Zhu; Huibiao Zhu; Si Liu; Jian Guo

doi:10.1109/SSIRI-C.2011.10

Towards denotational semantics for verilog in PVS

Han Zhu^*, Huibiao Zhu^*, Si Liu, Jian Guo

^*Corresponding author for this work

Software Engineering Institute

East China Normal University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Scopus citations

Abstract

Verilog is a hardware description language that has been widely used in industry. We have explored its denotational semantics, operational semantics and algebraic semantics. In order to support the mechanical proof for the properties of Verilog programs, this paper studies the mechanical approach to the denotational semantics. We apply PVS in this exploration. Based on this achievement, algebraic laws for Verilog programs can be verified in the PVS framework.

Original language	English
Title of host publication	2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011
Pages	1-2
Number of pages	2
DOIs	https://doi.org/10.1109/SSIRI-C.2011.10
State	Published - 2011
Event	2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011 - Jeju Island, Korea, Republic of Duration: 27 Jun 2011 → 29 Jun 2011

Publication series

Name	2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011

Conference

Conference	2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011
Country/Territory	Korea, Republic of
City	Jeju Island
Period	27/06/11 → 29/06/11

Access to Document

10.1109/SSIRI-C.2011.10

Cite this

Zhu, H., Zhu, H., Liu, S., & Guo, J. (2011). Towards denotational semantics for verilog in PVS. In 2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011 (pp. 1-2). Article 6004491 (2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011). https://doi.org/10.1109/SSIRI-C.2011.10

@inproceedings{40ca068b78114adbae74f78153d1df4c,

title = "Towards denotational semantics for verilog in PVS",

abstract = "Verilog is a hardware description language that has been widely used in industry. We have explored its denotational semantics, operational semantics and algebraic semantics. In order to support the mechanical proof for the properties of Verilog programs, this paper studies the mechanical approach to the denotational semantics. We apply PVS in this exploration. Based on this achievement, algebraic laws for Verilog programs can be verified in the PVS framework.",

author = "Han Zhu and Huibiao Zhu and Si Liu and Jian Guo",

year = "2011",

doi = "10.1109/SSIRI-C.2011.10",

language = "英语",

isbn = "9780769544540",

series = "2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011",

pages = "1--2",

booktitle = "2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011",

note = "2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011 ; Conference date: 27-06-2011 Through 29-06-2011",

}

Zhu, H, Zhu, H, Liu, S & Guo, J 2011, Towards denotational semantics for verilog in PVS. in 2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011., 6004491, 2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011, pp. 1-2, 2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011, Jeju Island, Korea, Republic of, 27/06/11. https://doi.org/10.1109/SSIRI-C.2011.10

Towards denotational semantics for verilog in PVS. / Zhu, Han; Zhu, Huibiao; Liu, Si et al.
2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011. 2011. p. 1-2 6004491 (2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Towards denotational semantics for verilog in PVS

AU - Zhu, Han

AU - Zhu, Huibiao

AU - Liu, Si

AU - Guo, Jian

PY - 2011

Y1 - 2011

N2 - Verilog is a hardware description language that has been widely used in industry. We have explored its denotational semantics, operational semantics and algebraic semantics. In order to support the mechanical proof for the properties of Verilog programs, this paper studies the mechanical approach to the denotational semantics. We apply PVS in this exploration. Based on this achievement, algebraic laws for Verilog programs can be verified in the PVS framework.

AB - Verilog is a hardware description language that has been widely used in industry. We have explored its denotational semantics, operational semantics and algebraic semantics. In order to support the mechanical proof for the properties of Verilog programs, this paper studies the mechanical approach to the denotational semantics. We apply PVS in this exploration. Based on this achievement, algebraic laws for Verilog programs can be verified in the PVS framework.

UR - https://www.scopus.com/pages/publications/80053006355

U2 - 10.1109/SSIRI-C.2011.10

DO - 10.1109/SSIRI-C.2011.10

M3 - 会议稿件

AN - SCOPUS:80053006355

SN - 9780769544540

T3 - 2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011

SP - 1

EP - 2

BT - 2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011

T2 - 2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011

Y2 - 27 June 2011 through 29 June 2011

ER -

Zhu H, Zhu H, Liu S, Guo J. Towards denotational semantics for verilog in PVS. In 2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011. 2011. p. 1-2. 6004491. (2011 5th International Conference on Secure Software Integration and Reliability Improvement - Companion, SSIRI-C 2011). doi: 10.1109/SSIRI-C.2011.10

Towards denotational semantics for verilog in PVS

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this