Improving ABV by generation and abstraction of PSL assertions