A Simplified Method for Automatic Verification of Java Programs

Zhi Li; Ling Xie; Yilong Yang

doi:10.18293/SEKE2022-180

A Simplified Method for Automatic Verification of Java Programs

Zhi Li
, Ling Xie
, Yilong Yang^*

^*Corresponding author for this work

School of Software

Guangxi Normal University

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

Abstract

Current KeY verification tool for Java programs provides limited capability for verifying Java programs. In order to solve this problem, we provide a method for simplifying complex Java programs into a format that is compatible with the KeY. A set of simplification rules based on abstract syntax tree (AST) are proposed. These rules can keep the logic and semantics of the original Java programs mostly unchanged, while meeting the requirements of KeY verification tool. The paper concludes with a bank ATM example to demonstrate the feasibility of our work.

Original language	English
Title of host publication	SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering
Publisher	Knowledge Systems Institute Graduate School
Pages	471-472
Number of pages	2
ISBN (Electronic)	1891706543, 9781891706547
DOIs	https://doi.org/10.18293/SEKE2022-180
State	Published - 2022
Event	34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022 - Pittsburgh, United States Duration: 1 Jul 2022 → 10 Jul 2022

Publication series

Name	Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
ISSN (Print)	2325-9000
ISSN (Electronic)	2325-9086

Conference

Conference	34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022
Country/Territory	United States
City	Pittsburgh
Period	1/07/22 → 10/07/22

Keywords

Java program simplification
KeY verification tool
Program verification
abstract syntax tree (AST)

Access to Document

10.18293/SEKE2022-180

Cite this

Li, Z., Xie, L., & Yang, Y. (2022). A Simplified Method for Automatic Verification of Java Programs. In SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering (pp. 471-472). (Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE). Knowledge Systems Institute Graduate School. https://doi.org/10.18293/SEKE2022-180

Li, Zhi ; Xie, Ling ; Yang, Yilong. / A Simplified Method for Automatic Verification of Java Programs. SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering. Knowledge Systems Institute Graduate School, 2022. pp. 471-472 (Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE).

@inproceedings{ddc81f923f2b4c39a38850a3bf488b48,

title = "A Simplified Method for Automatic Verification of Java Programs",

abstract = "Current KeY verification tool for Java programs provides limited capability for verifying Java programs. In order to solve this problem, we provide a method for simplifying complex Java programs into a format that is compatible with the KeY. A set of simplification rules based on abstract syntax tree (AST) are proposed. These rules can keep the logic and semantics of the original Java programs mostly unchanged, while meeting the requirements of KeY verification tool. The paper concludes with a bank ATM example to demonstrate the feasibility of our work.",

keywords = "Java program simplification, KeY verification tool, Program verification, abstract syntax tree (AST)",

author = "Zhi Li and Ling Xie and Yilong Yang",

note = "Publisher Copyright: {\textcopyright} 2022 Knowledge Systems Institute Graduate School. All rights reserved.; 34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022 ; Conference date: 01-07-2022 Through 10-07-2022",

year = "2022",

doi = "10.18293/SEKE2022-180",

language = "英语",

series = "Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE",

publisher = "Knowledge Systems Institute Graduate School",

pages = "471--472",

booktitle = "SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering",

address = "美国",

}

Li, Z, Xie, L & Yang, Y 2022, A Simplified Method for Automatic Verification of Java Programs. in SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering. Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE, Knowledge Systems Institute Graduate School, pp. 471-472, 34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022, Pittsburgh, United States, 1/07/22. https://doi.org/10.18293/SEKE2022-180

A Simplified Method for Automatic Verification of Java Programs. / Li, Zhi; Xie, Ling; Yang, Yilong.
SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering. Knowledge Systems Institute Graduate School, 2022. p. 471-472 (Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE).

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

TY - GEN

T1 - A Simplified Method for Automatic Verification of Java Programs

AU - Li, Zhi

AU - Xie, Ling

AU - Yang, Yilong

PY - 2022

Y1 - 2022

N2 - Current KeY verification tool for Java programs provides limited capability for verifying Java programs. In order to solve this problem, we provide a method for simplifying complex Java programs into a format that is compatible with the KeY. A set of simplification rules based on abstract syntax tree (AST) are proposed. These rules can keep the logic and semantics of the original Java programs mostly unchanged, while meeting the requirements of KeY verification tool. The paper concludes with a bank ATM example to demonstrate the feasibility of our work.

AB - Current KeY verification tool for Java programs provides limited capability for verifying Java programs. In order to solve this problem, we provide a method for simplifying complex Java programs into a format that is compatible with the KeY. A set of simplification rules based on abstract syntax tree (AST) are proposed. These rules can keep the logic and semantics of the original Java programs mostly unchanged, while meeting the requirements of KeY verification tool. The paper concludes with a bank ATM example to demonstrate the feasibility of our work.

KW - Java program simplification

KW - KeY verification tool

KW - Program verification

KW - abstract syntax tree (AST)

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

U2 - 10.18293/SEKE2022-180

DO - 10.18293/SEKE2022-180

M3 - 会议稿件

AN - SCOPUS:85137157860

T3 - Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE

SP - 471

EP - 472

BT - SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering

PB - Knowledge Systems Institute Graduate School

T2 - 34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022

Y2 - 1 July 2022 through 10 July 2022

ER -

Li Z, Xie L, Yang Y. A Simplified Method for Automatic Verification of Java Programs. In SEKE 2022 - Proceedings of the 34th International Conference on Software Engineering and Knowledge Engineering. Knowledge Systems Institute Graduate School. 2022. p. 471-472. (Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE). doi: 10.18293/SEKE2022-180

A Simplified Method for Automatic Verification of Java Programs

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this