menu

School of Electronic Engineering and Computer Science

News & Events menu

Distinguished Lecture by Professor Natasha Sharygina

17 October 2018

Time: 2:00 - 3:00pm
Venue: Bancroft Road Lecture Theatre BR 3.01

Title: HiFrog: SMT-based Function Summarization for Software Verification

Speaker: Professor Natasha Sharygina - Universita della Svizzera Italiana (University of Lugano) - Informatics Department

Event is preceded at 1:45pm by tea and followed by a reception - both in the Informatics Hub. All welcome (especially students), no pre-booking required.

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.

Bio:
Natasha Sharygina is a Full professor at the University of Lugano, Switzerland where she directs a Formal Verification and Security Lab. Her research focuses on improving the program development process through formal methods of specification and verification. In particular, her interests lie in automated formal verification with a specific focus on software/hardware model checking, information security, static analysis, abstract interpretation and decision procedures.  Prof. Sharygina received a Ph.D. degree from the University of Texas at Austin, USA in 2002. Her professional experience includes consulting at Bell Labs, Lucent Technologies Computing Sciences Research in 2000-2001 and research faculty positions at Carnegie Mellon University, SEI in 2002-2005 and at Imperial college London in 2018.  Results of Prof. Sharygina's and her research group's work resulted in award-winning theoretical frameworks and practical tools to enable sound and scalable verification of industrial-size systems.

…………………………………………………………………………………………………….
Forthcoming:
Prof John Chowning
Stanford University, Stanford, California - Centre for Computer Research in Music and Acoustics (CCRMA)
28/11/2018

Return to top