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