@inproceedings{0809a9cc147e4a2e830238162cf2b948,
title = "Assume, Capture, Verify, Establish: Ingredients for Scalable Software Analysis",
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.",
keywords = "Assume(), Capture(), Establish(), Invariant Relations, Loop Invariants, Program Functions, Specifications, Verify()",
author = "Hessamaldin Mohammadi and Wided Ghardallou and Ali Mili",
note = "Publisher Copyright: {\textcopyright} 2021 IEEE.; 21st International Conference on Software Quality, Reliability and Security Companion, QRS-C 2021 ; Conference date: 06-12-2021 Through 10-12-2021",
year = "2021",
doi = "10.1109/QRS-C55045.2021.00068",
language = "English (US)",
series = "Proceedings - 2021 21st International Conference on Software Quality, Reliability and Security Companion, QRS-C 2021",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "415--424",
booktitle = "Proceedings - 2021 21st International Conference on Software Quality, Reliability and Security Companion, QRS-C 2021",
address = "United States",
}