Time: 3:00 - 4:00pm Venue: Queen Mary, Mile End campus: Bancroft Road Lecture Theatre BR 3.02
Part of our Distinguished Lecture series
EVENT POSTPONED
Speaker: Associate Professor Natasha Sharygin, Universita della Svizzera Italiana (University of Lugano) - Informatics Department
Title: HiFrog: SMT-based Function Summarization for Software Verification
Abstract: Function summarization has recently become a popular approach for incremental software verification. In this talk I will present our recent tool, HiFrog, a fully featured function-summarization-based model checker that uses SMT as the modeling and summarization language. The tool supports three encoding precisions through SMT: uninterpreted functions, linear real arithmetics, and propositional logic. In addition the tool allows optimized traversal of reachability properties, counter-example-guided summary refinement, summary compression, and user-provided summaries. I will describe the use of the tool through the description of its architecture and a rich set of features and compare it to our earlier work where we invented the SAT-based function summarization approach. The presentation will be complemented by an experimental evaluation on the practical impact the different SMT precisions have on program verification.
Biography: Professor Natasha Sharygin joined USI in 2005 where she started the USI Formal Verification and Security group. She came to Lugano after working for several years at Carnegie Mellon University, USA, where Professor Natasha Sharygin now holds an adjunct Professorship at SCS. Her research interests are in software and hardware verification (e.g. Model-checking, Abstract Interpretation, Decision Procedures for first-order theories, Satisfiability Modulo Theories (SMT)), information security, and concurrent and distributed computing. Research of her group has been supported by Swiss National Science Foundation, Hasler Foundation and EU FP7 PINCETTE project.
All welcome (especially students), no pre-booking required.
This lecture will be preceded by tea at 2.45pm and followed by a reception - both in the Informatics Hub