BEGIN:VCALENDAR VERSION:2.0 PRODID:-//Drupal iCal API//EN X-WR-CALNAME:Events iCal Start May 2024 X-WR-TIMEZONE:America/New_York BEGIN:VTIMEZONE TZID:America/New_York X-LIC-LOCATION:America/New_York BEGIN:DAYLIGHT TZNAME:EDT TZOFFSETFROM:-0500 TZOFFSETTO:-0400 DTSTART:20260308T070000 END:DAYLIGHT BEGIN:DAYLIGHT TZNAME:EDT TZOFFSETFROM:-0500 TZOFFSETTO:-0400 DTSTART:20250309T070000 END:DAYLIGHT BEGIN:DAYLIGHT TZNAME:EDT TZOFFSETFROM:-0500 TZOFFSETTO:-0400 DTSTART:20240310T070000 END:DAYLIGHT BEGIN:STANDARD TZNAME:EST TZOFFSETFROM:-0400 TZOFFSETTO:-0500 DTSTART:20251102T060000 END:STANDARD BEGIN:STANDARD TZNAME:EST TZOFFSETFROM:-0400 TZOFFSETTO:-0500 DTSTART:20241103T060000 END:STANDARD BEGIN:STANDARD TZNAME:EST TZOFFSETFROM:-0400 TZOFFSETTO:-0500 DTSTART:20231105T060000 END:STANDARD END:VTIMEZONE BEGIN:VEVENT UID:6a33262c770c3 DTSTART;TZID=America/New_York:20260623T140000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260623T153000 LOCATION:Gates and Hillman Centers SUMMARY:Doctoral Thesis Proposal - Qi Pang CLASS:PUBLIC DESCRIPTION:Speaker: QI PANG\, Ph.D. Student\, Computer Science Department\ , Carnegie\nMellon University\n\nTalk Title: Provably Secure Approaches fo r Generative AI Systems: From\nPrivate Inference to Accountable Agents\n\n Generative AI is moving into high-stakes domains such as healthcare\,\nfin ance\, and law\, and it is evolving from static query-response models\nint o autonomous agents that hold memory\, call external tools\, and\ncommunic ate with one another. This shift expands the attack surface\ndramatically. A modern generative AI system spans several layers: the\ninputs a user pr ovides\, the model and the privacy guarantee it claims\,\nthe outputs it p roduces\, and the messages its agents exchange. Each of\nthese layers rest s on a fragile trust assumption: inputs may carry\nsensitive personal info rmation\, outputs cannot be reliably attributed\nto their source\, inter-a gent messages can hide cryptographically\nundetectable payloads\, and a mo del's advertised differential privacy\nguarantee may quietly fail to hold. Heuristic defenses such as input\nredaction\, AI-text classifiers\, trans cript monitors\, and procedural\nprivacy audits offer little assurance aga inst a motivated adversary\,\nbecause they rest on pattern matching rather than proof.\n\nThis thesis argues that trustworthiness should be a provab le\,\nfoundational property of generative AI systems\, achieved by\nco-des igning applied cryptography (secure multi-party computation\,\nhomomorphic encryption\, and zero-knowledge proofs) and differential\nprivacy with th e structure of modern generative models. I develop this\nargument across t he four layers above through four systems. BOLT\n(completed) protects user inputs with privacy-preserving Transformer\ninference that is accurate an d an order of magnitude more efficient\nthan prior work. A study of LLM wa termarking (completed) establishes\nthe fundamental trade-offs that govern output provenance and shows\nprecisely when heuristic watermarks can be r emoved or forged. For\ninter-agent communication\, I propose a study of st eganographic\ncollusion that constructs a high-capacity covert channel and a\nprovable mechanism to disrupt it. For the model layer\, I propose\nNoi sette\, a system that makes differential privacy verifiable by\ncertifying \, in zero knowledge\, that the differential privacy noise was\nsampled co rrectly. Together\, these systems chart a path toward\ngenerative AI that is not only powerful but also demonstrably private\,\naccountable\, and go vernable.\n\nThesis Committee\n\nVirginia Smith (Co-chair)\n\nWenting Zhen g (Co-chair)\n\nGiulia Fanti\n\nSomesh Jha (University of Wisconsin Madiso n)\n\nAdditional Information\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c782d6 DTSTART;TZID=America/New_York:20260528T140000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260528T153000 LOCATION:Gates and Hillman Centers SUMMARY:Doctoral Thesis Proposal - Edward Justin Chen CLASS:PUBLIC DESCRIPTION:Speaker: EDWARD JUSTIN CHEN\, Ph.D. Student\, Computer Science\ nDepartment\, Carnegie Mellon University\n\nTalk Title: Democratizing Secu re Computation: Compilers for\nPrivacy-Preserving Programs\n\nAdvanced ana lytics and machine learning increasingly depend on data\nthat is sensitive \, regulated\, and distributed across organizations.\nSecure multiparty co mputation (MPC) and fully homomorphic encryption\n(FHE) offer a path aroun d this barrier by allowing computation over\nprivate inputs without reveal ing the underlying data. Yet despite\ndecades of cryptographic progress\, privacy-preserving computation\nremains difficult to deploy in practice: p erformance overheads are\nhigh\, and optimization requires expert domain k nowledge.\n\nThis thesis argues that compilers are essential for democrati zing the\nuse of privacy-preserving computation. Rather than requiring\nap plication developers to manually design cryptographic protocols\,\nthis wo rk treats the key performance decisions in MPC and FHE as\nstatic optimiza tion problems over a program’s intermediate\nrepresentations (IR). Silph is a compiler that uses integer linear\nprogramming (ILP) to optimize the operation and conversion costs of\nmixed MPC primitives within hybrid MPC protocols. Rotom is an FHE\ncompiler that automatically assigns ciphertex t layouts to tensor\nprograms\, finding efficient packings that minimize e xpensive data\nmovement operations. Orbit is another FHE compiler that als o uses ILP\nto jointly place bootstrap and rescale operations by reasoning about\nthe dependencies between ciphertext levels and scales. Together\, these\nsystems show that compiler automation can reduce the expertise\nreq uired to build privacy-preserving applications while improving the\nperfor mance of the resulting cryptographic programs. The remaining\nwork explore s an open problem on how AI-driven methods\, such as\nOpenEvolve\, operati ng over compiler IRs  and cost models can discover\nbetter cryptographic optimization strategies.\n\nThesis Committee:\n\nWenting Zheng (Co-Chair)\ n\nFraser Brown (Co-Chair)\n\nBryan Parno\n\nAlex Ozdemir (Georgia Institu te of Technology)\n\nSrini Devadas (Massachusetts Institute of Technology) \n\n \n\nAdditional Information\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c78826 DTSTART;TZID=America/New_York:20260515T130000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260515T143000 LOCATION:Gates and Hillman Centers SUMMARY:Doctoral Thesis Proposal - Timothy Kim CLASS:PUBLIC DESCRIPTION:Speaker: TIMOTHY KIM\, Ph.D. Student\, Computer Science Departm ent\,\nCarnegie Mellon University\n\nTalk Title: Efficient Data Storage Pr ovisioning\, Placement\, and\nTransitions at Scale\n\nExascale storage sys tems are under increasing pressure to store more\ndata while providing gre ater performance per byte. Historically\,\nhyperscale storage systems have relied on a two-tiered hierarchy:\nhard-disk drives store most bytes\, wh ile smaller flash tiers absorb\nrequests for hot and performance-critical data. This design is\nbecoming increasingly difficult to sustain. Datacent er data is getting\nwarmer with the proliferation of AI/ML and analytics-h eavy workloads\,\nwhile storage devices are becoming denser without propor tional\nimprovements in per-byte performance or endurance. As a result\,\n enabling denser storage devices at exascale requires improving both\nthe s oftware storage system and the hardware provisioning strategies\nfor moder n datacenter workloads.\n\nThis thesis shows that exascale storage systems can enable denser\nstorage options by jointly reducing internal IO and im proving data\nplacement/hardware provisioning decisions. The first part of this\nthesis\, Morph\, reduces IO associated with lifetime redundancy\ntr ansitions. Morph introduces a novel hybrid redundancy scheme for\nearly-li fe data and a system designed around a new erasure-code for\nlate-life\, r educing ingest and transcode overheads. The second part of\nthis thesis de velops a total-cost-of-ownership (TCO) model and\noptimizer for exascale s torage provisioning. This model determines the\nminimum-cost set of hardwa re necessary to serve datacenter workloads\nand shows how heterogeneous co nfigurations can cost-effectively enable\ndense devices in modern datacent ers.\n\nWe propose work that connects these two directions by modeling sto rage\nworkloads from the bottom up\, using fine-grained lifetime and\ntemp erature transition behavior to reason about provisioning and\nplacement de cisions. By understanding how data cools and survives\nthroughout its life time\, this work aims to produce a more precise\nframework that co-optimiz es the heterogeneous storage mixture and the\nplacement of data across the storage tiers. Together\, these\ncontributions show how storage systems c an cost-effectively service\ncontemporary storage workloads with denser me dia and enable the\nmassive growth in data demand.\n\nThesis Committee\n\n Greg Ganger (Co-Chair)\n\nRashmi Vinayak (Co-Chair)\n\nGeorge Amvrosiadis\ n\nSaurabh Kadekodi (Google)\n\nAdditional Information \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c78d67 DTSTART;TZID=America/New_York:20260513T100000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260513T113000 LOCATION:Gates and Hillman Centers SUMMARY:Doctoral Thesis Proposal - Sophia Roshal CLASS:PUBLIC DESCRIPTION:Speaker: SOPHIA ROSHAL\, Ph.D. Student\, Computer Science Depar tment\,\nCarnegie Mellon University\n\nTalk Title: Adjoint Types for Funct ional Programming\n\nSubstructural type systems offer a principled foundat ion for reasoning\nabout resource usage by controlling the structural rule s of weakening\,\ncontraction\, and exchange. Linear\, affine\, strict\, a nd ordered types\neach enable distinct optimizations and semantic guarante es. However\,\nsystems restricted to a single structural discipline are of ten too\nrigid for practical programming\, limiting expressiveness and\npr eventing programs from simultaneously exploiting multiple structural\nprop erties.\n\nThis thesis develops Adjoint Types\, a logically founded substr uctural\ntype system based on Adjoint Logic\, that supports the principled \ncombination of multiple substructural modes within a single language.\nT his design preserves the practical expressiveness of an unrestricted\nlang uage\, while still permitting mode based optimizations on the\npieces of t he program that allow them.\n\nThe proposal proceeds in four parts. First\ , we present Adjoint Natural\nDeduction\, including both a declarative and algorithmic type system\,\nand establish soundness and completeness with respect to a sequent\ncalculus formulation. Second\, we develop a mode inf erence procedure\nthat supports mode polymorphism and eliminates the need for manual\nmode annotations. Third\, we extend the framework with ordered modes\,\nestablishing decidability for a corresponding type system\, whil e\noutlining ongoing work toward practical type-checking algorithms.\nFour th\, we propose generalized pattern matching in the adjoint\nsetting\, dev eloping a logically sound approach to nested patterns via\nfocusing and ou tlining extensions to support wildcards and ordered\nmodes.\n\nTogether\, these contributions establish ordered adjoint types as a\nlogical foundati on for substructural functional programming languages\nand logical framewo rks\, enabling structural properties to drive\ncompiler optimizations and intensional program behavior without\nsacrificing practical usability. \n \nThesis Committee:\n\nFrank Pfenning (Chair) \n\nJan Hoffmann\n\nJonatha n Aldrich\n\nBrigitte Pientka (McGill University)\n\nChris Martens (Northe astern University) \n\nAdditional Information\n\nIn-person and Zoom\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c79288 DTSTART;TZID=America/New_York:20260512T170000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260512T183000 LOCATION:Gates and Hillman Centers SUMMARY:Doctoral Thesis Proposal - Gabriele Oliaro CLASS:PUBLIC DESCRIPTION:Speaker: GABRIELE OLIARO\, Ph.D. Student\, Computer Science Dep artment\,\nCarnegie Mellon University\n\nTalk Title: Rethinking the AI Sta ck: Systems for Agents and Agents for\nSystems\n\nLarge language models ha ve become central infrastructure for modern AI\napplications\, but running them efficiently remains a major systems\nchallenge. Larger and more capa ble models require more GPU\ncomputation\, GPUs remain expensive\, and sop histicated applications\nsuch as agents require low latency and predictabl e service-level\nobjectives to be practically usable. At the same time\, i nference\noptimization increasingly depends on deep specialized expertise in\nscheduling\, memory management\, and GPU kernel engineering. This\nexp ertise is difficult to scale because model architectures and\naccelerator platforms evolve rapidly\, introducing new operators\,\nprecision formats\ , parallelization patterns\, and hardware-specific\noptimization requireme nts.\n\nThis thesis develops systems that use model-driven and agentic\nte chniques to automate parts of this optimization process. SpecInfer\nuses s maller language models to speculate on the outputs of larger\nmodels\, con verting otherwise serial autoregressive decoding into\nparallel verificati on. SuffixDecoding extends this idea to agentic\nworkloads by caching and reusing prior generation patterns to\nspeculate with minimal GPU overhead. FlexLLM automates fine-grained\nresource allocation between latency-criti cal inference and\nthroughput-oriented finetuning\, allowing both services to share GPUs\nwhile preserving inference service-level objectives. The r emaining\nwork moves from optimizing inference systems with AI techniques to\nusing AI agents to optimize the systems themselves. FastKernels\nprovi des a production-faithful benchmark for LLM-based GPU kernel\nagents\, and the proposed kernel agent will use compiler feedback\,\ncorrectness tests \, runtime measurements\, and hardware feedback to\ngenerate optimized ker nels for rapidly evolving operators such as\nlinear attention\, state-spac e models\, mixture-of-experts routing\,\nquantized inference\, and multimo dal fusion.\n\nThesis Committee\n\nZhihao Jia (Chair)\n\nTianqi Chen\n\nPh illip Gibbons\n\nHao Zhang (University of California\, San Diego)\n\nAddit ional Information\n\nIn-person & Zoom\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7975e DTSTART;TZID=America/New_York:20260505T100000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260505T113000 LOCATION:Gates and Hillman Centers SUMMARY:Doctoral Thesis Proposal - Carlos G. Martin CLASS:PUBLIC DESCRIPTION:Speaker: CARLOS G. MARTIN\, Ph.D. Student\, Computer Science De partment\,\nCarnegie Mellon University\n\nTalk Title: Solving infinite gam es with deep multiagent reinforcement\nlearning\n\nIn this thesis\, we stu dy the problem of solving infinite games. Such\ngames can have infinitely many states\, actions\, players\, and steps.\nUnlike mean‑field games\, our players need not be symmetric or\nexchangeable. Furthermore\, we allow such games to have partial\nobservability\, hidden information\, imperfec t recall\, stochastic state\ntransitions\, discontinuous utility functions \, and interdependent\nsocial preferences (i.e.\, matrix-valued discount f actors). Together\,\nthese properties can model a wide range of highly com plex\, real-world\nscenarios that defy traditional game-theoretic solvers. \n\nTo tackle this problem\, we propose a unified framework grounded in\nd eep multiagent reinforcement learning. It includes five core\ncomponents.\ n\nFirst\, it introduces randomized policy networks (RPNs) to model\nobser vation-dependent mixed strategies over infinite action\nspaces.Second\, it represents complex strategy profiles across an\ninfinite continuum of pla yers using player-to-strategy networks\n(P2SNs).Third\, it evolves these r epresentations through a\nshared-parameter simultaneous gradient (SPSG)\, which extends the\nstandard simultaneous gradient to this shared-parameter regime.Fourth\,\nto ensure computational efficiency\, it estimates this g radient using\nrandomized parameter perturbations via a joint-perturbation \nsimultaneous pseudo-gradient (JPSPG).Fifth\, it employs approximate\nexp loitability descent (ApproxED) with learned best-response functions\n(BRFs ).\n\nWe propose to benchmark our approach on a diverse suite of real-worl d\ndomains. These include financial markets\, traffic flow\,\nepidemiologi cal contagion\, energy grids\, and evolutionary ecology.\n\nThesis Committ ee:\n\nTuomas Sandholm (Chair)\n\nVincent Conitzer\n\nFei Fang\n\nIan Gemp (Google)\n\nAdditional Information\n\nIn-person and Zoom\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c79c06 DTSTART;TZID=America/New_York:20260430T150000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260430T163000 LOCATION:Newell-Simon Hall SUMMARY:Doctoral Thesis Proposal - Noah G. Singer CLASS:PUBLIC DESCRIPTION:Speaker: NOAH G. SINGER\, Ph.D. Student\, Computer Science Depa rtment\,\nCarnegie Mellon University\n\nTalk Title: Expansion of coset com plexes and applications\n\nIn computer science and discrete mathematics\, a hypergraph is a\ncollection of subsets of a set of vertices\; in particu lar\, a graph is\na collection of (unordered) pairs of vertices. Graphs ar e used to\nencode pairwise relationships between objects\, and hypergraphs to\nencode more general multi-way relationships.\n\nHigh-dimensional expa nders are\, informally\, hypergraphs which are\n\"well-connected\" in a qu antitative sense. While expansion in the\n\"low-dimensional\" case of grap hs has been studied intensively since\nthe 1970s\, high-dimensional expand ers have recently gained visibility\nfor their role in a number of theoret ical breakthroughs\, such as the\nconstruction of efficient sampling algor ithms for spanning trees\n(Anari–Liu–Oveis Gharan–Vinzant\, STOC 201 9\, Ann. Math. 2024)\,\noptimal locally testable codes\n(Dinur–Evra–Li vne–Lubotzky–Mozes\, STOC 2022)\, and efficient\nlow-soundness PCPs (B afna–Minzer–Vyas\, STOC 2025).\n\nKaufman and Oppenheim (STOC 2018\, E ur. J. Comb. 2023) gave a\nremarkably simple construction of high-dimensio nal expanders by using\ncarefully chosen groups of matrices to instantiate a classical\nconstruction known as a \"coset complex\". In this thesis\, we further\ninvestigate the expansion of these complexes and various\ngene ralizations\, as well as applications of this expansion in computer\nscien ce and mathematics.\n\nIn two preliminary works (joint with Ryan O’Donne ll)\, we:\n\nInvestigated a particular notion of high-dimensional expansio n\n(\"1-cosystolic expansion\") on certain generalized KO complexes by\nco mbining intricate group-theoretic arguments with computer-assisted\nmatrix rank calculations.Showed that KO complexes have a\n\"low-soundness agreem ent testing\" property which allows them to be\nused inside the PCP of Baf na et al.\, replacing a much more complicated\nconstruction.\n\nIn this pr oposal\, we propose several additional directions for the\nPh.D. thesis. T hese include:\n\nUsing the KO complex to improve the complexity of the Baf na et al. PCP\n(e.g.\, the verifier or prover runtimes)\,systematically ch aracterizing\nthe coboundary and cosystolic expansion of generalizations o f KO\ncomplexes\; andimproving existing constructions of agreement testers by\nusing alternative kinds of tests.\n\nThesis Committee:\n\nRyan O'Donn ell (Chair)\n\nAayush Jain\n\nYang P. Liu\n\nIrit Dinur (Institute for Adv anced Study)\n\nMadhur Tulsiani (Toyota Technological Institute at Chicago &\nUniversity of Chicago)\n\nAdditional Information\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7a123 DTSTART;TZID=America/New_York:20260429T140000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260429T153000 LOCATION:Newell-Simon 1305 & Zoom SUMMARY:Doctoral Thesis Proposal - Zhengyao Lin CLASS:PUBLIC DESCRIPTION:Speaker: ZHENGYAO LIN\, Ph.D. Student\, Computer Science Depart ment\,\nCarnegie Mellon University\n\nTalk Title: Verifying Asynchronous D ataflow Compilers\n\nThe paradigm of asynchronous dataflow circuits\, in w hich parallel\noperators are dynamically scheduled and data-driven\, unloc ks\nsubstantial energy efficiency and performance gains in reconfigurable\ ndataflow architectures (RDAs) and dynamic high-level synthesis (HLS)\ntoo lchains. A key challenge hindering their mainstream adoption is the\ndiffi culty of correct\, efficient\, and general-purpose compilation\ntowards as ynchronous dataflow.\n\nIn this proposal\, I present my efforts to apply f ormal verification to\nasynchronous dataflow\, with the goal of developing an end-to-end\,\nprovably correct dataflow compilation pipeline.\n\nThesi s Committee:\n\nBryan Parno (Chair)\n\nStephanie Balzer\n\nRuben Martins\n \nBrandon Lucia\n\nMilijana Surbatovich (University of Maryland\, College Park)\n\nAdditional Information\n\nIn-person and Zoom\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7a4e7 DTSTART;TZID=America/New_York:20260428T120000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260428T133000 LOCATION:Newell-Simon Hall 3002 & Zoom SUMMARY:Doctoral Thesis Proposal - Lingjing Kong CLASS:PUBLIC DESCRIPTION:Speaker: LINGJING KONG\, Ph.D. Student\, Computer Science Depar tment\,\nCarnegie Mellon University\n\nTalk Title: Causal AI for Transfera ble\, Interpretable\, and\nControllable Machine Learning\n\nFoundation mod els are rapidly becoming capable assistants for\nknowledge work\, but thei r deployment in real settings is limited by\nthree gaps: they do not trans fer reliably across environments\, their\ninternal reasoning is opaque\, a nd their behavior is hard to control\nprecisely. In this talk\, I argue th at these limitations are not only\nabout model size — they are fundament ally about whether learning\ncaptures and leverages the underlying structu re of the data-generating\nprocess. I use causal thinking as a practical l ens to model what is\ninvariant\, what changes\, and what can be intervene d on\, and I further\nshow how this leads to learning principles that impr ove\ntrustworthiness. I will first present methods for learning unifying\n mechanisms from heterogeneous data\, across domains and modalities\, to\ne nable reliable transfer and controllable generation. Next\, I will\nshow h ow structured concepts can be recovered even from seemingly\nunstructured data\, by analyzing and improving self-supervised\nobjectives (such as mas king and diffusion) through hierarchical\nlatent-variable models. These co ncept structures can then be used to\ninterpret generative models and supp ort targeted\, multi-level edits.\nFinally\, I connect these two threads t o generalization beyond the\ntraining distribution. I will discuss natural conditions for\nextrapolation and a compositional generation framework th at improves\nprompt following for novel concept combinations. I will concl ude with\na brief outlook on self-improving world models.\n\nThesis Commit tee:\n\nKun Zhang (Co-chair)\n\nYuejie Chi (Co-chair)\n\nEric Xing (Co-cha ir)\n\nTom Mitchell\n\nKevin Murphy (Google DeepMind)\n\nAdditional Inform ation \n\nIn-person and Zoom \n\n \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7a955 DTSTART;TZID=America/New_York:20260427T120000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260427T133000 LOCATION:Gates and Hillman Centers SUMMARY:Doctoral Thesis Proposal - Kevin Kuo CLASS:PUBLIC DESCRIPTION:Speaker: KEVIN KUO\, Ph.D. Student\, Computer Science Departmen t\,\nCarnegie Mellon University\n\nTalk Title: Algorithms for Efficient an d Safe Collaborative Learning\nSystems\n\nData for AI systems is becoming increasingly sparse. Within a decade\,\nLLMs are projected to be trained o n datasets the size of the total\nstock of public human data\, while indiv iduals and organizations are\nincreasingly restricting access to their dat a due to economic and\nprivacy concerns. Collaborative learning has the po tential to fuel\ndata-hungry AI systems by enabling access to restricted s ources of\ndata---but only if it can provide meaningful guarantees regardi ng data\nprivacy\, quality of service\, and computational cost. This thesi s\nstudies three unique ML system architectures that offer data\nprotectio n by design: (1) multi-round federated learning\, (2) model\nmerging-and-l ocalization\, and (3) proxy tuning. We leverage principles\nfrom model com pression and transfer learning to improve the utility\,\nefficiency\, and privacy guarantees of these frameworks.\n\nThesis Committee:\n\nVirginia S mith (Chair)\n\nAditi Raghunathan\n\nGauri Joshi\n\nHolger Roth (NVIDIA)\n \nAdditional Information\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7ad8f DTSTART;TZID=America/New_York:20260424T143000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260424T160000 LOCATION:Gates and Hillman Centers SUMMARY:Doctoral Thesis Proposal - Sagar Bharadwaj Kalasibail Seetharam CLASS:PUBLIC DESCRIPTION:Speaker: SAGAR BHARADWAJ KALASIBAIL SEETHARAM\, Ph.D. Student\, Computer\nScience Department\, Carnegie Mellon University\n\nTalk Title: OpenFLAME: Federated Spatial Intelligence\n\nSpatial applications\, i.e.\, applications that tie digital information\nwith the physical world\, have improved many of our daily activities\,\nsuch as navigation and ride-shar ing. This class of applications also\nholds significant promise of enablin g new industries such as augmented\nreality and robotics. The development of these applications is enabled\nby spatial intelligence systems\, or sy stems that can provide\nphysically-grounded services such as routing\, sp atial search\, and\nlocalization. Today\, mapping platforms provided by or ganizations like\nGoogle and Apple serve as spatial intelligence systems. These maps are\ncentralized and primarily cover outdoor spaces. We envisio n that\nfuture spatial applications\, such as persistent world-scale augme nted\nreality and robotics\, would require detailed and precise spatial\n intelligence across indoor and outdoor spaces. The scale of\ncartography e fforts required to survey indoor spaces and their privacy\nneeds inhibit e xisting centralized maps from incorporating such spaces\ninto their platfo rm.\n\nThis thesis proposes the design and implementation of OpenFLAME\, a \nfederated spatial intelligence platform built on two core pillars.\nFirs t\, it introduces a federated mapping infrastructure where\nindependent pa rties can manage and serve their own maps of physical\nregions. This unloc ks scalability of map management\, isolation\, and\nprivacy of maps. This is implemented on top of the existing Domain\nName System (DNS)\, which e nables us to leverage its existing\ninfrastructure. Second\, it explores t he development of spatial\nservices\, such as search\, routing\, and local ization\, by transforming\nraw spatial data (e.g.\, images and videos) of a space into structured\,\nqueryable maps that support these capabilities. \n\nThesis Committee:\n\nSrinivasan Seshan (Co-Chair)\n\nAnthony Rowe (Co- Chair)\n\nJustine Sherry\n\nHari Balakrishnan (Massachusetts Institute of Technology)\n\nAdditional Information\n\nIn-person & Zoom \n\n \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7b288 DTSTART;TZID=America/New_York:20260420T130000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260420T143000 LOCATION:Gates Hillman 5117 SUMMARY:Doctoral Thesis Proposal - Zhibo Chen CLASS:PUBLIC DESCRIPTION:Speaker: ZHIBO CHEN\, Ph.D. Student\nComputer Science Departmen t\nCarnegie Mellon University\n\nTalk Title: CoLF - A Coinductive Logical Framework\n\nThe LF logical framework represents judgments as types\, and objects\nand derivations as finitary terms. Twelf\, an implementation of L F\, is\na metalogical framework that incorporates metatheorem checking and a\nlogic programming engine. There is no direct encoding of infinitary\no bjects and derivations in LF and Twelf. In this thesis\, we propose a\nnew logical framework CoLF\, building on top of LF\, for encoding\ninfinitary objects and derivations as infinitary terms. We develop\nthe type theory and implementation of CoLF. We also propose to\ninvestigate the metatheor etic reasoning principles and a new logic\nprogramming semantics in the pr esence of infinitary terms.\n\nThesis Committee\n\nFrank Pfenning (Chair)\ n\nKarl Crary\n\nIliano Cervesato\n\nAlberto Momigliano (University of Mi lan)\n\nAdditional Information \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7b66e DTSTART;TZID=America/New_York:20260408T084500 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260408T101500 LOCATION:Reddy Conference Room\, Gates Hillman 4405 SUMMARY:Doctoral Thesis Proposal - Bernardo Subercaseaux CLASS:PUBLIC DESCRIPTION:Speaker: BERNARDO SUBERCASEAUX\, Ph.D. Student\nComputer Scienc e Department\nCarnegie Mellon University\n\nTalk Title: SAT Encodings: Fro m Art to Science\n\nAutomated reasoning engines\, and SAT solvers in parti cular\, have\nbecome a powerful tool for tackling hard combinatorial probl ems. While\nSAT solvers have improved dramatically\, their effectiveness s till\ndepends critically on how problems are encoded into conjunctive norm al\nform (CNF). Encoding choices routinely account for runtime differences \nof several orders of magnitude\, yet their design remains more art than\ nscience—guided by intuition and hard-won experience rather than a\nprin cipled theory. This thesis aims to shed light on the design of\neffective SAT encodings\, from both practical and theoretical\nperspectives.\n\nThe first part is dedicated to the art of encodings. We show how\nclever probl em-specific encodings\, together with other automated\nreasoning technique s\, have allowed us to solve a variety of open\nproblems in discrete mathe matics ranging from graph coloring to\ndiscrete geometry. These encodings benefit from mathematical insights\nincorporated via additional constraint s or auxiliary variables that\nrepresent semantically important aspects of the problem. Notably\, some\nof these insights are themselves inspired by computational\nexperiments\, establishing a symbiotic relationship betwee n automated\nreasoning and discrete mathematics. We also apply this art to \ncomputational problems in explainable AI—uncovering patterns in\ndecis ion trees\, nearest-neighbor classifiers\, and other symbolic\nmodels—de monstrating the transferability of our techniques beyond\nmathematics.\n\n The second part is dedicated to the foundations of a science of\nencodings . We present a landscape of theoretical results regarding the\nnumber of c lauses and auxiliary variables required to encode several\nbuilding blocks of propositional encodings\, from cardinality\nconstraints to arbitrary k -CNF functions. We posit that encoding\nboolean functions into CNF with as few clauses as possible offers a\nfascinating yet largely unexplored terr itory for circuit complexity.\nBy leveraging auxiliary variables and wide clauses\, this\nclause-minimization model permits rich combinatorial struc tures that\nsurpass known lower bounds for circuits. Furthermore\, while\n clause-minimization does not always correlate with solver performance\,\nt heoretical developments in this model have led us to novel encodings\nthat run faster on practical problems. More broadly\, this thesis aims\nto est ablish that the clause-minimization model is not only an elegant\ntheory\, but also a realistic path towards empirical speedups.\n\nThesis Committee \n\nMarijn Heule (Chair)\n\nJeremy Avigad\n\nRuben Martins\n\nStefan Szeid er (Technische Universität Wien)\n\nRyan Williams (Massachusetts Institu te of Technology)\n\nAdditional Information \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7bba1 DTSTART;TZID=America/New_York:20260403T130000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260403T143000 LOCATION:Newell-Simon 3002 SUMMARY:Doctoral Thesis Proposal - Andrew Park CLASS:PUBLIC DESCRIPTION:Speaker: ANDREW PARK\, Ph.D. Student\nComputer Science Departme nt\nCarnegie Mellon University\n\nTalk Title: Attacking and Designing Secu re Protocols for Database\nSearch\n\nThe increasing reliance on outsourced storage and cloud-based\ncomputing has made database accesses a fundament al problem in modern\nsecurity and cryptography. At its core\, the challen ge of accessing\ndatabases securely is to enable efficient query processin g over a\n(potentially encrypted) database without leaking private informa tion\nto untrusted parties. Large lines of work have yielded a plethora of \ndifferent solutions such as searchable encryption\, private information\ nretrieval (PIR)\, and oblivious RAM (ORAM)\, each offering various\ntrade offs among efficiency\, functionality\, and privacy. However\, these\nsolu tions have yet to find wide-scale adoption due to practical\ninefficiencie s. In addition\, their real-world implementations often\ncontain subtle le akage of the underlying private data.\n\nThis dissertation develops a unif ied perspective on secure database\nsearch by studying both attacks and de signs of new secure protocols\nfor database search. On the attack side\, w e design and implement a\nframework\, Polysys\, for modeling and analyzing leakage patterns. This\nresult demonstrates an empirical understanding of how theoretical\nprivacy guarantees behave in practice.\n\nOn the constru ction side\, we introduce new protocols for both PIR and\nORAM to motivate more real-world adoption of these protocols. For PIR\,\nwe design novel c ommunication-efficient\, fault-tolerant multi-server\nschemes that also su pport erasure-coded storage\, providing robustness\nagainst fail-stop or B yzantine servers. For ORAM\, we present two new\ndesigns for different wor kload settings. First\, we design a garbled\nRAM (GRAM) scheme which match es the interactive state of the art\nscheme and achieves practical improve ment against the prior state of\nart. Finally\, we propose to construct di stribution-aware ORAM schemes\,\nwhich provides ORAM-like security propert ies for a set distribution\nwhile providing better practical efficiency.\n \nOur results highlight the importance of accounting for leakage in\nreal- world settings and considering real-world limitations when\ndesigning secu re protocols.\n\nThesis Committee\n\nElaine Shi (Co-chair)\n\nWenting Zhen g (Co-chair)\n\nAayush Jain\n\nSeny Kamara (MongoDB)\n\nTarik Moataz (Mong oDB)\n\nAdditional Information \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7c0dc DTSTART;TZID=America/New_York:20260311T123000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260311T140000 LOCATION:Newell-Simon 4201 and Zoom SUMMARY:Doctoral Thesis Proposal - Yonghao Zhuang CLASS:PUBLIC DESCRIPTION:Speaker: YONGHAO ZHUANG\, Ph.D. Student\nComputer Science Depar tment\nCarnegie Mellon University\n\nTalk Title: On Efficient Language Mod el Post Training with Attention\nDisaggregation\n\nToday's LLM training in troduces more stages to further improve the\nmodel quality\, and post-trai ning is the most important. Despite the\nlong-context workload imbalance\, post-training includes reinforcement\nlearning (RL)\, which iteratively r uns the \"rollout generation - reward\nevaluation - policy update'' pipeli ne.\n\nThis thesis proposes the concept of attention server\, where the ma in\npart of attention (core attention) is disaggregated from other\ncompon ents of the model\, and is handled by an independent cluster of\nGPUs. The first benefit of the disaggregation is independent scaling\,\nenabling a higher batch size of other components\; Besides\, the core\nattention kern el only needs a subset of the GPU resources to saturate\nits memory bandwi dth demand\, allowing the GPU to utilize the remaining\nresources for comp ute intensive tasks.\n\nThesis Committee\n\nEric Xing (Chair)\n\nTianqi Ch en\n\nZhihao Jia\n\nIon Stoica (University of California\, Berkeley)\n\nHa o Zhang (University of California\, San Diego)\n\nAdditional Information\n \nIn Person and Zoom Participation.  See announcement. \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7c53f DTSTART;TZID=America/New_York:20260226T140000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260226T153000 LOCATION:Reddy Conference Room\, Gates HIllman 4405 and Zoom SUMMARY:Doctoral Thesis Proposal - Sam Arch CLASS:PUBLIC DESCRIPTION:Speaker: SAM ARCH\, Ph.D. Student\nComputer Science Department\ nCarnegie Mellon University\n\nTalk Title: Leveraging Optimization-Enablin g Properties of\nUser-Defined Functions for Efficient Database Query Execu tion\n\nAfter decades of research\, analytical database management systems \n(DBMSs) have become remarkably effective at optimizing and executing\nSQ L queries. However\, many users write queries that are not written\nentire ly in SQL. Instead\, these queries invoke user-defined functions\n(UDFs)\, external functions written in non-SQL programming languages\nsuch as Pyth on or PL/SQL. UDFs provide software engineering benefits\nby enabling code reuse and by extending the DBMS’s capabilities to\ninclude those of the UDF language. However\, UDFs are inherently\nnon-relational\, which makes them challenging for DBMSs to reason about\nand execute efficiently. Effe ctive optimization is also challenging\nbecause UDF languages are Turing-c omplete\, allowing UDFs to be\narbitrarily complex. Although general-purpo se optimization techniques\ncan improve UDF performance (e.g.\, compilatio n and batching)\, they\ntarget arbitrary UDF code and therefore have limit ed effectiveness. We\nobserve that the most beneficial UDF optimizations ( e.g.\, memoization\nand inlining) leverage key optimization-enabling prope rties of UDFs\n(i.e.\, how users actually use them in practice).\n\nIn thi s proposal\, we present multiple techniques that leverage\noptimization-en abling properties of UDFs to improve database query\nexecution performance . First\, we observe that inlining only the\nrelevant pieces of a UDF impr oves performance\, and leverage UDF\ndecomposability to break UDFs into pi eces and hide irrelevant pieces\nthrough outlining. Next\, we observe that processing all unique UDF\ninputs simultaneously improves parallelism\, a nd leverage UDF\nredundancy to build lightweight indexes during query proc essing to\navoid repeated UDF invocations.\n\nWe propose extending our pre liminary work by observing that enabling\ninter-tuple parallelism of UDFs improves query execution performance.\nWe plan to leverage UDF pipelining\ , the observation that UDFs operate\nas a pipeline of data transformations over their inputs\, to enable\nfusion and auto-vectorization of pipeline stages. Collectively\, the\ntechniques presented in this dissertation will enable an analytical\ndatabase system to execute queries that contain UDF calls efficiently.\n\nThesis Committee\n\nAndrew Pavlo (Co-Chair)\n\nTodd C. Mowry (Co-Chair)\n\nJignesh Patel (Co-Chair)\n\nPhillip B. Gibbons\n\n Joseph M. Hellerstein (University of California\, Berkeley)\n\nAdditional Information\n\nIn Person and Zoom Participation.  See announcement. \n\n  \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7ca60 DTSTART;TZID=America/New_York:20260213T153000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260213T170000 LOCATION:Gates Hillman 9115 and Zoom SUMMARY:Doctoral Thesis Proposal - Yash Savani CLASS:PUBLIC DESCRIPTION:Speaker: YASH SAVANI\, Ph.D. Student\nComputer Science Departme nt\nCarnegie Mellon University\n\nTalk Title: Controlled Generation of Fou ndation Models for Training\n\nThis thesis proposal presents controlled ge neration methods for\nfoundation models\, focusing on gradient-based steer ing to improve\ntraining and robustness. For diffusion and flow models\, I introduce\nDiffusing Differentiable Representations (NeurIPS 2024)\, whic h guides\nthe training of differentiable representations\, such as Neural\ nRadiance Fields\, by pulling back the score function through the\ndiffere ntiable render function. I also present work with Adobe\nResearch on tempo ral credit assignment for policy gradient methods\,\nenabling more effecti ve training of flow models via GRPO-style\nreinforcement learning. \n\nFo r large language models\, I present two methods for controlled\ngeneration . The first maximizes resource utilization in GRPO-style\nreinforcement le arning by selectively dropping low-variance\ntrajectories (in submission). The second\, Antidistillation Sampling\n(NeurIPS 2025)\, steers generatio n to defend against distillation\nattacks using precomputed proxy gradient s. Together\, these\ncontributions establish a unified framework for contr olled generation\nacross modalities\, with applications spanning creative content\nsynthesis\, model protection\, and efficient training.\n\nThesis Committee\n\nJ. Zico Kolter (Chair)\n\nAviral Kumar\n\nNicholas M. Boffi\n \nKrishna Kumar Singh (Adobe Research)\n\nAdditional Information\n\nIn Per son and Zoom Participation.  See announcement. \n\n \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7cec7 DTSTART;TZID=America/New_York:20260123T100000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260123T113000 LOCATION:Gates and Hillman Centers SUMMARY:Doctoral Thesis Proposal - Joshua Clune CLASS:PUBLIC DESCRIPTION:Speaker: JOSHUA CLUNE\, Ph.D. Student\, Computer Science Depart ment\,\nCarnegie Mellon University\n\nTalk Title: Leveraging Automated The orem Provers for Lean Proof\nAutomationThis proposal discusses work that b uilds towards the\ncreation of a hammer for the Lean interactive theorem p rover. Said\nwork includes the development of a proof-producing superposit ion\ntheorem prover for Lean\, a tool which interfaces with the cvc5 SMT\n solver to produce self-contained Lean proof scripts\, and a neural\npremis e selection system. The proposal culminates in the description\nof a preli minary hammer for Lean along with discussion of how to\nrefine and improve it into a more powerful and robust tool.\n\nThesis Committee:\n\nJeremy A vigad (Chair)\n\nMarijn Heule\n\nBryan Parno\n\nHaniel Barbosa (Universid ade Federal de Minas Gerais)\n\nIn-person and Zoom\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7d294 DTSTART;TZID=America/New_York:20260112T093000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20260112T110000 LOCATION:Gates and Hillman Centers SUMMARY:Doctoral Thesis Proposal - Zhihao Zhang CLASS:PUBLIC DESCRIPTION:Speaker: ZHIHAO ZHANG\, Ph.D. Student\, Computer Science Depart ment\,\nCarnegie Mellon University\n\nTalk Title: A Path Towards Efficient Large Language Model Deployment\nthrough Algorithm and System Co-Design\n \nRecent advancements in large language models have shown promising\nresul ts in diverse downstream tasks by training and test time scaling.\nHowever \, the fast-paced development of large models has posed\nsignificant chall enges to their energy cost and efficient\ndeployment. \n\nTo achieve this \, my thesis topic is centered around bridging the gap\nbetween the algori thm-system co-design space for better large model\ndeployment. More specif ically\, through:\n\nhardware-guided algorithmic explorations for efficien t large language\nmodel inference\, and LLM inference-specific system opt imizations to\nfully exploit hardware utilization. \n\nFor algorithmic im provements\, I will present two lines of research\nprojects on Speculative Decoding (SpecInfer\, RaLMSpec) and Sparse\nAttention (TidalDecode\, Less isMore).\n\nFor system optimizations\, I will present one project on LLM d eployment\nwith MegaKernel (MPK) and one ongoing project that is focusing on\ngeneralizing the megakernel runtime to support multi-LLM\ndeployment.  \n\nBenefiting from the algorithm-system co-optimizations\, the proposed \nthesis topic is expected to provide an effective solution for reducing\n the energy cost and improving the efficiency of LLM deployment in the\nrea l world.\n\nThesis Committee\n\nZhihao Jia (Chair)\n\nTianqi Chen\n\nDimit rios Skarlatos\n\nRavi Netravali (Princeton University)\n\nAdditional Info rmation\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7d73a DTSTART;TZID=America/New_York:20251208T123000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20251208T140000 LOCATION:Reddy Conference Room\, Gates Hillman 4405 SUMMARY:Doctoral Thesis Proposal - Myra Dotzel CLASS:PUBLIC DESCRIPTION:Speaker: MYRA DOTZEL\, Ph.D. Student\nComputer Science Departme nt\nCarnegie Mellon University\n\nTalk Title: Logical Foundations of Inter mittent Computing\n\nIntermittent computing is gaining popularity in appli cations that rely\non batteryless energy-harvesting devices which experien ce frequent and\narbitrary power failures. To enable correct program re-ex ecution\ndespite these potentially frequent and arbitrary power failures\, \nruntime support is needed to save and restore necessary state. \n\nIn t his talk\, we study the formal foundations of intermittent\ncomputing by u se of type systems to guarantee the correctness of\nprograms prior to thei r deployment\, and runtime systems to facilitate\ncorrect program executio n\, including support for sequential and\nconcurrent models of execution.  \n\nFirst\, we explore the logical underpinning of sequential\, intermit tent\ncomputing and model checkpoint\, crash\, restore\, and re-execution\ noperations as computation on crash types. We draw inspiration from\nadjoi nt logic to reason about the relationship between persistent and\ntransien t memories through (re-)execution\, checkpointing\, and\nrestoration. Usin g crash types\, we show that any correct intermittent\nexecution can be si mulated by a continuously-powered execution.\n\nSecond\, we present the fi rst provably-correct system for concurrent\,\nintermittent program executi on\, which is needed as many embedded\napplications rely on interactions w ith hardware-triggered interrupts\nand accesses to shared memory. Prior wo rk on concurrent\, intermittent\nexecution has only provided restrictive p rogramming models with no\nformal correctness guarantees. In this talk\, w e present a co-designed\nruntime system and type system that together supp ort the provably\ncorrect intermittent execution of task-based concurrent programs with\nshared memory. This system promotes a more flexible program ming model\nand supports a broader spectrum of task re-execution behaviors than is\nconsidered by prior work. We provide the first formal definition and\nproofs of correctness for concurrent\, intermittent execution.    \n\nThesis Committee\n\nLimin Jia (Co-chair)\n\nFarzaneh Derakhshan (Co-ch air\, Illinois Institute of Technology)\n\nFrank Pfenning \n\nJan Hoffman n \n\nBrigitte Pientka (McGill University) \n\n \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7dc40 DTSTART;TZID=America/New_York:20251202T100000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20251202T113000 LOCATION:Traffic21 Classroom\, Gates Hillman 6501 SUMMARY:Doctoral Thesis Proposal - Kaiyang Zhao CLASS:PUBLIC DESCRIPTION:Speaker: KAIYANG ZHAO\, Ph.D. Student\nComputer Science Departm ent\nCarnegie Mellon University\n\nTalk Title: Architecting Memory Efficie ncy in Modern Datacenters\n\nThe proliferation of memory-intensive applica tions\, the rapid\nexpansion of memory capacity to terabyte scales\, and t he slowing of\nDRAM cost scaling have established memory as the critical b ottleneck\nin modern datacenter computing. This inefficiency manifests in two\ndimensions: the cycle efficiency lost to the virtual memory\nabstract ion and the escalating financial cost of memory.\n\nFirst\, the virtual me mory abstraction is under increasing strain. As\nmemory capacity grows whi le Translation Lookaside Buffer sizes remain\nstagnant\, address translati on overhead becomes severe\; internal\nprofiling at hyperscalers reveals t hat approximately 20% of CPU cycles\nare stalled on TLB misses. This overh ead is bound to worsen due to\ninherent TLB scaling limits\, the introduct ion of additional page table\nlevels\, vast heterogeneous memory capacity\ , and the page-level\nsecurity checks required by confidential computing. Second\, the\nfinancial cost of memory has skyrocketed. Memory now account s for\nnearly a quarter of rack power consumption and half of the Total Co st\nof Ownership of a typical datacenter server. In this proposal\, I\nadd ress these challenges through a set of operating system and\narchitectural designs.\n\nTo improve cycle efficiency\, I present two completed works.\ nContiguitas creates abundant physical memory contiguity by grouping\nunmo vable allocations in the OS and introducing hardware extensions to\nmigrat e pages previously locked for device I/O. This contiguity is\nleveraged to allocate huge pages\, reducing translation overhead and\nyielding up to 1 8% performance improvement for production workloads.\nLearned Virtual Memo ry (LVM) replaces rigid radix page tables with\nlearned indexes tailored t o the application's virtual address space.\nBy leveraging address space re gularity\, LVM reduces page walk overhead\nby an average of 44% and achiev es a 2–27% speedup in execution.\n\nTo improve cost efficiency\, I prese nt two ongoing works. Multi-Tier\ndynamically manages pages across DRAM\, CXL memory\, and SSDs to\nmaximize financial savings by utilizing cheaper tiers within a defined\nperformance loss limit. Equilibria addresses the c hallenges of\nmulti-tenant tiering\, ensuring fair memory sharing and miti gating\nnoisy-neighbor interference through flexible placement policies an d\nthrashing mitigation.\n\nTogether\, these works provide a comprehensive solution to improving\nmemory efficiency in datacenters from the perspect ives of both cycle\noverhead and financial cost.\n\nThesis Committee\n\nDi mitrios Skarlatos (Chair)\n\nPhil Gibbons\n\nTodd Mowry \n\nKim Keeton (G oogle) \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7e17c DTSTART;TZID=America/New_York:20251120T090000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20251120T103000 LOCATION:Gates Hillman 8102 and Zoom SUMMARY:Doctoral Thesis Proposal - Cayden Codel CLASS:PUBLIC DESCRIPTION:Speaker: CAYDEN CODEL\, Ph.D. Student\nComputer Science Departm ent\nCarnegie Mellon University\n\nTalk Title: Building a Verified SAT Too lchain in Trestle\n\nAutomated reasoning (AR) tools are versatile and prac tically efficient\npieces of software that can solve a wide variety of pro blems in\nindustry and academia. One of their strengths is their ability t o\ngenerate proofs checkable by verified software. Even if the AR tools\nt hemselves contain bugs (and they often do)\, we can still have a high\ndeg ree of confidence in the correctness of their answers.\n\nHowever\, this v erified toolchain can be extended further to include\nencodings. Usually\, AR tools solve problems that have been encoded\ninto a form that they can understand. This process of encoding can\nintroduce bugs\, meaning that t he encoded form of the problem no longer\naccurately represents the origin al. Bugs are more likely to appear\nwhen the encoding is more complicated\ , such as when auxiliary logical\nobjects are introduced in order to make the encoding smaller or easier\nfor the AR tool to manipulate. Unfortunate ly\, complicated encodings\nare becoming increasingly necessary in order t o push the boundaries of\nwhat problems AR tools can solve. As a result\, we argue that the\nstandard AR toolchain should now include verified encod ings by\ndefault.\n\nIn this thesis\, we will develop an end-to-end verifi ed toolchain for\nthe boolean satisfiability problem (SAT) in the Trestle project.\nTrestle currently has a verified SAT proof checker and good supp ort\nfor writing verified encodings\, but its encoding tools are complicat ed\nand hard to use\, and only a handful of encodings have been verified s o\nfar. As a result\, we plan to redesign how encodings are written in\nTr estle\, and to verify new encodings. We also plan to add\nsymmetry-breakin g reasoning to Trestle and add features to enable\nend-to-end theorem prov ing with the use of SAT solvers.\n\nThesis Committee\n\nMarijn Heule (Chai r)\n\nJeremy Avigad\n\nBryan Parno\n\nBenjamin Kiesl-Reiter (Amazon Web Se rvices)\n\nAdditional Information\n\nIn Person and Zoom Participation.  S ee announcement. \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7e632 DTSTART;TZID=America/New_York:20251022T120000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20251022T133000 LOCATION:Reddy Conference Room\, Gates Hillman 4405 SUMMARY:Doctoral Thesis Proposal - Saranya Vijayakumar CLASS:PUBLIC DESCRIPTION:Speaker: SARANYA VIJAYAKUMAR\, Ph.D. Student\nComputer Science Department\nCarnegie Mellon University\n\nTalk Title: Protection Boundary Integrity: Detecting and Preventing\nSecurity Failures Across Contexts\n\n Modern computational systems deploy technical guardrails to enforce\nsecur ity\, privacy\, and safety boundaries across increasingly complex\noperati onal contexts. While effective within their design contexts\,\nthese mecha nisms exhibit systematic vulnerabilities when systems\ntransition between different operational modes: across interaction\nmodalities\, through temp oral evolution\, or when integrating neural and\nsymbolic reasoning. This dissertation investigates where\, how\, and why\nsecurity mechanisms fail at these critical transitions.\n\nFirst\, I demonstrate patterns of bounda ry failure through empirical\nanalysis across multiple domains. My cross-m odal work evaluates such\nfailures in browser-agent safety auditing (Brows erART) and\nauthenticity detection of AI-generated code (CodeFusion). Thro ugh\nBrowserART\, I show that language models refusing harmful instruction s\nin chat interfaces pursue identical harmful behaviors when deployed as\ nbrowser agents\, despite identical safety training. Through CodeFusion\,\ nI analyze visual structure and semantic content\, demonstrating that\naut henticity boundaries require reasoning across representational\nmodalities . Second\, I identify temporal vulnerabilities that emerge\nwhen security mechanisms designed for static analysis cannot adapt to\nevolving threats. I demonstrate this through MalCentroid\, tracking\nmalware family evoluti on while maintaining robustness against\nadversarial obfuscation\, and thr ough graph-based fraud detection\nsystems identifying attack patterns emer ging across temporal\ntransaction sequences. Through TRACE\, I achieve suc cessful\nre-identification against Google's Topics API by exploiting\nvuln erabilities where privacy mechanisms protecting individual\nobservations f ail when adversaries analyze sequential behavioral\npatterns.\n\nFinally\, I introduce methods to bridge neural-symbolic security\nboundaries. Throu gh SMTLayer\, I integrate satisfiability solvers\ndirectly into neural arc hitectures\, achieving substantial data\nefficiency improvements while mai ntaining formal logical guarantees.\nIn my proposed work\, I introduce ver ifiable protection mechanisms for\nlanguage models through a game-theoreti c prover-verifier framework and\ndevelop multiplicative gating architectur es enabling efficient\nlearning of complex logical structures like XOR gat es that standard\narchitectures struggle to represent. This research provi des\nfoundations for building protection mechanisms that maintain integrit y\nacross the complex operational transitions required for safe\ndeploymen t of autonomous computational systems.\n\nThesis Committee\n\nChristos Fal outsos (Co-Chair)\n\nMatt Fredrikson (Co-Chair)\n\nSarah Cen\n\nMihai Chri stodorescu (Google Research)\n\nAdditional Information \n\n \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7ec23 DTSTART;TZID=America/New_York:20251010T083000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20251010T100000 LOCATION:Reddy Conference Room\, Gates Hillman 4405 SUMMARY:Doctoral Thesis Proposal - Nicole Feng CLASS:PUBLIC DESCRIPTION:Speaker: NICOLE FENG\, Ph.D. Student\nComputer Science Departme nt\nCarnegie Mellon University\n\nTalk Title: Robust Algorithms for Windin g Numbers and Signed Distance\n\nThis thesis presents robust algorithms fo r inside-outside computation\nand curve reconstruction (via winding number s) and signed distance\ncomputation. These algorithms make geometric infer ences from imperfect\ndata\, where such imperfect data includes noisy\, in complete\, or\ninaccurate observations or representations of shapes that r esult from\neither acquisition or authoring of geometry. A theme is that\n robustness and versatility can often be achieved by processing smooth\,\ng lobally-defined functions encoding the geometry of interest\, that are\nmo re amenable to robust computation than the original\, defective curve\nor surface. For both inside-outside and signed distance computation we\ncan u nlock further control over geometry and topology by processing\nhigher-ord er derivatives of these functions. In many cases\, we can\nalso re-cast ou r algorithms\, formulated in terms of smooth functions\,\nonto different d iscretizations and geometric data structures. Another\ntheme is that robus t reconstruction and robust signed distance\ncomputation are closely relat ed problems\; towards this end\, we provide\na formalization of their rela tionship that justifies the design of our\nalgorithms.\n\nThesis Committee \n\nKeenan Crane (Chair)\n\nIoannis Gkioulekas\n\nNancy Pollard \n\nChris Wojtan (Institute of Science and Technology Austria)\n\nAdditional Inform ation \n\n \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7f048 DTSTART;TZID=America/New_York:20251003T160000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20251003T173000 LOCATION:Newell-Simon 4305 and Zoom SUMMARY:Doctoral Thesis Proposal - Honghao Lin CLASS:PUBLIC DESCRIPTION:Speaker: HONGHAO LIN\, Ph.D. Student\nComputer Science Departme nt\nCarnegie Mellon University\n\nTalk Title: Advances in Algorithms for M assive Data: Optimal Bounds\,\nAdversarial Robustness\, and Data-Driven In sights\n\nWith the rapid growth of massive datasets in areas such as machi ne\nlearning and numerical linear algebra\, classical algorithms are often \nno longer feasible. In this thesis proposal\, we develop provably\neffic ient algorithms for various problems in these settings\, such as\nstreamin g and distributed model. Our contributions span three\ndirections:\n\nOpti mal Bounds. We introduce a general technique for lifting dimension\nlower bounds for real-valued linear sketches to polynomially bounded\ninteger in puts. This leads to the first optimal sketching lower bounds\nfor discrete data streams in fundamental problems such as frequency\nmoment approximat ion\, operator norm estimation\, and compressed\nsensing. Beyond this\, we also establish nearly-optimal bounds for a\nvariety of streaming and sket ching tasks\, including ℓ p subspace\nsketches for constant dimension d \, ℓ p regression in the\narbitrary-partition distributed model\, and graph problems such as\napproximating the minimum cut and constructing cut sparsifiers in\nbalanced directed graphs.Adversarial Robustness. While mo st streaming\nalgorithms are studied in static worst-case models\, many pr actical\nscenarios involve adaptive adversaries who generate inputs based on\nprevious outputs. We present the first adaptive attack against linear\ nsketches for ℓ p-estimation over turnstile integer streams.\nSpecifica lly\, we show that any linear streaming algorithm with\nsketching matrix A ∈ ℤrxn can be broken using only poly(r log n)\nqueries\, with high co nstant probability. This result highlights\nfundamental limits of robustne ss in adaptive streaming. Learning-based\nAlgorithms. Classical algorithms guarantee correctness in the worst\ncase but often ignore structure in re al-world data\, while machine\nlearning methods leverage structure but typ ically lack guarantees. We\ndesign learning-based algorithms that incorpor ate machine learning\npredictions to adapt to input distributions\, achiev ing faster\nruntimes\, reduced space\, or improved accuracy. Crucially\, t hese\nalgorithms retain rigorous worst-case guarantees even when the\npred ictions are imperfect\, bridging the gap between theory and\ndata-driven p ractice.  \n\nThesis Committee\n\nDavid P. Woodruff (Chair)\n\nYang P. L iu \n\nRichard Peng\n\nJelani Nelson (University of California\, Berkeley )\n\nIn Person and Zoom Participation.  See announcement. \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7f559 DTSTART;TZID=America/New_York:20250923T120000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250923T133000 LOCATION:Gates Hillman 8115 SUMMARY:Doctoral Thesis Proposal - William Zhang CLASS:PUBLIC DESCRIPTION:Speaker: WILLIAM ZHANG\, Ph.D. Student\nComputer Science Depart ment\nCarnegie Mellon University\n\nTalk Title: On Holistic Database Optim ization via Leveraging\nSimilarity Across Actions\, Workloads\, Configurat ions\, and Scenarios\n\nModern database management systems (DBMSs) have ev olved to support\nincreasingly sophisticated data-intensive applications\, at the cost of\nsubstantial complexity to configure them for two reasons. First\, DBMSs\nexpose a vast configuration space with trillions of possib ilities that\nencompass system knobs\, physical design (e.g.\, indexes)\, and query\noptions\, amongst others. Second\, these applications are const antly\nevolving with changes in data access patterns\, query types\, load\ nintensities\, hardware\, and data distributions that necessitate\ncontinu ous re-optimization.\n\nTo address these challenges\, decades of autonomou s DBMS optimization\nresearch have produced specialized tuning tools to as sist human\noperators. Deploying these tools involves a complex multi-step \nworkflow where an operator (1) observes the DBMS’s behavior\, (2)\nsel ects tools based on the objectives and their expertise\, (3)\nconfigures t hem with an isolated environment\, (4) orchestrates their\nexecution to ob tain recommendations\, and (5) reviews those\nrecommendations before deplo yment. This cumbersome process results in\nsuboptimal configurations and s low adaptation to evolving\napplications’ workloads due to isolated spec ialized tools\,\ninefficient reuse of prior tuning knowledge\, and the fal lible human\nfactor.\n\nThis proposal presents techniques for addressing t hose limitations\nwith similarity to enable holistic database optimization . First\, we\npresent a holistic tuning tool that optimizes multiple DBMS aspects\nsimultaneously by using action similarity to organize actions int o\nneighborhoods conducive to exploration. We then present a framework\nth at assists tuners in adapting to environment changes by leveraging\nworklo ad and configuration similarity to re-mix historical knowledge.\n\nWe prop ose to extend our preliminary work by transforming the\nhuman-centric tuni ng workflow into an agentic process through scenario\nsimilarity. We will first investigate contextualizing deployments and\ncreating semantic tool interfaces. We will then design an orchestrator\nthat learns to select and deploy relevant tuning tools to obtain\nvalidated recommendations. With t hese efforts\, the agentic process\nwill enable holistic DBMS optimization throughout its lifetime. \n\nThesis Committee:\n\nAndrew Pavlo (Chair)\n \nJignesh Patel \n\nVincent Conitzer \n\nImmanuel Trummer (Cornell Unive rsity)\n\nAdditional Information \n\n \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7fa86 DTSTART;TZID=America/New_York:20250912T150000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250912T163000 LOCATION:Newell-Simon 4305 and Zoom SUMMARY:Doctoral Thesis Proposal - Bailey Miller CLASS:PUBLIC DESCRIPTION:Speaker: BAILEY MILLER\, Ph.D. Student\nComputer Science Depart ment\nCarnegie Mellon University\n\nTalk Title: Stochastic Geometry Primit ives\n\nNumerical computing on complex geometry faces two core challenges: \nrepresenting geometry and performing computation on it.\nDiscretization —voxels\, meshes\, global solves—works until geometry\nis too detailed or uncertain to resolve. To overcome these\nlimitations\, we propose a co mplementary paradigm—stochastic graphics\nprimitives (SGPs)—that use r andomness to avoid discretization in\nboth representation and computation. \n\nFirst\, we’ll survey SGPs in graphics today: Monte Carlo rendering a s\nan algorithmic primitive that interacts with geometry via local\nquerie s\, and participating-media models as distributional\nrepresentations that replace explicit particle interactions with\nfree-flight sampling. Buildi ng on these ideas\, we’ll show how the\nsame principles extend beyond li ght transport to Monte Carlo PDE\nsolvers that handle a range of boundary conditions using only local\ngeometric queries\, and stochastic solid repr esentations that move past\nmicroparticle media to prior-free\, uncertaint y-aware geometry. These\nprimitives are modular and differentiable\, enabl ing inverse\nreconstruction and optimization-driven shape design without r emeshing.\n\nCrucially\, we’ll position these methods as general-purpose \nprimitives: black-box operators for physics simulation (elliptic and\ntr ansport PDEs)\, geometric computation (harmonic coordinates\,\ndistance-dr iven queries\, shape optimization)\, and machine learning\n(differentiable PDE layers or neural PDE surrogates supervised by\nstochastic operators). In this view\, SGPs provide a common API in\nplace of meshes and global s olves\, so the same primitives serve\nsimulation\, geometry processing\, a nd learning.\n\nFinally\, we’ll outline current limits—hyperbolic and nonlinear\nPDEs—and a path forward via hybrid neural–Monte Carlo metho ds that\niteratively refine a neural surrogate under supervision while\npr eserving the geometric scalability and robustness of Monte Carlo PDE\nsolv ers. I’ll close with practical\, more expressive stochastic\nsurface mod els and a roadmap toward more general-purpose SGPs.\n\nThesis Committee\n\ nIoannis Gkioulekas (Chair)\n\nKeenan Crane\n\nNicholas Boffi\n\nRavi Rama moorthi (University of California San Diego)\n\nMathieu Desbrun (École Po lytechnique / Inria Paris-Saclay)\n\nAdditional Information\n\nIn Person a nd Zoom Participation.  See announcement. \n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c7ffdc DTSTART;TZID=America/New_York:20250617T140000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250617T153000 LOCATION:ASA Conference Room\, Gates Hillman 6115 SUMMARY:Doctoral Thesis Proposal - Daiyaan Arfeen CLASS:PUBLIC DESCRIPTION:Speaker: DAIYAAN ARFEEN\, Ph.D. Student\, Computer Science Depa rtment\,\nCarnegie Mellon University\n\nTalk Title: Designing Scalable DNN Training Systems to Overcome\nAlgorithmic Constraints\n\nLLM training req uires massive amounts of compute due to large model\nand dataset sizes\, s o it is not unusual to train LLMs on tens or\nhundreds of thousands of GPU s to complete training in a reasonable\namount of time (days or weeks). Ho wever\, GPU failures (which are\ncommon at these scales) and data-dependen cies (introduced by the\ntraining algorithms) can lead to severe GPU under utilization.  \n\nIn this talk\, we present distributed LLM training sys tems which are\nefficient and fault-tolerant at these scales. We first pre sent\nNonuniform-tensor-parallelism (NTP)\, a technique which increases th e\nfault-tolerance of tensor-parallel training\, thereby reducing the\nbla st-radius of GPU failures. NTP enables scale-up training with\nlittle-to-n o loss in training efficiency from realistic rates of GPU\nfailures. Next we present PipeFill\, a system for recovering GPU\nutilization (lost due t o scale-out training) by filling pipeline\nbubbles with third-party latenc y-insensitive jobs. We will discuss how\nPipeFill could be extended to sup port filling pipeline bubbles with\nonline inference jobs\, which are late ncy-sensitive.\n\nThesis Committee\n\nGreg Ganger (Chair)\n\nZhihao Jia\n\ nPhillip B. Gibbons\n\nDheevatsa Mudigere (NVIDIA)\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c803db DTSTART;TZID=America/New_York:20250602T100000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250602T113000 LOCATION:Traffic21 Classroom\, Gates Hillman 6501 and Zoom SUMMARY:Doctoral Thesis Proposal - Margarida Ferreira CLASS:PUBLIC DESCRIPTION:Speaker: MARGARIDA FERREIRA\, Ph.D. Student\, Computer Science\ nDepartment\, Carnegie Mellon University\n\nTalk Title: Synthesis of State ful Programs from Execution Traces\n\nExecution traces are a valuable sour ce of information in modern\ncomputing systems. They are continuously coll ected and used for system\ndebugging\, monitoring\, and optimization. They capture behavior across\ndiverse scenarios\, from routine operations to e dge cases. This thesis\ninvestigates how execution traces can serve as spe cifications for\nprogram synthesis\, enabling reverse engineering and anal ysis of\ncomplex systems and automation of traditionally manual tasks with out\nexplicit user input.\n\nThis proposal presents three synthesis framew orks\, Abagnale\, Syren\,\nand HyGLAD\, that illustrate the challenges of this problem on multiple\napplications and how we overcome them. Abagnale reverse-engineers the\nbehavior of congestion control algorithms (CCAs) fr om network traces.\nNetwork traces contain no information about the implem entation of the\nCCA\, displaying only the effects of their executions in the network.\nThus\, Abagnale must simulate each candidate solution in the same\nnetwork conditions to assess if they exhibit the same behavior. To\ ncapture all different behaviors\, we work with traces showing hundreds\no f executions\, making trace filtering and parallelization paramount to\nAb agnale's viability. Syren allows users to generate arbitrary\nprograms fro m partial traces that contain some of the function calls\nmade by the prog ram. Syren uses optimizing rewrites to introduce\ncontrol flow in the prog ram. These optimizing rewrites track the data\nused in the functions visib le in the trace\, which is then used to\ngenerate function calls not visib le in the trace using an\nexample-based syntax-guided synthesizer. HyGLAD synthesizes\nregex-based anomaly filters that flag deviations from a syste m's\nexpected behavior from execution logs. In this case\, our goal is not \nto reverse-engineer the system itself but to synthesize a model of its\n execution.\n\nAs future work\, we propose to develop a fourth synthesis ap proach to\nautomate data-aware business processes. We will use logs collec ted\nfrom human-executed processes as traces and synthesize implementation s\nthat model the task logic\, filtering out inconsistencies and errors\nu navoidable in human-generated logs.\n\nThesis Committee\n\nRuben Martins ( Co-chair)\n\nInês Lynce (Co-Chair\, Instituto Superior Técnico)\n\nJusti ne Sherry\n\nFraser Brown\n\nJoão F. Ferreira (Instituto Superior Técnic o)\n\nNate Foster (Cornell University)\n\nAdditional Information\n\nIn Per son and Zoom Participation.  See announcement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c808c8 DTSTART;TZID=America/New_York:20250519T140000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250519T153000 LOCATION:Traffic21 Classroom\, Gates Hillman 6501 and Zoom SUMMARY:Doctoral Thesis Proposal - Alexander Koujianos Goldberg CLASS:PUBLIC DESCRIPTION:Speaker: ALEXANDER KOUJIANOS GOLDBERG\, Ph.D. Student\, Compute r Science\nDepartment\, Carnegie Mellon University\n\nTalk Title: Improvin g Decision-Making from Distributed Human\nEvaluations\n\nSocially importan t decisions—from scientific funding\, to college\nadmissions and job hir ing—rely on ratings or rankings supplied by\nmultiple human evaluators. These judgments are prone to noise\, bias\,\nand strategic manipulation\, and there is seldom an objective ground\ntruth against which to determine their quality. The goal of this\nthesis is to understand and mitigate such errors in distributed human\nevaluation in order to make better decisions . Towards this end\, we\nboth conduct controlled experiments in review pro cesses and\ndevelop principled algorithms with provable guarantees. \n\ nIn particular\, we conduct large-scale experiments at peer\nreview confe rences to expose sources of error in evaluation and\nidentify opportunitie s for improvement. Then\, we develop a method for\nselecting top candidat es on the basis of uncertain evaluations\,\nproviding a principled instant iation of a \"peer review lottery.\"\nFinally\, we design privacy-preserv ing algorithms for releasing\nanonymized time-series and graph data\, whic h can enable more\ntransparency into review processes while preserving par ticipant\nanonymity.\n\nThesis Committee\n\nGiulia Fanti (Co-chair)\n\nNih ar B. Shah (Co-chair)\n\nTom Mitchell\n\nJohn Ioannidis (Stanford Universi ty)\n\nAdditional Information\n\nIn Person and Zoom Participation.  See a nnouncement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c80d58 DTSTART;TZID=America/New_York:20250507T090000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250507T090000 LOCATION:Gates Hillman 8102 and Zoom SUMMARY:Doctoral Thesis Proposal - Mingkuan Xu CLASS:PUBLIC DESCRIPTION:Speaker: MINGKUAN XU\, Ph.D. Student\, Computer Science Departm ent \,\nCarnegie Mellon University\n\nTalk Title: Optimization and Simulat ion of Quantum Circuits\n\nOptimizing quantum circuits and simulating them at scale remain\ncritical bottlenecks: manual design of quantum circuit o ptimizations\nis labor-intensive and device-specific\, while simulators st ruggle with\nexponential resource costs. This thesis delivers tools to tac kle these\nchallenges. \n\nFirst\, I introduce Quartz\, a superoptimizer that automates the\ngeneration and verification of circuit transformations for arbitrary\nquantum gate sets. By systematically exploring small circu its and\nemploying an automated theorem prover (Z3)\, Quartz discovers bot h\nexpert-designed and novel optimizations\, outperforming hand-tuned\nopt imizers across various gate sets. \n\nNext\, I present Atlas\, a distribu ted GPU-based simulator that\nhierarchically partitions circuits to exploi t available data\nparallelism while minimizing communication costs\, runni ng over 2×\nfaster than state-of-the-art GPU simulators. Atlas minimizes\ ncommunication overhead via integer linear programming to allocate\n\"near by\" gates to \"nearby\" GPUs and maximizes throughput through\ndynamic pr ogramming for kernel scheduling. \n\nFinally\, I propose an initial forma l verification framework to certify\neach application of transformation-ba sed optimizers like Quartz\,\npaving the way for full correctness guarante es. Together\, these\ncontributions advance automated\, scalable\, and rel iable quantum\ncomputing workflows for emerging devices. \n\nThesis Commi ttee\n\nZhihao Jia (Co-chair)\n\nUmut A. Acar (Co-chair)\n\nRyan O'Donnell \n\nYongshan Ding (Yale University)\n\n \n\nAdditional Information\n\nIn Person and Zoom Participation.  See announcement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c811f9 DTSTART;TZID=America/New_York:20250418T110000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250418T123000 LOCATION:Traffic21 Classroom\, Gates Hillman 6501 and Zoom SUMMARY:Doctoral Thesis Proposal - Madhusudhan Reddy Pittu CLASS:PUBLIC DESCRIPTION:Speaker: MADHUSUDHAN REDDY PITTU\, Ph.D. Student\, Computer Sci ence\nDepartment\, Carnegie Mellon University\n\nTalk Title: Fairness\, Di versity\, Explainability\, and Robustness for\nAlgorithmic Decision-making \n\nFairness\, diversity\, explainability\, and robustness are key challen ges\nin computational decision-making\, impacting machine learning\, resou rce\nallocation\, and data analysis. Balancing these principles with\neffi ciency presents significant computational and structural\nchallenges. This proposal investigates algorithmic approaches for\ndiverse selection\, fai r allocation\, interpretable clustering\,\nconstrained subspace approximat ion\, and comparison-based optimization.\nTogether\, these directions cont ribute to more equitable\,\nrepresentative\, interpretable\, and robust al gorithmic decision-making\nunder structural and informational constraints.  \n\nThesis Committee\n\nDavid Woodruff (Chair)\n\nAnupam Gupta\n\nPrasad Tetali\n\nMohit Singh (Georgia Institute of Technology)\n\nOla Svensson ( EPFL)\n\nAdditional Information\n\nIn Person and Zoom Participation.  See announcement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c815ef DTSTART;TZID=America/New_York:20250417T140000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250417T153000 LOCATION:Gordon Bell Conference Room\, Gates Hillman 5117 SUMMARY:Doctoral Thesis Proposal - Shawn Chen CLASS:PUBLIC DESCRIPTION:Speaker: SHAWN SHUOSHUO CHEN\, Ph.D. Student\, Computer Science \nDepartment\, Carnegie Mellon University\n\nTalk Title: Reshaping Data Ce nter Networks with Reconfigurability\n\nData center networks are fundament al to cloud computing—they tightly\ncouple compute and storage with high bandwidth and low latency. The\ndemand for data center network bandwidth is continuously growing\,\ndriven by the proliferation of data-intensive a pplications like AI/ML\nand video streaming. However\, electrical packet s witches struggle to\ndeliver the total bandwidth required by the growing d emands because a\n“plateauing” Moore’s Law limits I/O density and hi gh-speed\nmemory capacity. Moreover\, the sheer scale of modern data cente r\nnetworks makes electrical packet-switched networks increasingly\nexpens ive and power-hungry. Reconfigurable optical switching\ntechnology is a pr omising alternative\, offering the potential for\nhigher bandwidth\, reduc ed energy consumption\, and runtime\nreconfigurability. Reconfigurable dat a center networks (RDCNs) combine\nthe benefits of both optical and packet switches to accommodate\ndiverse traffic patterns and enhance network per formance. \n\nThis thesis addresses the limitations of current network de signs in\nRDCNs by revisiting underlying assumptions and redesigning core\ nnetwork components\, focusing on transport\, traffic engineering\, and\nt opology. First\, we present Time-division TCP (TDTCP)\, a new transport\np rotocol that adapts to the fluctuating bandwidth and latency in\ndemand-ob livious RDCNs by maintaining independent network states for\neach time-div ision multiplexed path. Second\, we tackle traffic\nengineering in demand- aware RDCNs with approaches that help implement\ncomplex traffic engineeri ng solutions in switches with minimum\nprecision loss. Third\, we propose a flexible machine learning job\nscheduling mechanism for reconfigurable c lusters based on torus\ntopologies\, ensuring optimal job performance whil e mitigating resource\nfragmentation. Together\, these innovations aim to unlock the full\npotential of RDCNs\, achieving higher performance\, cost- efficiency\, and\nscalability for future data center workloads. \n\nThesi s Committee\n\nSrinivasan Seshan (Chair)\n\nPeter Steenkiste\n\nTim Dettme rs\n\nMinlan Yu (Harvard University)\n\nAdditional Information\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c81adf DTSTART;TZID=America/New_York:20250408T113000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250408T130000 LOCATION:Gates Hillman 6115 SUMMARY:Doctoral Thesis Proposal - Wan Shen Lim CLASS:PUBLIC DESCRIPTION:Speaker: WAN SHEN LIM\, Ph.D. Student\, Computer Science Depart ment\,\nCarnegie Mellon University\n\nTalk Title: Database Gyms: Towards A utonomous Database Tuning\n\nDatabase management systems (DBMSs) are the f oundation of modern\ndata-intensive applications. But as more features are developed to\nsupport new workloads\, they become increasingly complex an d difficult\nto configure. Decades of research on autonomous DBMS configur ation\nhave largely produced advisory tools that still rely on human\nexpe rtise for their deployment into database tuning pipelines. Using\nthese to ols involves a multi-step process where a human operator (1)\ndetermines a n optimization objective\, (2) selects a suitable tool to\nimprove the obj ective\, (3) sets up and configures the DBMS to run a\nparticular workload \, (4) runs the workload to collect telemetry\, (5)\nuses the collected te lemetry to calibrate the tool\, and (6) operates\nthe tool to obtain recom mendations\, which the operator must then\nreview and apply. Because of th e ad-hoc nature of these pipelines\,\nthey require significant human effor t to set up\, extend\, and deploy.\nMoreover\, these tools are difficult t o compose and swap.\n\nThis proposal presents the database gym\, an integr ated framework that\nsystematizes and automates the DBMS configuration pip eline. The gym\neliminates repetition in the setup and operation of such p ipelines by\nproviding a set of reusable\, interoperable\, and interchange able\ncomponents that simplify the development and integration of ML-drive n\nDBMS configuration tools. It leverages its complete control over the\nt uning process to enable optimizations that require end-to-end\nknowledge. First\, it eliminates step-level repetition by skipping over\nredundant co mputation during telemetry collection to reduce the\nlatency of the tuning pipeline. Next\, it eliminates pipeline-level\nrepetition by reusing past experience to improve tool performance. For\nexample\, it adapts models o f DBMS behavior to account for how operator\nsemantics differ across DBMS versions. \n\nWe propose to extend our preliminary work by developing a t ool for\nDBMS upgrades that uses version-aware models to predict performan ce\nimprovements and regressions\, addressing another database\nadministra tion task with significant human involvement. Lastly\, we\nwill leverage r ecent advances in agentic artificial intelligence to\norchestrate tools on behalf of a human operator. These efforts will\ntransform the database gy m from a platform for developing and\ndeploying DBMS configuration tools i nto an autonomous database\nadministrator for production environments. \n \nThesis Committee\n\nAndrew Pavlo (Chair)\n\nJignesh Patel\n\nDavid Ander sen\n\nLin Ma (University of Michigan)\n\nAdditional Information\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c81ffe DTSTART;TZID=America/New_York:20250311T130000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250311T143000 LOCATION:Traffic21 Classroom\, Gates Hillman 6501 SUMMARY:Doctoral Thesis Proposal - Caspar Oesterheld CLASS:PUBLIC DESCRIPTION:Speaker: CASPAR OESTERHELD\, Ph.D. Student\, Computer Science\n Department\, Carnegie Mellon University\n\nTalk Title: New foundational id eas for cooperative AI\n\nMy doctoral research addresses two fundamental o bstacles to beneficial\noutcomes from strategic interactions between multi ple parties:\nstrategic incentives against cooperation (as in the Prisoner 's\nDilemma) and the multiplicity of solutions (sometimes called the\nequi librium selection problem). As AI systems are increasingly\ninvolved in co nsequential decision making processes on behalf of human\nprincipals\, und erstanding how to achieve desirable outcomes in\nmulti-agent AI settings b ecomes critical. My research leverages unique\nfeatures of AI systems — including their transparency\,\nreproducibility\, and malleability — to develop novel game-theoretic\napproaches that enable better\, more coopera tive outcomes.      \n\nThree primary research directions form the cor e of this dissertation.\nFirst\, the concept of safe Pareto improvements  provides a rigorous\nframework for improving outcomes without resolving equilibrium\nselection problems. Unlike traditional solution concepts\, sa fe Pareto\nimprovements make qualitative assumptions about pairs of games rather\nthan individual games. This sometimes allows us to prefer playing one\ngame over another\, without any judgment about how each of the\nindiv idual games is played. Second\, the concept of program\nequilibrium expl ores how the use of mutually transparent\ndecision-making algorithms can a llow for cooperation. Third\, my\nresearch on so-called Newcomb-like dec ision problems takes\ninspiration from philosophical branches of decision theory. I\ninvestigate how cooperation can be achieved when different part ies\ndeploy similar AI systems.\n\nCurrent and planned work extends these directions through several\nprojects\, including: connecting program equil ibrium with mediated\nequilibrium\; exploring sequential program/mediated equilibrium-type\nsettings\; investigating the relationship between self-l ocating beliefs\nand decision theory\; developing theoretical foundations for safe\nPareto improvements\, as well as analyzing safe Pareto improveme nts in\na new setting. I've also started to implement some of these\ntheor etical ideas in language models to test their practical\napplicability. \ n\nThesis Committee\n\nVincent Conitzer (Chair)\n\nTuomas Sandholm\n\nFei Fang\n\nStuart Russell (University of California\, Berkeley)\n\nBen Levins tein (University of Illinois at Urbana-Champaign)\n\nAdditional Informatio n\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c82532 DTSTART;TZID=America/New_York:20250210T143000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250210T160000 LOCATION:Reddy Conference Room\, Gates Hillman 4405 SUMMARY:Doctoral Thesis Proposal - Jeff Xu CLASS:PUBLIC DESCRIPTION:Speaker: JEFF XU\, Ph.D. Student\, Computer Science Department\ , Carnegie\nMellon University\n\nTalk Title: Spectral Techniques for Avera ge-Case Complexity and Beyond\n\nIn recent years\, algorithmic challenges across diverse areas including\nstatistical physics\, machine learning and cryptography have centered\naround statistical inference problems\, i.e.\ , computational problems\nwith average-case inputs. For many of these prob lems\, the best-known\nefficient algorithms are often suboptimal\, giving rise to information\nvs. computation gaps\, discrepancies between what is theoretically\npossible given the amount of information and what can be at tained via\nefficient algorithms. One fundamental question is how we can p rovide\nrigorous evidence of hardness to show that such gaps are\ninsurmou ntable for efficient computation. \n\nWe propose to provide rigorous evid ence via the lens of the\nSum-of-Squares (SoS) algorithms\, a hierarchy of semidefinite\nprogrammings. Unlike several other popular models in the av erage-case\nsetting (eg. low-degree polynomials/statistical-query/ overlap -gap).\nSum-of-Squares algorithms are known to capture various optimal\nal gorithms in both the average and worst-case setting\, and therefore\nprovi de one of the strongest form of hardness. \n\nIn this talk\, I will illus trate that average-case SoS hardness usually\nboils down to the study of s pectral techniques\, specifically the study\nof random matrices with corre lated input\, and how a refined\nunderstanding of such matrices gives rise to the resolution of key\naverage-case complexity questions including spa rse graph\nindependent-set\, densest-k subgraph\, and coloring. Finally\, I will\ntalk about some exciting challenges in the future along this\ndire ction\, and specifically how they boil down again to\nsimple-to-state\, se lf-contained questions about random matrices\, and\nexplore the applicatio ns beyond average-case hardness.\n\nThesis Committee\n\nPravesh K. Kothari (Chair)\n\nAayush Jain\n\nRyan O’Donnell\n\nMadhur Tulsiani (Toyota Tec hnical Institute at Chicago / University of\nChicago)\n\nAdditional Inform ation\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c829a8 DTSTART;TZID=America/New_York:20250121T133000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250121T150000 LOCATION:Reddy Conference Room\, Gates Hillman 4405 and Zoom SUMMARY:Doctoral Thesis Proposal - Joshua Nathaniel Williams CLASS:PUBLIC DESCRIPTION:Speaker: JOSHUA NATHANIEL WILLIAMS\, Ph.D. Student\, Computer S cience\nDepartment\, Carnegie Mellon University\n\nTalk Title: Understandi ng Generative Image Modeling Through Discrete\nCounterfactual Prompt Optim ization\n\nIt is well understood that generative models can exhibit\nrepre sentational biases across various social groups. Without explicit\nconditi oning\, the vast majority of airplane pilots will be male and\nthe vast ma jority of bank tellers will be female. While much of the\nexisting work fo cuses on hypothesis-driven investigations into these\nbiases\, in this pro posed thesis\, we focus on discovery of new and\nunexpected patterns in ho w these models represent people. We show\nthrough the lens of counterfactu al explainability – processes that\nfind minimal input changes that alte r a model's output – a framework\nfor hypothesis generation in order to reveal surprising patterns in\nhow text-to-image models align textual inpu t with socially meaningful\ngroup memberships.\n\nWe establish a formal\, mathematical distinction between counterfactual\nexplanations and adversar ial examples\, which enables the development\nof novel distance metrics an d optimization strategies for identifying\nhuman-readable counterfactual p rompts. Our approach employs discrete\noptimization techniques\, including an adapter for computing gradients\nacross embeddings from diverse models . Furthermore\, we evaluate\ndiscrete prompt optimization methods and demo nstrate that additional\nregularization is crucial for generating coherent and human-like\nprompts. This work lays the foundation for more nuanced u nderstanding\nof representational biases in generative models and offers t ools for\ntheir systematic exploration.\n\nThesis Committee\n\nZico Kolter (Chair)\n\nAditi Raghunathan\n\nHoda Heidari\n\nSarah Laszlo (Visa)\n\n  \n\nAdditional Information\n\nIn Person and Zoom Participation.  See anno uncement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c82e06 DTSTART;TZID=America/New_York:20250117T120000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250117T133000 LOCATION:Gordon Bell Conference Room\, Gates Hillman 5117 SUMMARY:Doctoral Thesis Proposal - Long Pham CLASS:PUBLIC DESCRIPTION:Speaker: LONG PHAM\, Ph.D. Student\, Computer Science Departmen t\,\nCarnegie Mellon University\n\nTalk Title: Hybrid Resource-Bound Analy ses of Programs\n\nResource-bound analysis aims to infer symbolic bounds o f worst-case\nresource usage (e.g.\, running time\, memory\, and energy) o f programs as\nfunctions of program inputs. Resource analysis has numerous \napplications\, including job scheduling in cloud computing and\npreventi on of side-channel attacks. Various resource analysis\ntechniques have bee n developed\, and they have unique strengths and\nweaknesses that compleme nt each other. (Automatic) static resource\nanalysis\, which analyzes the source code of programs\, is sound: if it\nsuccessfully infers a cost boun d\, it is guaranteed to be a valid\nbound. However\, every static analysis technique is incomplete: there\nexists a program that the analysis techni que cannot handle. Meanwhile\,\ndata-driven analysis\, which statistically analyzes cost measurements\nobtained by running programs on many inputs\, can infer a candidate\ncost bound for any program. However\, it does not guarantee soundness\nof inference results. \n\nTo overcome limitations of individual analysis techniques\, I propose\nhybrid resource analysis\, wh ich integrates two complementary analysis\ntechniques to retain their stre ngths while mitigating their respective\nweaknesses. The user first specif ies which analysis techniques are\nused to analyze which code fragments an d quantities. Hybrid analysis\nthen performs its constituent analysis tech niques on their respective\ncode fragments and quantities. Finally\, their inference results are\ncombined into an overall cost bound. \n\nThe deve lopment of hybrid resource analysis has been driven by the\ndesire to go b eyond Automatic Amortized Resource Analysis (AARA)\, a\nstate-of-the-art t ype-based static resource analysis technique. I\nstart by proving polynomi al-time completeness of AARA. I next\nintroduce Bayesian data-driven analy sis\, which conducts Bayesian\ninference on cost measurements to infer a p osterior distribution of\nsymbolic cost bounds. I then present the first h ybrid resource\nanalysis\, Hybrid AARA\, followed by a discussion of its l imitations. To\novercome these limitations\, I introduce the second hybrid resource\nanalysis\, resource decomposition. I additionally describe Swif tlet\,\nwhich instantiates the resource-decomposition framework with AARA and\nBayesian resource analysis. \n\nFinally\, for proposed work\, my col laborators and I plan to develop\ndata-driven-analysis for statistically i nferring not only a worst-case\nsymbolic cost bound but also a worst-case input generator\, which is a\nprogram generating worst-case program inputs of various sizes. \n\nThesis Committee\n\nJan Hoffmann (Chair)\n\nFeras Saad\n\nMatt Fredrikson\n\nFrancois Pottier (Inria Paris Centre)\n\nAdditi onal Information\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c8336d DTSTART;TZID=America/New_York:20250114T150000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20250114T163000 LOCATION:Reddy Conference Room\, Gates Hillman 4405 SUMMARY:Doctoral Thesis Proposal - Hojin Park CLASS:PUBLIC DESCRIPTION:Speaker: HOJIN PARK\, Ph.D. Student\, Computer Science Departme nt\,\nCarnegie Mellon University\n\nTalk Title: Cost-Efficient Storage and Caching in Public Clouds\n\nPublic clouds are widely adopted for their sc alability\, flexibility\,\nand reduced operational overhead\, but optimizi ng costs while\nmaintaining performance remains a significant challenge. T his thesis\naddresses the problems of reducing storage cluster costs in pu blic\nclouds and minimizing cross-cloud/region data access costs by\nexplo iting the elasticity and diversity of public cloud resources\ncombined wit h real-time workload monitoring. \n\nFirst\, this work addresses the chal lenge of reducing storage cluster\ncosts in public clouds through Mimir\, an automated system that\nleverages heterogeneous storage types to determi ne storage cluster\nconfigurations that reduce costs while meeting workloa d performance\nrequirements. Next\, this thesis introduces Macaron\, an\na uto-configuring caching system designed for cross-cloud/region data\nacces s. By dynamically adjusting cache capacity based on workload\ncharacterist ics\, Macaron minimizes remote data access costs and\nensures low latency. Utilizing the object storage for caching storage\ntype\, Macaron demonstr ates substantial cost savings compared to\nexisting cross-cloud/region dat a access approaches. \n\nBuilding on Macaron\, I propose a novel prefetch ing design for\ncross-region data access in public clouds that includes an object\ngrouping-based prefetching algorithm and dynamic cache space\nall ocation for demand-requested and prefetched data. This design aims\nto mit igate cache pollution\, reduce wasted prefetches\, and improve\ndata acces s latency while minimizing additional costs. \n\nBy addressing cost and p erformance optimization in public cloud\nstorage and cross-cloud/region da ta access systems\, this thesis\nenables reducing costs of utilizing publi c cloud resources for storage\nand caching. \n\nThesis Committee\n\nGeorg e Amvrosiadis (Co-Chair)\n\nGregory R. Ganger (Co-Chair)\n\nJignesh M. Pat el\n\nCarlo Curino (Microsoft Research)\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c83818 DTSTART;TZID=America/New_York:20241210T110000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20241210T123000 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-anup-agarwal LOCATION:Reddy Conference Room\, Gates Hillman 4405 and Zoom SUMMARY:Doctoral Thesis Proposal - Anup Agarwal CLASS:PUBLIC DESCRIPTION:Speaker: ANUP AGARWAL\, Ph.D. Student\, Computer Science Depart ment\,\nCarnegie Mellon University\n\nTalk Title: Designing Network Contro l Algorithms with Performance\nGuarantees\n\nControl algorithms\, such as those used in congestion control (CC) and\nadaptive-bitrate (ABR) streamin g\, make critical decisions that\ninfluence performance\, user experience\ , and revenue in networked\napplications. Despite their importance\, these algorithms are often\ndeveloped through heuristics and intuition\, leadin g to implicit\nassumptions about network environments and a lack of formal guarantees\nabout their performance. The result is anywhere from silent t o\nembarrassing performance degradation (e.g.\, the recent Netflix\nlivest ream of Paul vs Tyson).\n\nIn this proposed thesis\, we design tools (both mathematical and\ncomputational) that make formal performance guarantees possible.\nNetwork control algorithms often operate in partially observabl e\nenvironments\, e.g.\, they do not explicitly know the network topology\ ,\nrouting\, link capacities\, or what other flows they share the network\ nwith. The mathematical tools allow us to reason about what information\na lgorithms may infer from their partial observations. The\ncomputational to ols build on these mathematical tools to semi-automate\nthe design of cont rol algorithms\, using techniques from program\nsynthesis\, and game theor y. By combining our tools with techniques in\nnetwork calculus and formal methods\, we precisely state performance\nobjectives and environment assum ptions\, enabling us to construct\nproofs about the performance of the des igned control algorithms.\n\nThrough this work\, we design new CC algorith ms that provide\nperformance bounds on networks where existing algorithms struggle to\nguarantee even 1% utilization. Our systematic methodology als o led us\nto discover and prove new fundamental tradeoffs in congestion co ntrol\,\nincluding a tradeoff between loss and convergence time on network s\nwith jitter and short buffers\, and a tradeoff between fairness and\nro bustness vs. latency and generality of CC algorithms.\n\nThe majority of t he completed work deals with single-agent congestion\ncontrol. In the prop osed work\, we extend our tools to reason about\nmulti-agent control envir onments and ABR algorithms. \n\nThesis Committee\n\nSrinivasan Seshan (Ch air)\n\nVyas Sekar\n\nJustine Sherry\n\nPhilip Brighten Godfrey (Universit y of Illinois Urbana-Champaign)\n\n \n\nAdditional Information\n\nIn Pers on and Zoom Participation.  See announcement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c83cf7 DTSTART;TZID=America/New_York:20241205T153000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20241205T170000 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-asher-trockman LOCATION:Scott Hall 6002 and Zoom SUMMARY:Doctoral Thesis Proposal - Asher Trockman CLASS:PUBLIC DESCRIPTION:Speaker: ASHER TROCKMAN\, Ph.D. Student\, Computer Science Depa rtment\,\nCarnegie Mellon University\n\nTalk Title: Mimetic Initialization for Deep Neural Networks\n\nWhile neural network weights are typically in itialized randomly from\nunivariate distributions\, pre-trained weights of ten have\nvisually-discernible multivariate structure. We propose a techni que\ncalled \"mimetic initialization\" that aims to replicate such structu res\nwhen initializing convolutional networks (CNNs)\, Transformers\, and\ nState Space Models (SSMs). For CNNs\, we handcraft a class of\nmultivaria te Gaussian distributions to initialize filters for\ndepthwise convolution al layers\; for Transformers\, we initialize the\nquery and key weights fo r self-attention layers such that their\nproduct approximates the identity \; and for SSMs\, we initialize layers\nto approximate simple linear atten tion. Mimetic initialization\nsubstantially reduces training time and incr eases final accuracy on\nvarious common small-scale benchmarks.\n\nOur tec hnique enables us to almost close the gap between untrained and\npre-train ed Vision Transformers on small datasets like CIFAR-10\,\nachieving up to a 6% gain in accuracy through initialization alone.\nFor convolutional net works like ConvMixer and ConvNeXt\, we observe\nimprovements in accuracy a nd reductions in training time\, even when\nconvolutional filters are froz en (untrained) after initialization. For\nSSMs\, mimetic initialization su bstantially improves generalization\nabilities on synthetic language tasks like copying and associative\nrecall. Overall\, our findings suggest that the benefits of\npre-training can be separated into two components: servi ng as a good\ninitialization and storing transferable knowledge\, with the former\nbeing simple enough to (at least partially) capture by hand in\nc losed-form.\n\nThesis Committee\n\nZico Kolter (Chair)\n\nAlbert Gu\n\nAdi ti Raghunathan\n\nSébastien Bubeck (OpenAI)\n\n \n\nAdditional Informati on\n\nIn Person and Zoom Participation.  See announcement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c841f7 DTSTART;TZID=America/New_York:20241205T140000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20241205T153000 LOCATION:Gordon Bell Conference\, Gates Hillman 5117 SUMMARY:Doctoral Thesis Proposal - Emre Yolcu CLASS:PUBLIC DESCRIPTION:Speaker: EMRE YOLCU\, Ph.D. Student\, Computer Science Departme nt\,\nCarnegie Mellon University\n\nTalk Title: Weak Extended Resolution a nd Nonautomatability in Proof\nComplexity\n\nThe satisfiability problem fo r propositional logic (SAT) has been a\ncentral topic in computer science for many decades. It is arguably the\ncanonical NP-complete problem: reduc tions from many other problems in\nNP to SAT are often straightforward. As a consequence\, a reasonable\nstrategy when trying to solve a problem in NP is to reduce it to SAT\nand to try to solve the resulting SAT problem i nstead. This strategy\nturns out to be surprisingly effective thanks to th e effectiveness of\nimplementations of heuristic algorithms for SAT\, comm only known as SAT\nsolvers. Those solvers are expected to output proofs to certify their\nanswers\, and in this sense they are proof search algorith ms. Proof\ncomplexity\, the branch of computational complexity that studie s the\nlengths of proofs in propositional proof systems\, offers a way to\ nanalyze the performance of SAT solvers. \n\nIn this thesis proposal\, we focus on proof complexity theoretic\nproblems from two \"contrasting\" en ds of a spectrum: those motivated by\nSAT solving\, aiming to improve heur istic proof search\, and those\narising from computational complexity\, ai ming to show that proof\nsearch is hard in the worst case. In particular\, we focus on the\nfollowing two lines of research: proof complexity of a f amily of\nsystems that we refer to as weak extended resolution systems and the\nautomatability problem from computational complexity. The first\ninv olves proof systems that formalize restricted versions of the\nability to make assumptions that hold without loss of generality\,\ncommonly used inf ormally to shorten proofs. The second is the question\nof whether efficien t proof search is possible in the worst case. We\ngive a complete descript ion of the relative strengths of core weak\nextended resolution systems by introducing a high-level recipe for\nproving separations. We introduce a technique to reduce the hardness\nof automatability between proof systems in a black-box manner\; we give\nan example application and propose an app roach to lift hardness\nresults from weaker to stronger proof systems. \n \nThesis Committee \n\nMarijn J. H. Heule (Chair)\n\nJeremy Avigad\n\nRya n O'Donnell\n\nSamuel R. Buss (University of California San Diego)\n\nAddi tional Information\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c84710 DTSTART;TZID=America/New_York:20241119T100000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20241119T113000 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-nuno-sabino LOCATION:Gates Hillman 7101 SUMMARY:Doctoral Thesis Proposal - Nuno Sabino CLASS:PUBLIC DESCRIPTION:Speaker: NUNO SABINO\, Ph.D. Student\, Computer Science Departm ent\,\nCarnegie Mellon University\n\nTalk Title: Improving Code-Injection Vulnerability Detection &\nConfirmation in JS Programs via Program Analysi s\n\nApplications written in JavaScript are often vulnerable to a range of \nsecurity threats. On the frontend\, DOM-based Cross-Site Scripting\n(DOM -XSS) allows attackers to inject malicious JavaScript code into a\nwebpage . On the backend\, arbitrary code execution (ACE) and arbitrary\ncommand i njection (ACI) enable attackers to execute arbitrary code or\ncommands on the server. Exploiting such vulnerabilities can lead to\nsevere consequenc es\, including unauthorized access to sensitive data\nand even full system compromise.\n\nEach potential flow identified by these tools traces a pro gram path\nwhere attacker-controlled input\, such as a URL\, reaches a sen sitive\nfunction that may lead to arbitrary code execution. DTA requires\n finding a concrete input that demonstrates a potential flow in the\ntarget application\, but prior work fails to thoroughly explore program\npaths. In the backend\, these tools miss ACI and ACE that require\ninputs with co mplex structure. We develop a novel type- and\nstructure-aware fuzzing tec hnique to explore Node.js packages\, and an\nenumerator to synthesize synt actically valid payloads for ACE\nvulnerabilities. Incorporating these com ponents on prior work\nNodeMedic led to finding 2257 potential flows and c onfirm\nvulnerabilities in 766 Node.js packages.\n\nA unique challenge in exploring frontend code is that program behavior\nmay depend on user actio ns on the webpage. To address this\, we develop\na fuzzer to interact with the target webpage and evaluated it against\n43\,436 popular pages. Furth ermore\, we found that including optional\nGET parameters in the target UR L uncovers significantly more DOM-XSS\nvulnerabilities. This led us to use dynamic symbolic execution to\nautomatically synthesize GET parameters sa tisfying program\nconstraints. Compared to our replication of prior work D OMsday\, the\nfuzzer increases potential DOM-XSS flows found by 37% and co nfirms 57%\nmore vulnerabilities.\n\nFinally\, we find that non-exploitabl e potential flows may still hint\ntowards real vulnerabilities that requir e additional steps to confirm\,\nsuch as bypassing sanitization measures a nd extending the attacker’s\ncapabilities by executing other program par ts. Thus\, we propose the\ndesign and implementation of exploration strate gies that efficiently\nexplores the program to discover an exploitable pat h\, using\ninformation from a given potential flow that we assume to have found\nalready. \n\nThesis Committee\n\nLimin Jia (Chair)\n\nPedro Adão (Co-chair\, Instituto Superior Técnico)\n\nRui Maranhão (Co-chair\, Univ ersidade do Porto)\n\nLujo Bauer\n\nRuben Martins\n\nJosé Fragoso (Instit uto Superior Técnico)\n\nCristian-Alexandru Staicu (CISPA Helmholtz Cente r for Information\nSecurity)\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c84c73 DTSTART;TZID=America/New_York:20241118T140000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20241118T150000 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-long-pham LOCATION:ASA Conference Room\, Gates Hillman 6115 SUMMARY:Doctoral Thesis Proposal - to be rescheduled CLASS:PUBLIC DESCRIPTION:Speaker: LONG PHAM \, Ph.D. Student\, Computer Science Departme nt\,\nCarnegie Mellon University\n\nTalk Title: Hybrid Resource-Bound Anal yses of Programs\n\nResource-bound analysis aims to infer symbolic bounds of worst-case\nresource usage (e.g.\, running time\, memory\, and energy) of programs as\nfunctions of program inputs. Resource analysis has numerou s\napplications\, including job scheduling in cloud computing and\nprevent ion of side-channel attacks. Various resource analysis\ntechnique have bee n developed\, and they have unique strengths and\nweaknesses that compleme nt each other. (Automatic) static resource\nanalysis\, which analyzes the source code of programs\, is sound: if it\nsuccessfully infers a cost boun d\, it is guaranteed to be a valid\nbound. However\, every static analysis technique is incomplete: there\nexists a program that the analysis techni que cannot handle. Meanwhile\,\ndata-driven analysis\, which statistically analyzes cost measurements\nobtained by running programs on many inputs\, can infer a candidate\ncost bound for any program. However\, it does not guarantee soundness\nof inference results. \n\nTo overcome limitations of individual analysis techniques\, I propose\nhybrid resource analysis\, wh ich integrates two complementary analysis\ntechniques to retain their stre ngths while mitigating their respective\nweaknesses. The user first specif ies which analysis techniques are\nused to analyze which code fragments an d quantities. Hybrid analysis\nthen performs its constituent analysis tech niques on their respective\ncode fragments and quantities. Finally\, their inference results are\ncombined into an overall cost bound. \n\nThe deve lopment of hybrid resource analysis has been driven by the\ndesire to go b eyond Automatic Amortized Resource Analysis (AARA)\, a\nstate-of-the-art t ype-based static resource analysis technique. I\nstart by proving polynomi al-time completeness of AARA. I next\nintroduce Bayesian data-driven analy sis\, which conducts Bayesian\ninference on cost measurements to infer a p osterior distribution of\nsymbolic cost bounds. I then present the first h ybrid resource\nanalysis\, Hybrid AARA\, followed by a discussion of its l imitations. To\novercome these limitations\, I introduce the second hybrid resource\nanalysis\, resource decomposition. I additionally describe Swif tlet\,\nwhich instantiates the resource-decomposition framework with AARA and\nBayesian resource analysis. Finally\, for proposed work\, my\ncollabo rators and I plan to develop data-driven-analysis for\nstatistically infer ring not only a worst-case symbolic cost bound but\nalso a worst-case inpu t generator\, which is a program generating\nworst-case program inputs of various sizes. \n\nThesis Committee\n\nJan Hoffmann (Chair)\n\nFeras Saad \n\nMatt Fredrikson\n\nNadia Polikarpova (University of California\, San D iego)\n\n \n\nAdditional Information\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c85236 DTSTART;TZID=America/New_York:20241115T123000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20241115T140000 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-benjamin-stoler LOCATION:Reddy Conference Room\, Gates Hillman 4405 and Zoom SUMMARY:Doctoral Thesis Proposal - Benjamin Stoler CLASS:PUBLIC DESCRIPTION:Speaker: BENJAMIN STOLER\, Ph.D. Student\, Computer Science Dep artment\,\nCarnegie Mellon University\n\nTalk Title: Towards Robust Autono mous Driving and Social Robot\nNavigation via Enhanced Data Utilization\n\ nAutonomous robots—including self-driving vehicles\, sidewalk delivery\n robots\, and more—must navigate among humans in a safe and\nsocially-com pliant manner. Current approaches for building and\nevaluating such autono mous systems rely on data-driven techniques\;\nhowever\, a generalization gap emerges\, as methods trained in these\ntraditional paradigms are unabl e to cope with unexpected real-world\nscenarios. Therefore\, this thesis a ims to develop improved evaluation\nsettings and methodologies to increase and assess robustness in\nautonomous robot navigation against these chall enges. This thesis\nproposal describes several completed works that assess and improve\ndifferent facets of robustness in autonomy:\n\nFor robustnes s against perception errors affecting downstream motion\nprediction\, we c onstruct a framework for converting top-down\npedestrian trajectory datase ts into a more challenging first-person\nview perspective. We then develop a correction module to account for\nthe resulting errors\, trained end-to -end with trajectory prediction\napproaches.For robustness against out-of- distribution\, safety-relevant\nscenarios\, we create a hierarchical chara cterization method which\nleverages counterfactual probes to find hidden s afety-relevant\nscenarios in large datasets. We then address the induced\n generalization gap by incorporating the characterizations into\ndownstream trajectory prediction models' inductive biases.For\nrobustness against ad versarial\, safety-critical scenarios\, we develop\na reactive\, skill-bas ed adversary policy which leverages a learned\,\nmulti-faceted criticality objective to perturb existing scenarios. We\nthen train ego policies in a closed-loop manner against these\ngenerated scenarios\, demonstrating imp roved downstream ego\nperformance.\n\nThis proposal concludes by outlining and discussing proposed works to\nfurther advance robustness in autonomou s navigation. These works\ninclude enhancements in scenario characterizati on and\nout-of-distribution generalization\, as well as novel formulations of\nrealism as an objective in safety-critical generation. \n\nThesis Co mmittee\n\nJean Oh (Chair)\n\nSebastian Scherer\n\nReid Simmons\n\nJonatha n Francis (Bosch Center for Artificial Intelligence)\n\n \n\nAdditional I nformation\n\nIn Person and Zoom Participation.  See announcement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c857b9 DTSTART;TZID=America/New_York:20241029T110000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20241029T123000 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-joseph-e-reeves LOCATION:Reddy Conference Room\, Gates Hillman 4405 and Zoom SUMMARY:Doctoral Thesis Proposal - Joseph E. Reeves CLASS:PUBLIC DESCRIPTION:Speaker: JOSEPH E. REEVES\, Ph.D. Student\, Computer Science De partment\,\nCarnegie Mellon University\n\nTalk Title: Cardinality Constrai nts in Satisfiability Solving\n\nAutomated reasoning (AR) engines solve pr oblems represented in\nmathematics and logic stemming from a wide range of domains including\nhardware and software verification\, cryptography\, an d cloud security.\nBoolean satisfiability (SAT) solvers drive much of the reasoning\nbehind many AR engines\, but their input format\, a formula in\ npropositional logic\, can be limiting. High-level constraints must\nbe e ncoded into sets of simpler constraints\, clauses\, and finding\na good  encoding often requires expert knowledge. We propose\nextending the inpu t of SAT solvers to include cardinality constraints\,\nmoving encoding que stions from the user-side to the solver-side.\nCardinality constraints are a frequently occurring type high-level\nconstraint that represent countin g\, e.g.\, “at least k packages must\nbe delivered” or “you can wor k from home at most one day of the\nweek”.\n\nIn this proposal we disc uss four research problems arising from a\ncardinality-based input. First\ , we will develop a cardinality\nconstraint extraction tool that will conv ert previously encoded\nproblems into a cardinality-based normal form\, pr oviding backwards\ncompatibility for our solving techniques. Second\, we w ill engineer\ndynamic cardinality constraint encoding into the top-tier SA T solver\nCaDiCaL to improve performance on problems with many cardinality \nconstraints. Third\, we will explore the ways in which parallel solving\ ntechniques can leverage information within cardinality constraints to\nac hieve better problem partitioning. Fourth\, we will equip the\nextraction and solving with end-to-end proof checking through\nmodifications to exist ing proof systems and proof checkers. Our goal\nin investigating these fou r research problems is to support the claim\nthat a cardinality-based form at should be the standard input format\nfor modern SAT solvers.\n\nThesis Committee\n\nMarijn Heule (Chair)\n\nRandal Bryant\n\nRuben Martins\n\nArm in Biere (University of Freiburg) \n\nAdditional Information\n\nIn Person and Zoom Participation.  See announcement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c85ccb DTSTART;TZID=America/New_York:20241015T140000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20241015T153000 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-mengchieh-jeremy- lee LOCATION:Reddy Conference Room\, Gates Hillman 4405 and Zoom SUMMARY:Doctoral Thesis Proposal - Meng-Chieh (Jeremy) Lee CLASS:PUBLIC DESCRIPTION:Speaker: MENG-CHIEH (JEREMY) LEE\, Ph.D. Student\, Computer Sci ence\nDepartment\, Carnegie Mellon University\n\nTalk Title: Explainable M ining of Graphs and Time Series: Algorithms\nand Applications\n\nGiven a s ocial network\, how can we predict the connections between\nusers and dete rmine whether they are based on shared hobbies or common\nfriends? Similar ly\, how can we identify anomalies in time series data\nand explain why th ey are suspicious? Although recent machine learning\nmodels with improved performance are being developed\, they are often\nblack-box methods that a re difficult to interpret. This leads us to\nexplainable artificial intell igence (XAI)\, which offers valuable\ninsights through its explanations.   \n\nIn this thesis proposal\, we introduce carefully designed explaina ble\nmethods tailored for graph and time series data\, with diverse\nappli cations. Each method we proposed is either inherently\nexplainable\, or pr ovides explanations for the data or decisions it\nmakes.  \n\nThesis Com mittee \n\nChristos Faloutsos (Co-Chair)\n\nLeman Akoglu (Co-Chair)\n\nGe offrey Gordon\n\nNina Mishra (Amazon)\n\nAdditional Information\n\nIn Pers on and Zoom Participation.  See announcement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c8611d DTSTART;TZID=America/New_York:20241003T110000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20241003T123000 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-junting-hsieh LOCATION:Blellock-Skees Conference Room\, Gates Hillman 8115 SUMMARY:Doctoral Thesis Proposal - Jun-Ting Hsieh CLASS:PUBLIC DESCRIPTION:Speaker: JUN-TING HSIEH\, Ph.D. Student\, Computer Science Depa rtment\,\nCarnegie Mellon University\n\nTalk Title: Spectral Algorithms fo r Optimization beyond the\nAverage-Case\n\nSpectral algorithms involve usi ng the eigenvalues and eigenvectors of\nmatrices derived from the input fo r algorithm design and analysis.\nThese techniques have achieved remarkabl e success across a wide range\nof computational problems. In particular\, through the study of random\nmatrices\, spectral methods have been widely used to solve problems in\naverage-case complexity\, where the input is dr awn from some random\nmodel. \n\nIn this proposal\, we explore the robust ness of spectral algorithms for\nhybrids between worst-case and average-ca se input models. Many\nexisting algorithms tend to “overfit” to the sp ecific randomness\nof the input – they fail even with slight perturbatio ns of the input\nmodels. First\, we show that spectral algorithms succeed in both\nrefuting semirandom constraint satisfaction problems (CSPs) and\n solving semirandom planted instances\, generalizing results previously\nkn own only for fully random CSPs. Second\, we demonstrate how upper\nbounds on the second eigenvalue of the adjacency matrix suffice for\nfinding larg e independent sets in 3-colorable graphs\, extending\nexisting results for random 3-colorable graphs.\n\nFinally\, for future work\, we aim to exten d such ideas to worst-case\ninstances by understanding the minimal assumpt ions necessary for\nalgorithmic success. Moreover\, we will explore the li mitations of\nspectral algorithms and investigate formal connections betwe en\nspectral algorithms and low-degree polynomials of the input. \n\nThes is Committee \n\nPravesh K. Kothari (Carnegie Mellon University/Princeton University)\n\nRyan O'Donnell\n\nJason Li\n\nVenkatesan Guruswami (Univer sity of California\, Berkeley)\n\nDavid Steurer (ETH\, Zürich)\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c865c2 DTSTART;TZID=America/New_York:20240919T113000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20240919T130000 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-aditi-kabra LOCATION:Gordon Bell Conference Room\, Gates Hillman 5117 SUMMARY:Doctoral Thesis Proposal - Aditi Kabra CLASS:PUBLIC DESCRIPTION:Speaker: ADITI KABRA\, Ph.D. Student\, Computer Science Departm ent\,\nCarnegie Mellon University\n\nTalk Title: Verified Control Envelope Synthesis for Hybrid Systems\n\nMany cyber-physical systems\, such as tra ins\, planes\, and self-driving\ncars\, are safety-critical but difficult to reason about. Formal\nverification can provide strong safety guarantees \, but most industrial\ncontrollers are too complex to formally verify. Sa fe control envelopes\ncharacterize families of safe controllers and are us ed to monitor\nuntrusted controllers on verifiable abstractions of control systems\nthat isolate the parts relevant to safety without the full compl exity\nof a specific control implementation\, at runtime. They can put com plex\ncontrollers\, even when machine learning based\, within the reach of \nformal guarantees. But correct control envelopes are still hard to\ndesi gn because the control engineer needs to identify correct control\nconditi ons that tell the controller what to do right now to stay safe\nat all tim es in the future by anticipating the behavior of the system\nover complex dynamics and an uncountably infinite state space. \n\nThis thesis propose s to provide synthesis techniques to automatically\nsynthesize provably co rrect control conditions\, greatly reducing the\nmanual effort required fo r control envelope design. It aims to scale\nsynthesis to complexity of re al-world systems. The input of the\nsynthesis tool is a sketch of the cont rol envelope in a hybrid system\nshowing what kind of control behavior is physically possible. The tool\nfills in the blanks of the sketch by synthe sizing control conditions\nusing hybrid system game theory. The output is a provably correct\nsymbolic control envelope. Existing controller synthes is techniques do\nnot solve control envelope synthesis because control env elopes have\nthe higher-order constraint of permitting as many valid contr ol\nsolutions as possible. \n\nCompleted work provides the algorithm CESA R (Control Envelope\nSynthesis via Angelic Refinement) which solves a clas s of problems\nwhere a set of systematic game refinements allows automatic control\nenvelope synthesis. Proposed work generalizes synthesis to a bro ad\nclass of systems (characterized by admitting a natural representation\ nin differential game logic) and develops a system that allows users to\np rovide the human intuition based insights that\, together with\nautomated reasoning\, can complete the control envelope synthesis\nprocess in more c omplex cases. \n\nThesis Committee\n\nAndré Platzer (Co-chair\, Carnegie Mellon University/Karlsruhe\nInstitute of Technology)\n\nStefan Mitsch (C o-chair\, Carnegie Mellon University/DePaul University)\n\nEunsuk Kang\n\n Armando Solar-Lezama (Massachusetts Institute of Technology)\n\n \n\nAdd itional Information\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c86b2a DTSTART;TZID=America/New_York:20240903T143000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20240903T160000 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-mingxun-zhou LOCATION:Reddy Conference Room\, Gates Hillman 4405 and Zoom SUMMARY:Doctoral Thesis Proposal - Mingxun Zhou CLASS:PUBLIC DESCRIPTION:Speaker: MINGXUN ZHOU\, Ph.D. Student\, Computer Science Depart ment\,\nCarnegie Mellon University\n\nTalk Title: Practical Private Inform ation Retrieval and Searching with\nSublinear Cost\nMathJax.Hub.Config({\n tex2jax: {\ninlineMath: [ ['$'\,'$']\, [\"\\\\(\"\,\"\\\\)\"] ]\,\nprocess Escapes: true\n}\n})\;\n\nPrivate Information Retrieval (PIR) is a long-st udied cryptographic\nprimitive that allows a user to retrieve information from a public\ndatabase without revealing the query to the service provid er.\nClassically\, PIR was studied in a setting without any preprocessing\ ,\nand this setting is known to have inherent limitations that the total\n computation cost per query must be linear in the size of the database\nto achieve privacy. This limitation is the fundamental barrier for\nscaling P IR to large databases and building practical product systems\nbased on PIR . Pioneered by Beimel\, Ishai and Malkin (Crypto 2000) and\nCorrigan-Gibbs and Kogan (Eurocrypt 2020)\, the preprocessing PIR\nparadigm has been sho wn to overcome the linear computation cost\nbarrier. Nonetheless\, prior w orks on preprocessing PIR remain mostly\nin the theoretical space due to t heir use of heavy cryptographic\nprimitives and/or convoluted algorithmic constructions.\n\nAchieved Results: We proposed a practical single-server PIR\nconstruction in the preprocessing setting\, named Piano (S P 2023)\,\ nthat achieved sublinear query cost based on lightweight cryptographic\npr imitives. Piano achieved $\\tilde O(\\sqrt{n})$ amortized\ncommunication a nd computation per query given a database of size n \,\nand only required $\\tilde O(\\sqrt{n})$ client storage. Notably\, it is\nalso concretely ef ficient – for a 100GB database of 1.6 billion\nentries\, Piano takes onl y 12ms online computation time on a single\nCPU-core. Subsequently\, we im proved the construction and obtained a\nnew practical PIR scheme\, Quarter PIR (Eurocrypt 2024)\, that reduced\nthe online communication cost to $\\t ilde O(n^{1/4})$ per query\, while\nmaintaining competitive practical perf ormances. Proposed Direction:\nNearly all existing PIR constructions are d esigned for point accesses\nin an array-type database\, while many practic al information retrieval\nsystems like search engines do need more advance d access algorithms to\nsupport semantic and similarity queries. We propos e to construct a\nprivate search algorithm that can handle semantic/simila rity queries\nwith sublinear communication and computation query costs bas ed on our\npractical PIR constructions and graph-based Nearest Neighbor Se arch\n(NNS) algorithms. This construction will be the first private search \nalgorithm that achieves sublinear query cost\, and it has the potential\ nto support multi-modal search queries including text\, image\, voice and\ nvideo search.\n\nThesis Committee: \n\nElaine Shi (Co-chair)\n\nGiulia F anti (Co-chair)\n\nBryan Parno\n\nDavid Wu (University of Texas at Austin) \n\nAdditional Information\n\nIn Person and Zoom Participation. See announ cement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c87484 DTSTART;TZID=America/New_York:20240903T080000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20240903T213000 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-afonso-tinnoco LOCATION:Gates Hillman 8102 and Zoom SUMMARY:Doctoral Thesis Proposal - Afonso Tinnoco CLASS:PUBLIC DESCRIPTION:Speaker: AFONSO TINOCO\, Ph.D. Student\, Computer Science Depar tment\,\nCarnegie Mellon University\n\nTalk Title: Towards Practical and V erifiable Distributed Systems:\nApplications of Oblivious Algorithms\, Gar bled Circuits and Formal\nMethods+\n\nIn my research\, I want to design an d develop practically efficient and\nprovably secure distributed systems. To this end\, I combine applied\ncryptography and formal verification tool s. The goal of this proposal\nis to provide primitives that can be used in distributed systems\, as\nwell as methodologies to verify consensus proto cols\, to ensure the\nsecurity\, efficiency\, and correctness of distribut ed systems.\nSpecifically\, the research focuses on three main areas: prac tical\nimplementations of oblivious algorithms for Trusted Execution\nEnvi ronments (TEEs)\; practical and verified implementations of Garbled\nRAM\; and methodologies to verify safety and liveness of consensus\nprotocols.  \n\nTEEs can be used to offer efficient crash fault nodes with\nconfiden tial computations\; however\, most TEEs implementations leak the\npage-lev el memory access pattern to the host machine where the TEE is\nrunning. Th erefore\, to guarantee confidential computations\, TEE\nprograms need not only correct implementations but also to be memory\ntrace-oblivious. There has been extensive theoretical research in\noblivious algorithms\; howeve r\, there is a gap with practical\nimplementations\, particularly in the T EE setting. In this proposal\, we\naim to close this gap\, providing an ob livious data structure library\nakin to C++'s STL\, and extending it with oblivious graph algorithms. \n\nTEEs require trust in the hardware manufa cturer and a certain level of\nhardware/software integrity. In scenarios w here this isn't possible\,\nGarbled Circuits can be used to provide equiva lent secure processor\nguarantees based on cryptographic assumptions. To a chieve an efficient\nGarbled Circuit processor\, Garbled RAM is necessary\ , and recent\ntheoretical advancements suggest using tristate circuits to implement\nit. In this proposal\, we aim to achieve concretely more effici ent\nGarbled RAM constructions\, as well as provide methodologies to verif y\nthe correctness of tristate circuits. \n\nFinally\, while TEEs and Gar bled RAM aim to achieve secure\ncomputations\, ensuring the correctness of the underlying protocols\nthat use them is critical. We have previously d eveloped a python DSL\nto verify safety properties of distributed system p rotocols. In this\nproposal\, we aim to extend this framework to verify li veness\nproperties of distributed system protocols\, focusing on proof\nau tomation and generalization.  \n\nThesis Committee: \n\nElaine Shi (Co- chair)\n\nRodrigo Rodrigues (Co-chair\, University of Lisbon\, Instituto S uperior\nTécnico)\n\nBryan Parno\n\nPedro Adão (University of Lisbon\, I nstituto Superior Técnico)\n\nJosé Fragoso (University of Lisbon\, Insti tuto Superior Técnico)\n\nAndrew Miller (University of Illinois Urbana-Ch ampaign)\n\n \n\nAdditional Information\n\nIn Person and Zoom Participati on. See announcement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c87a9d DTSTART;TZID=America/New_York:20240823T150000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20240823T163000 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-brian-zhang LOCATION:Gates Hillman 8102 SUMMARY:Doctoral Thesis Proposal - Brian Zhang CLASS:PUBLIC DESCRIPTION:Speaker: BRIAN ZHANG\, Ph.D. Student\, Computer Science Departm ent\,\nCarnegie Mellon University\n\nTalk Title: New Solution Concepts\, A lgorithms\, and Applications for\nExtensive-Form Games: Learning\, Correla tion\, Communication\, and Common\nKnowledge\n\nComputational game theory has led to significant breakthroughs in AI\ndating back to the start of AI as a discipline. These include the\nstrongest AI agents for both recreati onal and practical applications.\nIt has been instrumental in enabling sup erhuman AI from recreational\ngames such as two-player zero-sum games ches s\, go\, and heads-up poker\nto multiplayer games such as six-player poker and Hanabi\, and even in\ngames involving human language such as Diplomac y. It has also\nempowered a growing range of non-recreational applications \, such as\ntrading\, machine learning robustness and safety\, negotiation \, conflict\nresolution\, mechanism design\, information design\, security \, political\ncampaigning\, and self-driving cars. \n\nThis thesis pushes the boundary on computational game theory\,\nespecially in imperfect-info rmation sequential (extensive-form) games\,\nwhich are most prevalent in p ractical applications both in zero-sum\ngames and beyond. We present new t heoretical concepts and frameworks\,\nstate-of-the-art and often provably optimal algorithms for computing\nand learning equilibria\, and new ways t o apply such algorithms to\nreal-world problems\, including problems in ec onomics such as mechanism\nand information design.\n\nThe thesis contains four parts.\n\nI)  We develop new solution concepts and state-of-the-art complexity\nresults for adversarial team games. Among other results\, we c ompute\nexact solutions to several variants of the popular game The\nResis tance: Avalon with up to six players.\n\nII)  We develop an algorithmic f ramework for generalized mechanism\ndesign that covers sequential mechanis m design\, sequential information\ndesign\, optimal correlated equilibria and more for the first time\, and\nreduces them to zero-sum games. This en ables computation using any\nzero-sum game solving technique\, including d eep reinforcement\nlearning.\n\nIII)  We develop the fastest learning alg orithms for minimizing\nregret against linear and low-degree deviations\, which are the\ntightest solution concepts known to be efficiently learnabl e in games.\n\nIV)  We develop new techniques for subgame solving that wo rk even\nwhen the common-knowledge set is too large to work with\, and use these\ntechniques to build the first strong bot—and\, to our knowledge\ ,\ncurrently the best bot—for the game of dark chess. \n\nThesis Commit tee\n\nTuomas Sandholm (Chair)\n\nVincent Conitzer\n\nZico Kolter\n\nKevin Leyton-Brown (University of British Columbia)\n\nAdditional Information\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c88025 DTSTART;TZID=America/New_York:20240823T121500 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20240823T134500 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-arjun-laksmipathy LOCATION:Gates Hillman 8102 and Zoom SUMMARY:Doctoral Thesis Proposal - Arjun Laksmipathy CLASS:PUBLIC DESCRIPTION:Speaker: ARJUN LAKSMIPATHY\, Ph.D. Student\, Computer Science\n Department\, Carnegie Mellon University\n\nTalk Title: Contact Areas for D exterous Manipulation\n\nHumans use their hands to effortlessly manipulate objects of\narbitrarily complex geometries and physical properties every day\;\nhowever\, adapting such manipulations to dexterous robots and virtu al\ncharacters is an extremely difficult task. Understanding the ways in\n which humans exploit contact to perform these manipulations has the\npoten tial to greatly advance progress towards this goal. \n\nUnsurprisingly\, research efforts have analyzed contact in the context\nof dexterous manipu lation for decades. We now have numerous metrics\nfor evaluating grasp qua lity in terms of contacts\, efficient means of\ncomputing contact in physi cal simulation\, and countless strategies\nexploiting contact corresponden ces between hands and objects to\nsynthesize grasps and manipulations. But the majority of existing\nworks fundamentally characterize contact in the same way: as points\,\nlines\, or planes of interaction. \n\nBut contact s in the real world are much more complicated. Instead\,\nreal bodies inte rface with one another via areas of contact which\ngreatly vary with the g eometries of contacting surfaces. If we wish to\nmodel the complexities of manipulations as they actually occur\, then\nwe must progress beyond such simplifying assumptions and deal with the\nmessy nature of reality. This thesis aims to do so by presenting\nframeworks and algorithms for the mode ling\, capture\, mutation\, and\nexploitation of contact areas. Our intent ion is to establish the\nfoundations necessary to elevate contact areas to first-class\nprimitives and demonstrate their inherent value across a ran ge of\npractical applications in dexterous manipulation and adjacent\ndoma ins.    \n\nFirst\, we introduce three novel models of contact areas al ongside\noperations supported by each model which are fundamentally design ed to\nrun on real geometries rather than simple primitive shapes. Second\ , we\nintroduce a low cost approach for capturing human contacts from the\ nreal world. Then\, using these models\, we introduce: a new set of\nintui tive artist tools for drafting high quality grasps\, a novel\nmotion retar geting pipeline for dexterous manipulations\, a novel\ncontact-driven cont rol framework for dexterous robot hands\, and two\npractical extensions of our work. The contributions in this thesis are\nnot intended to be the la st words\, but rather important first steps\ndesigned to promote future re search in contact area modeling.\n\nThesis Committee\n\nNancy S. Pollard ( Chair)\n\nJessica K. Hodgins\n\nKeenan Crane\n\nC. Karen Liu (Stanford Uni versity)\n\nAdditional Information\n\nIn Person and Zoom Participation.  See announcement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c885db DTSTART;TZID=America/New_York:20240812T160000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20240812T173000 URL:https://csd.cmu.edu/calendar/thesis-proposal-runtian-zhai LOCATION:Traffic21 Classroom\, Gates Hillm 6501 and Zoom SUMMARY:Thesis Proposal - Runtian Zhai CLASS:PUBLIC DESCRIPTION:Speaker: RUNTIAN ZHAI\, Ph.D. Student\, Computer Science Depart ment\,\nCarnegie Mellon University\n\nTalk Title: Learning Generalizable a nd Transferable Representations\nwith Big Models\n\nMachine learning has s hifted to a new paradigm driven by\nrepresentation learning and foundation models\, big encoders that\nextract useful features from data. This thesi s studies how big models\nlearn good representations\, and especially focu ses on two aspects:\ngeneralization and transferability. For generalizatio n\, the problem is\nwhy big foundation models wouldn’t overfit as classi cal theory\nsuggests.\n\nMy work proves a generalization bound that works for big models\, by\nviewing them as algorithmic models instead of data mo dels. For\ntransferability\, my work focuses on reweighting\, the most pop ular\nclass of methods. This talk will focus on one issue with reweighting \nthat is its sensitivity to outliers\, and propose a solution that\nsigni ficantly improves the performance and stability of reweighting.\nFinally\, I will propose two future work\, feature learning for tabular\ndata\, and combining multiple sources of prior knowledge.\n\nThesis Committee:\n\nPr adeep Ravikumar (Co-chair)\n\nZico Kolter (Co-chair)\n\nAndrej Risteski\n\ nYuandong Tian (Meta AI)\n\nAdditional Information\n\nIn Person and Zoom P articipation. See announcement.\n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c88a07 DTSTART;TZID=America/New_York:20240806T150000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20240806T163000 URL:https://csd.cmu.edu/calendar/doctoral-thesis-proposal-suhas-jayaram-sub ramanya LOCATION:Reddy Conference Room\, Gates Hillman 4405 SUMMARY:Doctoral Thesis Proposal - Suhas Jayaram Subramanya CLASS:PUBLIC DESCRIPTION:Speaker: SUHAS JAYARAM SUBRAMANYA\, Ph.D. Student\, Computer Sc ience\nDepartment\, Carnegie Mellon University\n\nTalk Title: Efficient jo b-resource co-adaptivity for deep learning\nworkloads on large heterogeneo us GPU clusters\n\nThe training performance of a deep learning (DL) traini ng job is\ndetermined by the number\, type and arrangement of the allocate d GPU\nresources\, and the job parameters (like batch size and learning ra te)\nused for execution. Modern clusters for DL training contain tens of\n thousands of GPUs of many types\, and a cluster scheduler allocates\nGPUs to training jobs to maximize collective training progress in the\ncluster. Existing DL cluster schedulers cannot handle the large space\nof adaptivi ty choices (i.e.\, combined space of GPU allocations and job\nparameters) for large\, heterogeneous GPU clusters — many are not\nheterogeneity-awa re\, few are adaptivity-aware\, and none scale to large\nclusters without sacrificing allocation fidelity and cluster\nefficiency. \n\nIn this thes is\, we introduce (a) a scheduler to facilitate efficient\njob-resource ad aptivity for DL training jobs on large heterogeneous\nGPU clusters\, and ( b) a method to scale optimization-based scheduling\nto much larger cluster sizes without sacrificing allocation fidelity\nand resource efficiency. O ur adaptivity-aware scheduler\, Sia\, uses GPU\nresources judiciously to l earn a job's training performance across\ndifferent GPU types\, and contin uously co-optimizes the GPU allocation\nand job execution parameters to ma ximize cluster-wide training\nprogress in heterogeneous GPU clusters. We t hen scale Sia to large\ncluster sizes by modeling the scheduling policy as a continuous\noptimization problem. We show that it is possible to augmen t the\ninterface between a scheduler and the optimization problem solver t o\nefficiently track changes to the scheduling problem arising from\nchang ing cluster conditions like job arrivals\, departures and phase\nchanges. We develop a prototype solver with the augmented interface\nfor the Sia sc heduling policy that can efficiently recover allocations\nfor very large c lusters. As an additional contribution\, we observe\nthat many other resou rce-allocation problems can also be formulated as\ncontinuous optimization problems and can be solved both quickly and\nefficiently using our propos ed solver. \n\nThesis Committee:\n\nGreg Ganger (Chair)\n\nZhihao Jia\n\n Virginia Smith\n\nAmar Phanishayee (Meta)\n\n \n\nAdditional Information\ n DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c88f28 DTSTART;TZID=America/New_York:20240529T140000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20240529T153000 LOCATION:Reddy Conference Room\, Gates Hillman 4405 SUMMARY:Thesis Proposal - Eric Sturzinger CLASS:PUBLIC DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c8910b DTSTART;TZID=America/New_York:20240528T130000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20240528T130000 LOCATION:Traffic21 Classroom\, Gates Hillman 6501 SUMMARY:Thesis Proposal - Mingjie Sun CLASS:PUBLIC DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c892a1 DTSTART;TZID=America/New_York:20240502T120000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20240502T133000 LOCATION:Reddy Conference Room\, Gates Hillman 4405 SUMMARY:Computer Science Thesis Proposal CLASS:PUBLIC DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c89440 DTSTART;TZID=America/New_York:20240430T100000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20240430T113000 LOCATION:Reddy Conference Room\, Gates Hillman 4405 and Zoom SUMMARY:Computer Science Thesis Proposal CLASS:PUBLIC DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c895e3 DTSTART;TZID=America/New_York:20240426T100000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20240426T100000 LOCATION:Gordon Bell Conference Room\, Gates Hillman 5117 SUMMARY:Computer Science Thesis Proposal CLASS:PUBLIC DTSTAMP:20260617T225644Z END:VEVENT BEGIN:VEVENT UID:6a33262c8977f DTSTART;TZID=America/New_York:20240422T130000 SEQUENCE:0 TRANSP:TRANSPARENT DTEND;TZID=America/New_York:20240422T143000 LOCATION:Reddy Conference Room\, Gates Hillman 4405 and Zoom SUMMARY:Computer Science Thesis Proposal CLASS:PUBLIC DTSTAMP:20260617T225644Z END:VEVENT END:VCALENDAR