Function summarization can be used as a means of incremental verification based on the structure of the program. I present HiFrog, a multi-goal function-summarization-based framework, which uses Satisfiability Modulo Theories (SMT) as the modeling and summarization language. The tool supports three encoding precisions through SMT: uninterpreted functions, linear real arithmetics, and propositional logic. Its main target is bounded model checking. In addition, the tool allows optimized traversal of user-defined assertions, counter-example-guided summary refinement, summary compression, and user-provided summaries. In the talk, I will describe already established and ongoing developments within the framework and will conduct an interactive demo.

Grigory Fedyukovich is a postdoc at PLSE lab of University of Washington, USA, working with Prof. Rastislav Bodik. He completed his PhD at Formal Verification Lab of University of Lugano, Switzerland (2015), under supervision of Prof. Natasha Sharygina, with whom he continues his collaboration. He graduated from Saint Petersburg State University, Russia (2008), and also did two internships at Institute of Cybernetics, Estonia (2009); and at National University of Singapore (2010). The main focus of his research is Software Model Checking, and Synthesis.