Seminars

Formal methods can provide strong correctness guarantees for today's computing systems, but their usage is often restricted to formal methods experts. Formal verification is then bottlenecked on these experts, limiting its effectiveness. This problem is acute in computer architecture, since many architects do not have formal methods expertise.

In this talk, I will present recent work with my students and collaborators that reduces the barriers to entry for computer architects to use formal methods. First, I will discuss our work on automatically generating formal…

Medical devices, healthcare delivery, and other cyber-physical systems depend on sensors to make safety-critical, automated decisions. My research lab investigates the problem of how to protect cyber-physical systems from adversaries who can maliciously control sensor output by subverting its semiconductor physics. Finding principled, systematic solutions is extremely important to give consumers confidence in innovative medical devices and other emerging technology. Unique to our embedded security research contributions is an emphasis on protecting the longevity of implanted batteries and…

Remarkable advances in imaging, computation, and technology are rapidly moving us into an era where biomedical knowledge discovery is increasingly limited only by creativity. This has resulted in unprecedented opportunities to improve the diagnosis and treatment of disease. The vision field has been at the forefront of these advances in AI for healthcare because of the easy accessibility of images and clinical data.…

Recent advances in digital health technologies are enabling biomedical researchers to reframe health optimization and disease treatment in a patient-specific, personalized manner. This talk will focus on my group’s research in two areas of relevance to digital health: (1) cardiogenic vibration sensing and analytics; and (2) musculoskeletal sensing with joint acoustic emissions and bioimpedance. Our group has extensively studied the timings and characteristics of cardiogenic vibration signals such as the ballistocardiogram and seismocardiogram, and applied these…

For safety, AI systems in health undergo thorough evaluations before deployment, validating their predictions against a ground truth that is assumed certain. However, this is actually not the case and the ground truth may be uncertain. Unfortunately, this is largely ignored in standard evaluation of AI models but can have severe consequences such as overestimating the future performance. To avoid this, we measure the effects of ground truth uncertainty, which we assume decomposes into two main components: annotation uncertainty which stems from the lack of reliable annotations, and…