Tool Artifact for ``Imperative Program Synthesis from Assertions by Abstract Static Analysis and SMT Mutations''

In this work, we describe the installation, usage, and evaluation results of the tool, denoted IMPSynth, introduced by the paper``Imperative Program Synthesis from Assertions by Abstract Static Analysis and SMT Mutations''. We provide step-by-step instructions on how to download, run, and compare the tool's outputs to outputs described in the paper. The tool is a research prototype tool for synthesizing imperative programs that meet behavioral specifications given in the form of assertions. In particular, we combine basic statement-directed enumerative search, static analysis via abstraction interpretation, and expression-directed enumerative search via (incremental) SMT-based mutations to efficiently explore all candidate complete programs generated from an input program template (with statement and expression holes) until a solution is found.