Assume, Capture, Verify, Establish: Ingredients for Scalable Software Analysis

Hessamaldin Mohammadi, Wided Ghardallou, Ali Mili

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

2 Scopus citations

Abstract

Despite several decades of research and development, the dependable verification / certification of software prod-ucts remains an elusive goal, and software is routinely delivered with known failures but undiagnosed faults. Several obstacles come to mind to explain this gap: the absence of validated specifications against which the program must be verified; the difficulty to capture the semantics of programs, most notably iterative constructs; the size and complexity of verification tasks; the depth / level of expertise that is required to operate verification tools. In this paper, we present the specification of an interactive environment that enables the software engineer (or the software engineering student) to verify the correctness of a program by juggling / negociating what the engineer wishes the program does with what the program actually does, as written. The use-case scenario we envision is that a programmer (or engineer or student) may start a session with an incomplete or an invalid specification and an incorrect program, and conclude with a validated specification and a verified program.

Original languageEnglish (US)
Title of host publicationProceedings - 2021 21st International Conference on Software Quality, Reliability and Security Companion, QRS-C 2021
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages415-424
Number of pages10
ISBN (Electronic)9781665478366
DOIs
StatePublished - 2021
Event21st International Conference on Software Quality, Reliability and Security Companion, QRS-C 2021 - Virtual, Hainan, China
Duration: Dec 6 2021Dec 10 2021

Publication series

NameProceedings - 2021 21st International Conference on Software Quality, Reliability and Security Companion, QRS-C 2021

Conference

Conference21st International Conference on Software Quality, Reliability and Security Companion, QRS-C 2021
Country/TerritoryChina
CityVirtual, Hainan
Period12/6/2112/10/21

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Software
  • Safety, Risk, Reliability and Quality

Keywords

  • Assume()
  • Capture()
  • Establish()
  • Invariant Relations
  • Loop Invariants
  • Program Functions
  • Specifications
  • Verify()

Fingerprint

Dive into the research topics of 'Assume, Capture, Verify, Establish: Ingredients for Scalable Software Analysis'. Together they form a unique fingerprint.

Cite this