Reference:

Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Solving recursion-free horn clauses over li+uif. In Yang, pages 188–203.

Suggested BibTeX entry:

@inproceedings{DBLP:confaplasGuptaPR11,
    author = {Ashutosh Gupta and Corneliu Popeea and Andrey Rybalchenko},
    booktitle = {APLAS},
    editor = {Hongseok Yang},
    pages = {188-203},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Solving Recursion-Free Horn Clauses over LI+UIF},
    volume = {7078},
    year = {2011}
}