Retaining Dafny specifications
US11921616B1 · kind B1 · utility
Assignee
Inventors
Key dates
| Filing date | Mar 29, 2022 |
| Grant date | Mar 5, 2024 |
| Priority date | — |
| Expiry date | Mar 29, 2042 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3608
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
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.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.