Patent · US Active

Transitioning legacy software to be provably correct

US11797317B1 · kind B1 · utility

1Cited by

3References

20Claims

0Family size

Assignee

AMAZON TECHNOLOGIES, INC. · US

Inventors

Sean McLaughlin · Seattle, US
Tongtong Xiang · Seattle, US
Matthias Schlaipfer · Berlin, DE
Neha Rungta · San Jose, US
Serdar Tasiran · New York, US
John Cook · Brooklyn, US
Michael William Whalen · Edina, US

Key dates

Filing date	Dec 10, 2021
Grant date	Oct 24, 2023
Priority date	—
Expiry date	Dec 10, 2041

Classification

Technology area (CPC G)Physics
CPC primaryG06F9/455
WIPO fieldComputer technology
WIPO sectorElectrical engineering

Abstract

A software development process may support a transition from unverifiable, legacy code to verifiable code that is provably correct by construction. A behavioral model may be developed for legacy software that includes various behavioral criteria. Then, source code implemented in a verifiable language may be verified using the behavioral model to perform verification. Once the source code is complete and verified, a new verified implementation may be compiled. The verified implementation may then be executed, along with the legacy software, to identify differences in behavior which are fed back into the behavioral model and subsequently into the new source code. This process may then be iterated with the verifiable code being deployable once behavioral differences are resolved.

Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.