The AsmRefProver (Asmeta Refinement correctness Prover) can be used to prove the correctness of refinement steps.
Download the tool: AsmRefProver.jar
How to run
To 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
Some models with SMT contexts generated during the proof are available at AsmRefProverExamples.zip
Complete results regarding our experiments are available here.
P. 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