Amazon Technologies, Inc.

Tongtong Xiang

Neha Rungta

Sean McLaughlin

John Byron Cook

Serdar Tasiran

Matthias Schlaipfer

Michael William Whalen

Marianna Rapoport

Florian Rabe

Disclosed are systems and methods that determine specification portions of Dafny code and transform those specifications into one or more annotations, expressions, comments, and/or assertions that are included in a destination code written in a destination language as part of a compilation of the Dafny code into the destination code. The annotations, expressions, comments, and/or assertions in the destination code may be utilized by a verification component, such as a Checker Framework, to detect errors that are introduced into the destination code by the compiler as part of the compilation or to verify the absence of errors in the destination code.

Retaining Dafny specifications

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.

Transitioning legacy software to be provably correct

Growing community of inventors

Seattle, WA, United States of America

Tongtong Xiang