Patent ID: 11921616
Assignee: AMAZON TECHNOLOGIES, INC.
Field: Computer technology (Electrical engineering)
Classification: CPC G | IPC G

Claim 5:
6. A computing system, comprising:
one or more processors; and
a memory storing program instructions that, when executed by the one or more processors, cause the one or more processors to at least:
initiate, with a compiler, a compiling of a first code written in a Dafny programming language to a second code written in a destination programming language;
detect, as part of the compiling, a specification included in the first code;
compile the specification into at least one of an annotation that is understandable to a verification component, an expression that is understandable to the verification component, a comment that is understandable to the verification component, or an assertion that is understandable to the verification component;
include the at least one of the annotation, the expression, the comment, or the assertion in the second code; and
verify, with the verification component, the second code, wherein the verification component utilizes the at least one of the annotation, the expression, the comment, or the assertion to verify at least a portion of the second code.