|
|
--- |
|
|
license: mit |
|
|
language: |
|
|
- en |
|
|
base_model: |
|
|
- Qwen/Qwen2.5-Coder-7B-Instruct |
|
|
--- |
|
|
|
|
|
## Introduction |
|
|
|
|
|
We present a fine-tuned model for formal verification tasks. It is fine-tuned in five formal specification languages (Cog, Dafny, Lean4, ACSL, and TLA) on six formal-verification-related tasks: |
|
|
|
|
|
- **Requirement Analysis**: given requirements and description of the verification or modeling goals, decomposing the goal into detailed verification steps |
|
|
|
|
|
- **Proof/Model Generation**: given requirements and description of the verification or modeling goals, writing formal proofs or models that can be verified by verifier/model checker. |
|
|
|
|
|
- **Proof segment generation** |
|
|
|
|
|
- **Proof Completion**: complete the given incomplete proofs or models |
|
|
|
|
|
- **Proof Infilling**: filling in the middle of the given incomplete proofs or models |
|
|
|
|
|
- **Code 2 Proof**: (Currently only support for ACSL whose specification is in form of code annotations) given the code under verification, generate the proof with the specifications |
|
|
|
|
|
## Application Scenario |
|
|
|
|
|
<p align="center"> |
|
|
<img width=100%" src="figures/application.png"> |
|
|
</p> |
|
|
|
|
|
|
|
|
## Supported Formal Specification Languages |
|
|
|
|
|
<p align="center"> |
|
|
<img width=100%" src="figures/examples.png"> |
|
|
</p> |
|
|
|
|
|
## Data Preparation Pipeline |
|
|
<p align="center"> |
|
|
<img width=60%" src="figures/data-prepare.png"> |
|
|
</p> |
|
|
|
|
|
|
