Programme

We have been building trustworthy agentic AI for code renovation by combining the creativity of LLMs with the rigor of static and dynamic program analysis, formal constraints, and meaningful human oversight. Rather than replacing software engineers, these hybrid human-AI systems enable safer, more transparent, and more reliable automation of complex software maintenance and evolution tasks. Our thorough evaluation demonstrates substantial improvements over existing approaches and successful adoption by major open-source projects.

Lingming Zhang is an Associate Professor at UIUC. His research interests involve designing, training and benchmarking LLMs and agents for more reliable and trustworthy software intelligence. His work has largely inspired the design of modern coding agents and has been widely adopted in practice.

Our group has developed a series of software quality assurance techniques for improving the reliability of agent harnesses. Our work spans two key directions: testing, where we develop harness-centric test generation techniques to uncover failures arising from interactions between agent harnesses and LLMs; and debugging, where we build SE agents that can automatically diagnose and fix harness bugs. Our techniques have reported hundreds of previously unknown bugs in real-world open-source agentic systems.

Aditya Thimmaiah is a final-year ECE PhD candidate at The University of Texas at Austin, advised by Dr Milos Gligoric. His research interest lies broadly at the intersection of programming languages (PL) and generative AI, with a focus on developing trustworthy AI for software engineering using PL and formal methods. His recent work studies whether LLMs can flexibly condition their reasoning on explicitly specified formal semantic rules even when those rules conflict with their pretrained priors, a capability that is important for building models that reason faithfully about formal specifications.

Bogdan "Bo" Stoica is a Visiting Lecturer and Postdoctoral Fellow at the University of Illinois Urbana-Champaign, working at the intersection of systems, software engineering and generative AI. His research focuses on the reliability, efficiency and trustworthy operation of complex software systems, including AI-assisted development. His recent work studies the behaviour of AI agents on system operation and reproducibility tasks, with particular interest in when agents faithfully execute predefined procedures versus intervening to modify the systems they are meant to operate and observe.

LLM agents are increasingly deployed in safety-critical applications, yet current guardrail systems fail to prevent violations of temporal safety policies. We present a novel general framework that provides run-time guarantees ensuring LLM agents adhere to temporal and state-dependent constraints. We evaluate our implementation, AGENT-C, on three real-world applications — retail customer service, airline ticket reservation and telecom customer service — with multiple language models, both open-weight and closed-weight, as agents. Our results demonstrate perfect conformance to the specification and increased safe utility over state-of-the-art alternatives.

AI agents are now involved in autonomous operations in safety-critical areas such as air traffic management, autonomous vehicle navigation and control of robotic systems. However, their use presents serious safety challenges. In this talk we present two complementary approaches that use ideas from logic and formal reasoning to provide runtime assurance for these systems — the synthesis of guaranteed control invariants, and the use of logic-based methods for intent inference.

Large reasoning models have demonstrated that ubiquitously useful generalization is possible across many domains. However, this capability is limited by classical assumptions on machine learning models, such as the test distribution matching the training distribution, the manifold hypothesis of relying on shared simple features across an otherwise complex dataset, and the availability of large datasets. These assumptions raise a critical question: how can AI generalize outside of such domains for problems in autonomy where there is inherent noise? In this talk, we mention how the foregoing assumptions are violated for important problems in these application domains. We posit that, at some level of abstraction, the shared symbolic structures across domains will enable greater generalization, and present research directions for neurosymbolic AI to achieve this vision of symbolic generalization that is robust to the gaps between AI and reality.

AI agents now write code faster than anyone can review it, and "looks right" is no longer good enough. Formal verification offers an independent, machine-checked notion of "right", but the obvious way to combine it with LLMs is expensive. Proof assistants give an agent almost no signal: a failed proof does not say whether the code is wrong or the proof just has not been found yet. So the agent burns tokens on neural search. An IMO-medal-level run at this scale costs thousands of GPU-hours and billions of tokens. This talk argues that the cheapest intelligence is a stronger feedback loop, not a bigger model. SMT solvers return proofs or counterexamples, but they can also fail silently with "unknown". We show how encoding programs in decidable logics removes that failure mode, and how this idea, together with relational abstraction and counterexample-guided refinement, underlies Ravencheck, our verifier for Rust. Properties are written like tests and checked automatically, and the LLM only fills in what the solver cannot. In early results on the TIP benchmarks, verification needs no hand-written lemmas or instantiations, finishes in minutes, and uses about 9× fewer tokens than a Lean 4 baseline.

