Computing Program Functions

Hessamaldin Mohammadi, Wided Ghardallou, Richard C. Linger, Ali Mili

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

Abstract

Extracting the function of a program from a static analysis of its source code is a valuable capability in software engineering, but it has proved to be an elusive goal, due primarily to the difficulty of deriving the function of iterative statements. Several automated tools obviate this difficulty by unrolling the loops; but this is clearly an imperfect solution, especially in light of the fact that loops capture most of the computing power of a program, are the locus of most of its complexity, and the source of most of its faults. In this paper we discuss the design and ongoing implementation of an automated tool for deriving the function of a program in three steps: first, the source code is mapped onto an abstract syntax tree (AST), using standard parsing technology; then each node of the AST is mapped onto an equation between pre and post states; finally, these equations are submitted to a symbolic computation engine that extracts the final program state as a function of its initial state. Loop functions are derived by pattern matching against semantic recognizers, which capture the requisite programming knowledge and domain knowledge.

Original languageEnglish (US)
Title of host publicationProceedings - IEEE/ACM 10th International Conference on Formal Methods in Software Engineering, FormaliSE 2022
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages102-112
Number of pages11
ISBN (Electronic)9781450392877
DOIs
StatePublished - 2022
Event10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE 2022 - Pittsburgh, United States
Duration: May 18 2022May 19 2022

Publication series

NameProceedings - IEEE/ACM 10th International Conference on Formal Methods in Software Engineering, FormaliSE 2022

Conference

Conference10th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE 2022
Country/TerritoryUnited States
CityPittsburgh
Period5/18/225/19/22

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality

Keywords

  • invariantrelations
  • Java
  • program functions
  • Program verification
  • symbolic execution

Fingerprint

Dive into the research topics of 'Computing Program Functions'. Together they form a unique fingerprint.

Cite this