PRECISE Seminar: Assertion-driven Development and Analyses
University of Texas, Austin
Abstract: To increase reliability, developers have long used assertions — logical statements that are expected to be true — as lightweight specifications of crucial properties of code. Assertions have predominantly served two purposes: documentation and runtime checking. We envision a far broader role of assertions where they are the cornerstone of a wide range of analyses that synergistically promise to bring about an unprecedented increase in reliability.
This talk describes our ongoing work on assertion-driven development and analyses, where developers first assert designs and then write code, static analyses check conformance of code to designs, testing checks correctness of executable code, and runtime checking detects erroneous executions, which error recovery repairs as desired. Our vision is to enable new analyses that uniformly apply across the whole spectrum of software design, development, and maintenance — static checking, testing, runtime checking, and error recovery all use the same assertions that developers write just once. Consequently, writing assertions becomes much more attractive. As developers write more assertions, they benefit not only from the new analyses but also from leveraging a host of existing analyses that utilize assertions.
Biography: Sarfraz Khurshid is an Associate Professor in the Department of Electrical and Computer Engineering at the University of Texas at Austin, where he leads the Software Verification and Testing Research Group. He obtained PhD in Computer Science at MIT in 2004. He received BSc in Mathematics and Computer Science from Imperial College London and read Part III of the Mathematical Tripos at Trinity College Cambridge. His current research focuses on software testing, model checking, specification languages, code conformance, data structure repair, and parallel and incremental techniques for software analysis. He is a recipient of the ACM SIGSOFT Impact Paper Award for 2012, two ACM SIGSOFT Distinguished Paper Awards (ISSTA 2002 and ICSE 2010), a Best Research Paper Award (ASWEC 2009), and an NSF CAREER Award (2009). He is an avid player and keen follower of squash (the racket sport, not the vegetable).