With agentic workflows, the need for flexible, modular, and sound static analyzers has never been greater. Static analyzers are complex and hard to build. Composable interfaces will make it easier to build or generate. While there are well-understood theories for the modular definition of sound semantic reasoning domains, the challenge is that static analyzers are generally defined in a monolithic manner for a fixed language. In this talk, we explore how we might realize a cumulative approach to defining static analyzers that enables flexibly interpreting in different ways — for example, with different sensitivities, going forwards or backwards, mixing over- and under-approximations, and computing results in batch, incrementally, or on demand.

What happens when AI agents encounter tools and webpages designed to mislead them? This talk explores how attackers can exploit the external information agents rely on to decide what to do. Drawing on two recent studies, I will show how convincing tool descriptions can steer language model agents toward malicious tools, and how localized visual changes to webpages can induce unintended browser actions. These attacks reveal vulnerabilities in both how agents select relevant information and how they translate model outputs into executed actions. I will discuss why these attacks remain effective against existing defenses and what they teach us about evaluating agent security across the full path from perception to action.

Stefan Nagy is an Assistant Professor in the University of Utah's Kahlert School of Computing and director of the FuTURES³ Lab, where his research in software engineering, systems and security develops efficient and broadly applicable techniques for automated software vetting that have uncovered more than 270 previously unknown bugs and vulnerabilities.

As AI agents combine models and tools into multi-step workflows, their latency, cost and task quality become harder to anticipate. Making these systems dependable requires understanding how model and deployment choices affect these outcomes. I will present MaverIQ, an intent-based LLM serving system that lets users express their goals and takes responsibility for deployment decisions. Through lightweight profiling, analytical modeling and efficient use of fragmented GPU resources, MaverIQ makes informed deployment choices without expensive trial and error. I will then briefly discuss ongoing work on FlowMaker, which brings task-level requirements to workflow selection and deployment, and DAGGER, which aims to estimate workflow quality. These efforts provide building blocks toward agentic AI that can meet explicit performance, cost and quality requirements.

As AI transitions from conversational screens into cyber-physical environments, maintaining user agency and physical legibility becomes paramount. Drawing on recent projects from the ACME Lab — spanning augmented reality, dynamic behaviour authoring and sensorimotor feedback — this talk highlights design strategies for building predictable, adaptable and spatially grounded partners that seamlessly assist across real-world tasks.

This work examines how humans develop, perceive and evaluate trust in AI systems applied within the built environment, exploring the factors that influence users' confidence in AI-enabled technologies — including system transparency, reliability, explainability, accountability and perceived effectiveness. Beyond these technical competencies, it also studies how trust influences the extent to which humans adopt, accept and use AI systems in built environment applications.

Multimodal LLMs have shown the capability to browse the web, use computers, control robots and do many other exciting tasks. However, most of these systems run on closed, proprietary models hosted on remote third-party servers, with design decisions and training based on the priorities of a few closed labs aiming to serve a broad range of users. In this talk I lay out a different vision: smaller, local agents that run on users' own machines, keep their data private, and adapt to the needs and preferences of individuals and organizations. Achieving this vision requires new breakthroughs, both in the general capabilities of these smaller local models and in methods for improving and adapting these agents over time. I will discuss the work of my lab to address these challenges and lay out a hopeful vision for agents: one where individual users and organizations are empowered to shape the future of this exciting new technology.

Autonomous agents working with or around humans has long been a part of Human-Robot Interaction, a multidisciplinary field that investigates how people and robotic systems perceive, communicate and collaborate with one another. Inconveniently, many of the insights and findings we have that characterize human-human interactions do not hold true during human-agent interactions — often in surprising or contradictory ways. In this talk I provide an accessible introduction to two critical aspects of successful human-agent teaming: shared mental models and shared situational awareness. I will discuss results and lessons learned from my lab's work on the establishment and reconciliation of these aspects through our investigations into operationalizing agent identity, behavioural predictability, belief estimation and social manipulation, to make human-autonomy teams that are greater than the sum of their parts.

How can we design AI that is worthy of trust when people are at their most vulnerable? The Identity Lab studies AI in sensitive contexts, from gender classification to mental health to "generative ghosts" built on the data of those who have died. I will share findings from this work, including a recent study showing that people value emotional fidelity over factual fidelity in AI conversations, and early work with mental health professionals exposing tradeoffs when using AI for bereavement. Like edge cases in software, these contexts expose the normative assumptions we are building into AI systems and show that trust depends on how systems are used and what people expect from them.