DynaMate: Dynamically Inferring Loop Invariants for Automatic Full Functional Verification - HVC 2014
by Juan Pablo Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, Andreas Zeller

Proceedings of 10th Haifa Verification Conference (HVC 2014), LNCS, Springer, November 2014.

Download as PDF file.

Abstract

DYNAMATE is a tool that automatically infers loop invariants and uses them to prove Java programs correct with respect to a given JML functional specification. DYNAMATE improves the flexibility of loop invariant inference by integrating static (proving) and dynamic (testing) techniques with the goal of combining their complementary strengths. In an experimental evaluation involving 26 Java methods of java.util annotated with JML pre- and postconditions, it automatically discharged over 97% of all proof obligations, resulting in automatic complete correctness proofs of 23 out of the 26 methods.

BibTeX Entry

@inproceedings{galeotti-hvc-2014,
    title = "DynaMate: Dynamically Inferring Loop Invariants for Automatic Full Functional Verification",
    author = "Juan Pablo Galeotti and Carlo A. Furia and Eva May and Gordon Fraser and Andreas Zeller",
    year = "2014",
    month = nov,
    booktitle = "Proceedings of 10th Haifa Verification Conference (HVC 2014)",
    location = "Haifa, Israel",
    publisher = "Springer",
    series = "LNCS",
}

Show all publications of the Software Engineering Chair.