Upcycling Formal Specifications for Similar Implementations with Arís.
Kuruvilla George Aiyankovil, Rosemary Monahan, Diarmuid O’Donoghue · Maynooth University ePrints and eTheses Archive (Maynooth University) · 2021
We describe the Arís system for creating new formal specifications for source code by transferring existing specifications to similar implementations. We show the code graphs underlying its operation, graph matching supports retrieval, and pattern completion enables transfer of specifications to new implementations. A theorem prover formally verifies the new specifications.