CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Triggerless happy: Intermediate verification with a first-order prover

Yuting Chen (Institutionen för Data- och informationsteknik, Formella metoder (Chalmers)) ; Carlo A. Furia (Institutionen för Data- och informationsteknik, Formella metoder (Chalmers))
Lecture Notes in Computer Science - 13th International Conference on Integrated Formal Methods, IFM 2017, Turin, Italy, 20-22 September 2017 Vol. 10510 (2017), p. 295-311.
[Konferensbidrag, refereegranskat]

SMT solvers have become de rigueur in deductive verification to automatically prove the validity of verification conditions. While these solvers provide an effective support for theories—such as arithmetic—that feature strongly in program verification, they tend to be more limited in dealing with first-order quantification, for which they have to rely on special annotations—known as triggers—to guide the instantiation of quantifiers. Writing effective triggers is necessary to achieve satisfactory performance with SMT solvers, but remains a tricky endeavor—beyond the purview of non-highly trained experts. In this paper, we experiment with the idea of using first-order provers instead of SMT solvers to prove the validity of verification conditions. First-order provers offer a native support for unrestricted quantification, but have been traditionally limited in theory reasoning. By leveraging some recent extensions to narrow this gap in the Vampire first-order prover, we describe a first-order encoding of verification conditions of programs written in the Boogie intermediate verification language. Experiments with a prototype implementation on a variety of Boogie programs suggest that first-order provers can help achieve more flexible and robust performance in program verification, while avoiding the pitfalls of having to manually guide instantiations by means of triggers.

Denna post skapades 2017-10-25.
CPL Pubid: 252756


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för Data- och informationsteknik, Formella metoder (Chalmers)


Datavetenskap (datalogi)

Chalmers infrastruktur