Please join us for the CS UNDERGRADUATE FACULTY SPEAKER SERIES - “Beyond the Bytes”

Abstract:  Algorithms increasingly influence decisions about employment, credit, healthcare, taxation, and access to public services. But what does it mean for an algorithm to treat people fairly—and how can we verify that it does? Unlike traditional correctness requirements, fairness cannot usually be assessed by examining a single execution. We must compare how the algorithm behaves for different individuals or under different circumstances.

This talk introduces hyperproperties, a framework for specifying requirements that relate multiple executions of a system. Through examples from machine learning, autonomous systems, and tax-preparation software, we will see how the same perspective can capture fairness, privacy, and legal compliance. We will then explore how ideas from logic and formal verification can help determine whether a system satisfies these requirements, and why doing so is considerably more challenging than checking conventional safety properties. The talk will conclude with recent approaches that use mathematical certificates to provide guarantees about such relational behavior. No prior background in formal methods is required.

Bio: Ashutosh Trivedi is an Associate Professor of Computer Science at the University of Colorado Boulder. His research lies at the intersection of formal methods, reinforcement learning, and trustworthy AI, with an emphasis on providing rigorous guarantees for learning-enabled systems. His current work investigates hyperproperties as a framework for reasoning about privacy, fairness, and legal compliance, as well as correct-by-construction reinforcement learning for implantable medical devices.

Trivedi received the 2022 NSF CAREER Award and a 2024 Royal Society Wolfson Visiting Fellowship. In 2026, he received the CEAS Outstanding Faculty Research Advisor and Mentor Award. Research from his group has received paper awards at CAV, HSCC, and SAS.