Formal Methods for Dependable Computing: From Models, through Software, to Circuits

Formal Methods for Dependable Computing: From Models, through Software, to Circuits Speaker/Performer: Sanjit A. Seshia, Asst. Professor of EECS, UC Berkeley Live broadcast at mms://media.citris.berkeley.edu/webcast; Questions can be sent via Yahoo IM to username: citrisevents. The schedule for the fall Research Exchange is at www.citris-uc.org Abstract: Computing has become ubiquitous and indispensable: it is embedded all around us, in cell phones, automobiles, medical devices, and much more. This ubiquity brings with it a growing challenge to ensure that our computing infrastructure is also dependable and secure. We need to develop and maintain complex software systems on top of increasingly unreliable computing substrates under stringent resource constraints such as energy usage. In this talk, I will discuss how formal methods --- mathematical techniques for specification, design, and verification of systems --- can help improve system dependability. As illustrative case studies, I will present work we have done on verifying timing properties of control software (relevant for cyber-physical systems, such as automobiles), analyzing the impact of faulty devices in digital circuits, and designing electronic voting machines so as to enable verification of desired properties. The talk will also touch upon some of the core underlying technology, such as satisfiability modulo theories (SMT) solvers, and describe challenges for the future. Bio: Sanjit A. Seshia is an assistant ...



http://www.youtube.com/watch?v=VUyfi6JJRgA&hl=en

Recommend : circuit board design circuit boards design