Asmeta | Refinement prover | |
The AsmRefProver (Asmeta Refinement correctness Prover) can be used to prove the correctness of refinement steps. DownloadDownload the tool: AsmRefProver.jar How to runTo run AsmRefProver java -jar AsmRefProver.jar [options...] abstractModel.asm refinedModel.asm -ep : execute the proof (default: false) -log : show the SMT context (default: false) -sp : save the proof (default: false) The tool is based on the SMT solver Yices that can be downloaded from here. You have to put libyices.dll (Windows users) or libyices.so (Linux users) in the same folder of the jar file. Proof invariants must be specified in the model in the invariant section. Their name must start with inv_invForRef ModelsSome models with SMT contexts generated during the proof are available at AsmRefProverExamples.zip Complete results regarding our experiments are available here. PaperP. Arcaini, A. Gargantini, E. Riccobene. SMT-based automatic proof of ASM model refinement, in 14th International Conference on Software Engineering and Formal Methods (SEFM 2016), Vienna, Austria, July 4-8, 2016 doi |