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

Despite several decades of research and development, the dependable verification / certification of software products 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.