HiFrog: SMT-based Model Checker for Software Verification

Abstract:

Incremental verification addresses the unique opportunities and challenges that arise when a verification task can be performed in an incremental way as a sequence of smaller closely related tasks, and thus can cop with verification of larger code while trying to avoid state explosion.

In this talk, we present HiFrog, a fully featured function-summarization-based bounded model checker that uses SMT as the modeling and summarization language. HiFrog supports verification based on several theories as the quantifier-free theories of linear real arithmetics (QFLRA), and the quantifier-free theories of uninterpreted functions (QFUF); implements several refinement strategies; and allows user-provided summaries input.

Biography:

Karine Even Mendoza: currently a PhD student at King's College London in the Software Modelling and Applied Logic group under the supervision of Dr Hana Chockler; does a collaborative research in SMT-based model checking with the USI Formal Verification and Security group; worked previously in research at eBay, Netanya, Israel and at IBM Research Labs, Haifa, Israel for several years; and obtained her M.Sc. in Computer Science from the Technion(2013) in the field of software verification and testing, software engineering and learning. The results of the M.Sc. thesis were presented at ISSTA 2013.