The AsmRefProver (Asmeta Refinement correctness Prover) can be used to prove the correctness of refinement steps.

Download

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

Models

Some models with SMT contexts generated during the proof are available at AsmRefProverExamples.zip

Complete results regarding our experiments are available here.

Paper

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