Assume(), Capture(), Verify(), Establish(): A Vocabulary for Static Program Analysis

Hessamaldin Mohammadi, Wided Ghardallou, Elijah Brick, Ali Mili

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationProceedings - 2023 IEEE 23rd International Conference on Software Quality, Reliability, and Security Companion, QRS-C 2023
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages845-846
Number of pages2
ISBN (Electronic)9798350359398
DOIs
StatePublished - 2023
Event23rd IEEE International Conference on Software Quality, Reliability, and Security Companion, QRS-C 2023 - Chiang Mai, Thailand
Duration: Oct 22 2023Oct 26 2023

Publication series

NameProceedings - 2023 IEEE 23rd International Conference on Software Quality, Reliability, and Security Companion, QRS-C 2023

Conference

Conference23rd IEEE International Conference on Software Quality, Reliability, and Security Companion, QRS-C 2023
Country/TerritoryThailand
CityChiang Mai
Period10/22/2310/26/23

All Science Journal Classification (ASJC) codes

  • Computer Vision and Pattern Recognition
  • Software
  • Safety, Risk, Reliability and Quality

Keywords

  • Assume()
  • Capture()
  • Establish()
  • invariant relations
  • Mathematica (©Wolfran Research)
  • Symbolic execution
  • Verify()
  • while loops

Fingerprint

Dive into the research topics of 'Assume(), Capture(), Verify(), Establish(): A Vocabulary for Static Program Analysis'. Together they form a unique fingerprint.

Cite this