@inproceedings{990d769cd3c443f9a16b699ff349f2a5,
title = "Assume(), Capture(), Verify(), Establish(): A Vocabulary for Static Program Analysis",
abstract = "We propose a set of functions that a user can invoke to analyze a program written in a C-like language: Assume() refers to a label in the source code or to a program part, and enables the user to make an assumption about the state of the program at some label or the function of some program part; Capture() refers to a label or a program part and returns an assertion about the state of the program at the label or the function of the program part; Verify() refers to a label or a program part and tests a unary assertion about the state of the program at the label or a binary assertion about the function of the program part; Establish() refers to a label or a program part and modifies the program code to make Verify() return TRUE at that label or program part, if it did not originally. We discuss the foundations of this tool as well as a preliminary implementation.",
keywords = "Assume(), Capture(), Establish(), invariant relations, Mathematica ({\textcopyright}Wolfran Research), Symbolic execution, Verify(), while loops",
author = "Hessamaldin Mohammadi and Wided Ghardallou and Elijah Brick and Ali Mili",
note = "Publisher Copyright: {\textcopyright} 2023 IEEE.; 23rd IEEE International Conference on Software Quality, Reliability, and Security Companion, QRS-C 2023 ; Conference date: 22-10-2023 Through 26-10-2023",
year = "2023",
doi = "10.1109/QRS-C60940.2023.00067",
language = "English (US)",
series = "Proceedings - 2023 IEEE 23rd International Conference on Software Quality, Reliability, and Security Companion, QRS-C 2023",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "845--846",
booktitle = "Proceedings - 2023 IEEE 23rd International Conference on Software Quality, Reliability, and Security Companion, QRS-C 2023",
address = "United States",
}