BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Events - ECPv6.15.20//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-ORIGINAL-URL:https://events.ucsc.edu
X-WR-CALDESC:Events for Events
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:America/Los_Angeles
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:20240310T100000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:20241103T090000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:20250309T100000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:20251102T090000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:20260308T100000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:20261101T090000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Los_Angeles:20251119T110000
DTEND;TZID=America/Los_Angeles:20251119T121500
DTSTAMP:20260429T232332
CREATED:20251105T220936Z
LAST-MODIFIED:20251118T181912Z
UID:10005101-1763550000-1763554500@events.ucsc.edu
SUMMARY:CSE Colloquium - Flux: Refinement Types for Verified Rust Systems
DESCRIPTION:Presenter: Ranjit Jhala\, UCSD\n\nAbstract: Rust has risen as a language of choice for new systems code — from OS kernels to hypervisors\, firmware and run-times — as it is memory safe and provides the sort of abstractions needed for efficient low-level systems implementation. We present Flux\, a refinement type checker for Rust that shows how logical refinements can work in tandem with Rust’s ownership mechanisms to yield ergonomic type-based verification of low-level systems code. We then present a case study showing how Flux was used to formally verify process isolation in Tock: a microcontroller OS used in security-critical systems like the Google Security Chip (GSC) and Microsoft’s Pluton security processor. Our verification effort unearthed multiple subtle bugs that broke isolation\, allowing malicious applications to compromise the OS to potentially steal sensitive data or brick or take control of the OS. We describe how Flux helped design and implement a new granular process abstraction that is both simpler\, more efficient\, and yields formally verified security guarantees.\n\nBio:\nRanjit Jhala is a professor of Computer Science and Engineering at the University of California\, San Diego. He works on algorithms and tools that help engineer reliable computer systems. His work draws from and contributes to the areas of Model Checking\, Program Analysis\, and Automated Deduction\, and Type Systems. He helped create several influential and award winning systems including the BLAST software model checker and Liquid Types\, received ACM SIGPLAN’s Robin Milner Young Researcher Award\, and is a Fellow of the ACM.\n\nHosted by: Professor Mohsen Lesani\n\nLocation: Engineering 2\, Room E2-180\n*Refreshments such as coffee and pastries will be provided.\n\nZoom: https://ucsc.zoom.us/j/93445911992?pwd=YkJ2TQtF79h0PcNXbEcpZLbpK0coiY.1
URL:https://events.ucsc.edu/event/cse-colloquium-flux-refinement-types-for-verified-rust-systems/
LOCATION:Engineering 2\, Engineering 2 1156 High Street\, Santa Cruz\, CA\, 95064
CATEGORIES:Lectures & Presentations
ATTACH;FMTTYPE=image/jpeg:https://events.ucsc.edu/wp-content/uploads/2025/11/235.jpg
GEO:37.0009723;-122.0632371
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=Engineering 2 Engineering 2 1156 High Street Santa Cruz CA 95064;X-APPLE-RADIUS=500;X-TITLE=Engineering 2 1156 High Street:geo:-122.0632371,37.0009723
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=America/Los_Angeles:20251121T140000
DTEND;TZID=America/Los_Angeles:20251121T160000
DTSTAMP:20260429T232332
CREATED:20251021T182427Z
LAST-MODIFIED:20251022T181942Z
UID:10004960-1763733600-1763740800@events.ucsc.edu
SUMMARY:Torres\, S. (ECE) - An Integrated Platform for Real-time Monitoring and Support of 3D Tissue Growth
DESCRIPTION:Organoids are three-dimensional tissue cultures that model real organs and serve as valuable tools for studying development\, disease\, and treatment response. Traditional methods\, which rely on manual handling and incubators\, limit consistency and real-time monitoring. To address these issues\, we developed a modular microfluidic platform that integrates automated feeding\, live fluorescence imaging\, and environmental control without the need for a standard incubator. The core of the system is a vertically oriented PDMS-glass chip that enables precise media delivery and continuous imaging of small 3D structures such as organoids. Using fluorescent dyes to mimic molecules\, such as nutrients or drugs\, we tracked their movement through tissue in real time without invasive sensors. This setup maintains metabolic stability and provides detailed insight into molecular transport\, which improves applications in disease modeling\, drug testing\, and personalized medicine. \n  \nEvent Host- Sebastián Torres\, Ph.D. Candidate\, Electrical & Computer Engineering  \nAdvisor: Mircea Teodorescu \n  \nZoom- https://ucsc.zoom.us/j/2333595627?pwd=aWtwL3V2QnFTMkNDSWowZnRNS0xSQT09 \nPasscode- 579836
URL:https://events.ucsc.edu/event/torres-s-ece-an-integrated-platform-for-real-time-monitoring-and-support-of-3d-tissue-growth/
LOCATION:
CATEGORIES:Ph.D. Presentations
ATTACH;FMTTYPE=image/png:https://events.ucsc.edu/wp-content/uploads/2025/10/option-3-1.png
END:VEVENT
END:VCALENDAR