HiFrog: SMT-based Function Summarization for Software Verification

Decanato - Facoltà di scienze informatiche

Data d'inizio: 25 Gennaio 2017

Data di fine: 26 Gennaio 2017

Speaker:

Grigory Fedyukovich

University of Washington, USA

Date:

Wednesday, January 25, 2017

Place:

USI Lugano Campus, room SI-007, informatics building (Via G. Buffi 13)

Time:

15:30

Abstract:

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.

Biography:

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.