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:6a4a12c73a2fc 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: \nSpeaker: QI PANG\, Ph.D. Student\, Computer Science Departme nt\, Carnegie\nMellon University\n\nTalk Title: Provably Secure Approaches for Generative AI Systems: From\nPrivate Inference to Accountable Agents\ n\nGenerative AI is moving into high-stakes domains such as healthcare\,\n finance\, and law\, and it is evolving from static query-response models\n into autonomous agents that hold memory\, call external tools\, and\ncommu nicate with one another. This shift expands the attack surface\ndramatical ly. A modern generative AI system spans several layers: the\ninputs a user provides\, the model and the privacy guarantee it claims\,\nthe outputs i t produces\, and the messages its agents exchange. Each of\nthese layers r ests on a fragile trust assumption: inputs may carry\nsensitive personal i nformation\, outputs cannot be reliably attributed\nto their source\, inte r-agent messages can hide cryptographically\nundetectable payloads\, and a model's advertised differential privacy\nguarantee may quietly fail to ho ld. Heuristic defenses such as input\nredaction\, AI-text classifiers\, tr anscript monitors\, and procedural\nprivacy audits offer little assurance against a motivated adversary\,\nbecause they rest on pattern matching rat her than proof.\n\nThis thesis argues that trustworthiness should be a pro vable\,\nfoundational property of generative AI systems\, achieved by\nco- designing applied cryptography (secure multi-party computation\,\nhomomorp hic encryption\, and zero-knowledge proofs) and differential\nprivacy with the structure of modern generative models. I develop this\nargument acros s the four layers above through four systems. BOLT\n(completed) protects u ser inputs with privacy-preserving Transformer\ninference that is accurate and an order of magnitude more efficient\nthan prior work. A study of LLM watermarking (completed) establishes\nthe fundamental trade-offs that gov ern output provenance and shows\nprecisely when heuristic watermarks can b e removed or forged. For\ninter-agent communication\, I propose a study of steganographic\ncollusion that constructs a high-capacity covert channel and a\nprovable mechanism to disrupt it. For the model layer\, I propose\n Noisette\, a system that makes differential privacy verifiable by\ncertify ing\, in zero knowledge\, that the differential privacy noise was\nsampled correctly. Together\, these systems chart a path toward\ngenerative AI th at is not only powerful but also demonstrably private\,\naccountable\, and governable.\n\nThesis Committee\n\nVirginia Smith (Co-chair)\n\nWenting Z heng (Co-chair)\n\nGiulia Fanti\n\nSomesh Jha (University of Wisconsin Mad ison)\n\nAdditional Information\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c74839f 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: \nSpeaker: EDWARD JUSTIN CHEN\, Ph.D. Student\, Computer Scien ce\nDepartment\, Carnegie Mellon University\n\nTalk Title: Democratizing S ecure Computation: Compilers for\nPrivacy-Preserving Programs\n\nAdvanced analytics and machine learning increasingly depend on data\nthat is sensit ive\, regulated\, and distributed across organizations.\nSecure multiparty computation (MPC) and fully homomorphic encryption\n(FHE) offer a path ar ound this barrier by allowing computation over\nprivate inputs without rev ealing the underlying data. Yet despite\ndecades of cryptographic progress \, privacy-preserving computation\nremains difficult to deploy in practice : performance overheads are\nhigh\, and optimization requires expert domai n knowledge.\n\nThis thesis argues that compilers are essential for democr atizing the\nuse of privacy-preserving computation. Rather than requiring\ napplication developers to manually design cryptographic protocols\,\nthis work treats the key performance decisions in MPC and FHE as\nstatic optim ization problems over a program’s intermediate\nrepresentations (IR). Si lph 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 cipher text layouts to tensor\nprograms\, finding efficient packings that minimiz e expensive data\nmovement operations. Orbit is another FHE compiler that also uses ILP\nto jointly place bootstrap and rescale operations by reason ing about\nthe dependencies between ciphertext levels and scales. Together \, these\nsystems show that compiler automation can reduce the expertise\n required to build privacy-preserving applications while improving the\nper formance of the resulting cryptographic programs. The remaining\nwork expl ores an open problem on how AI-driven methods\, such as\nOpenEvolve\, oper ating over compiler IRs  and cost models can discover\nbetter cryptograph ic optimization strategies.\n\nThesis Committee:\n\nWenting Zheng (Co-Chai r)\n\nFraser Brown (Co-Chair)\n\nBryan Parno\n\nAlex Ozdemir (Georgia Inst itute of Technology)\n\nSrini Devadas (Massachusetts Institute of Technolo gy)\n\n \n\nAdditional Information\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c7489df 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: \nSpeaker: TIMOTHY KIM\, Ph.D. Student\, Computer Science Depa rtment\,\nCarnegie Mellon University\n\nTalk Title: Efficient Data Storage Provisioning\, Placement\, and\nTransitions at Scale\n\nExascale storage systems are under increasing pressure to store more\ndata while providing greater performance per byte. Historically\,\nhyperscale storage systems h ave relied on a two-tiered hierarchy:\nhard-disk drives store most bytes\, while smaller flash tiers absorb\nrequests for hot and performance-critic al data. This design is\nbecoming increasingly difficult to sustain. Datac enter data is getting\nwarmer with the proliferation of AI/ML and analytic s-heavy workloads\,\nwhile storage devices are becoming denser without pro portional\nimprovements in per-byte performance or endurance. As a result\ ,\nenabling denser storage devices at exascale requires improving both\nth e software storage system and the hardware provisioning strategies\nfor mo dern datacenter workloads.\n\nThis thesis shows that exascale storage syst ems can enable denser\nstorage options by jointly reducing internal IO and improving data\nplacement/hardware provisioning decisions. The first part of this\nthesis\, Morph\, reduces IO associated with lifetime redundancy\ ntransitions. Morph introduces a novel hybrid redundancy scheme for\nearly -life data and a system designed around a new erasure-code for\nlate-life\ , reducing ingest and transcode overheads. The second part of\nthis thesis develops a total-cost-of-ownership (TCO) model and\noptimizer for exascal e storage provisioning. This model determines the\nminimum-cost set of har dware necessary to serve datacenter workloads\nand shows how heterogeneous configurations can cost-effectively enable\ndense devices in modern datac enters.\n\nWe propose work that connects these two directions by modeling storage\nworkloads from the bottom up\, using fine-grained lifetime and\nt emperature transition behavior to reason about provisioning and\nplacement decisions. By understanding how data cools and survives\nthroughout its l ifetime\, this work aims to produce a more precise\nframework that co-opti mizes the heterogeneous storage mixture and the\nplacement of data across the storage tiers. Together\, these\ncontributions show how storage system s can cost-effectively service\ncontemporary storage workloads with denser media and enable the\nmassive growth in data demand.\n\nThesis Committee\ n\nGreg Ganger (Co-Chair)\n\nRashmi Vinayak (Co-Chair)\n\nGeorge Amvrosiad is\n\nSaurabh Kadekodi (Google)\n\nAdditional Information \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c748f66 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: \nSpeaker: SOPHIA ROSHAL\, Ph.D. Student\, Computer Science De partment\,\nCarnegie Mellon University\n\nTalk Title: Adjoint Types for Fu nctional Programming\n\nSubstructural type systems offer a principled foun dation for reasoning\nabout resource usage by controlling the structural r ules of weakening\,\ncontraction\, and exchange. Linear\, affine\, strict\ , and ordered types\neach enable distinct optimizations and semantic guara ntees. However\,\nsystems restricted to a single structural discipline are often too\nrigid for practical programming\, limiting expressiveness and\ npreventing programs from simultaneously exploiting multiple structural\np roperties.\n\nThis thesis develops Adjoint Types\, a logically founded sub structural\ntype system based on Adjoint Logic\, that supports the princip led\ncombination of multiple substructural modes within a single language. \nThis design preserves the practical expressiveness of an unrestricted\nl anguage\, while still permitting mode based optimizations on the\npieces o f the program that allow them.\n\nThe proposal proceeds in four parts. Fir st\, we present Adjoint Natural\nDeduction\, including both a declarative and algorithmic type system\,\nand establish soundness and completeness wi th respect to a sequent\ncalculus formulation. Second\, we develop a mode inference procedure\nthat supports mode polymorphism and eliminates the ne ed for manual\nmode annotations. Third\, we extend the framework with orde red modes\,\nestablishing decidability for a corresponding type system\, w hile\noutlining ongoing work toward practical type-checking algorithms.\nF ourth\, we propose generalized pattern matching in the adjoint\nsetting\, developing a logically sound approach to nested patterns via\nfocusing and outlining extensions to support wildcards and ordered\nmodes.\n\nTogether \, these contributions establish ordered adjoint types as a\nlogical found ation for substructural functional programming languages\nand logical fram eworks\, enabling structural properties to drive\ncompiler optimizations a nd intensional program behavior without\nsacrificing practical usability.  \n\nThesis Committee:\n\nFrank Pfenning (Chair) \n\nJan Hoffmann\n\nJon athan Aldrich\n\nBrigitte Pientka (McGill University)\n\nChris Martens (No rtheastern University) \n\nAdditional Information\n\nIn-person and Zoom\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c7494c4 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: \nSpeaker: GABRIELE OLIARO\, Ph.D. Student\, Computer Science Department\,\nCarnegie Mellon University\n\nTalk Title: Rethinking the AI Stack: Systems for Agents and Agents for\nSystems\n\nLarge language models have become central infrastructure for modern AI\napplications\, but runn ing them efficiently remains a major systems\nchallenge. Larger and more c apable models require more GPU\ncomputation\, GPUs remain expensive\, and sophisticated applications\nsuch as agents require low latency and predict able service-level\nobjectives to be practically usable. At the same time\ , inference\noptimization increasingly depends on deep specialized experti se in\nscheduling\, memory management\, and GPU kernel engineering. This\n expertise is difficult to scale because model architectures and\naccelerat or platforms evolve rapidly\, introducing new operators\,\nprecision forma ts\, parallelization patterns\, and hardware-specific\noptimization requir ements.\n\nThis thesis develops systems that use model-driven and agentic\ ntechniques to automate parts of this optimization process. SpecInfer\nuse s smaller language models to speculate on the outputs of larger\nmodels\, converting otherwise serial autoregressive decoding into\nparallel verific ation. SuffixDecoding extends this idea to agentic\nworkloads by caching a nd reusing prior generation patterns to\nspeculate with minimal GPU overhe ad. FlexLLM automates fine-grained\nresource allocation between latency-cr itical inference and\nthroughput-oriented finetuning\, allowing both servi ces to share GPUs\nwhile preserving inference service-level objectives. Th e remaining\nwork moves from optimizing inference systems with AI techniqu es to\nusing AI agents to optimize the systems themselves. FastKernels\npr ovides a production-faithful benchmark for LLM-based GPU kernel\nagents\, and the proposed kernel agent will use compiler feedback\,\ncorrectness te sts\, runtime measurements\, and hardware feedback to\ngenerate optimized kernels for rapidly evolving operators such as\nlinear attention\, state-s pace models\, mixture-of-experts routing\,\nquantized inference\, and mult imodal fusion.\n\nThesis Committee\n\nZhihao Jia (Chair)\n\nTianqi Chen\n\ nPhillip Gibbons\n\nHao Zhang (University of California\, San Diego)\n\nAd ditional Information\n\nIn-person & Zoom\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c749a0b 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: \nSpeaker: CARLOS G. MARTIN\, Ph.D. Student\, Computer Science Department\,\nCarnegie Mellon University\n\nTalk Title: Solving infinite games with deep multiagent reinforcement\nlearning\n\nIn this thesis\, we study the problem of solving infinite games. Such\ngames can have infinite ly many states\, actions\, players\, and steps.\nUnlike mean‑field games \, our players need not be symmetric or\nexchangeable. Furthermore\, we al low such games to have partial\nobservability\, hidden information\, imper fect recall\, stochastic state\ntransitions\, discontinuous utility functi ons\, and interdependent\nsocial preferences (i.e.\, matrix-valued discoun t factors). Together\,\nthese properties can model a wide range of highly complex\, real-world\nscenarios that defy traditional game-theoretic solve rs.\n\nTo tackle this problem\, we propose a unified framework grounded in \ndeep multiagent reinforcement learning. It includes five core\ncomponent s.\n\nFirst\, it introduces randomized policy networks (RPNs) to model\nob servation-dependent mixed strategies over infinite action\nspaces.Second\, it represents complex strategy profiles across an\ninfinite continuum of players using player-to-strategy networks\n(P2SNs).Third\, it evolves thes e representations through a\nshared-parameter simultaneous gradient (SPSG) \, which extends the\nstandard simultaneous gradient to this shared-parame ter regime.Fourth\,\nto ensure computational efficiency\, it estimates thi s gradient using\nrandomized parameter perturbations via a joint-perturbat ion\nsimultaneous pseudo-gradient (JPSPG).Fifth\, it employs approximate\n exploitability descent (ApproxED) with learned best-response functions\n(B RFs).\n\nWe propose to benchmark our approach on a diverse suite of real-w orld\ndomains. These include financial markets\, traffic flow\,\nepidemiol ogical contagion\, energy grids\, and evolutionary ecology.\n\nThesis Comm ittee:\n\nTuomas Sandholm (Chair)\n\nVincent Conitzer\n\nFei Fang\n\nIan G emp (Google)\n\nAdditional Information\n\nIn-person and Zoom\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c749f44 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: \nSpeaker: NOAH G. SINGER\, Ph.D. Student\, Computer Science D epartment\,\nCarnegie Mellon University\n\nTalk Title: Expansion of coset complexes and applications\n\nIn computer science and discrete mathematics \, a hypergraph is a\ncollection of subsets of a set of vertices\; in part icular\, a graph is\na collection of (unordered) pairs of vertices. Graphs are used to\nencode pairwise relationships between objects\, and hypergra phs to\nencode more general multi-way relationships.\n\nHigh-dimensional e xpanders are\, informally\, hypergraphs which are\n\"well-connected\" in a quantitative sense. While expansion in the\n\"low-dimensional\" case of g raphs has been studied intensively since\nthe 1970s\, high-dimensional exp anders have recently gained visibility\nfor their role in a number of theo retical breakthroughs\, such as the\nconstruction of efficient sampling al gorithms for spanning trees\n(Anari–Liu–Oveis Gharan–Vinzant\, STOC 2019\, Ann. Math. 2024)\,\noptimal locally testable codes\n(Dinur–Evra –Livne–Lubotzky–Mozes\, STOC 2022)\, and efficient\nlow-soundness PC Ps (Bafna–Minzer–Vyas\, STOC 2025).\n\nKaufman and Oppenheim (STOC 201 8\, Eur. J. Comb. 2023) gave a\nremarkably simple construction of high-dim ensional expanders by using\ncarefully chosen groups of matrices to instan tiate a classical\nconstruction known as a \"coset complex\". In this thes is\, we further\ninvestigate the expansion of these complexes and various\ ngeneralizations\, as well as applications of this expansion in computer\n science and mathematics.\n\nIn two preliminary works (joint with Ryan O’ Donnell)\, we:\n\nInvestigated a particular notion of high-dimensional exp ansion\n(\"1-cosystolic expansion\") on certain generalized KO complexes b y\ncombining intricate group-theoretic arguments with computer-assisted\nm atrix rank calculations.Showed that KO complexes have a\n\"low-soundness a greement testing\" property which allows them to be\nused inside the PCP o f Bafna et al.\, replacing a much more complicated\nconstruction.\n\nIn th is proposal\, we propose several additional directions for the\nPh.D. thes is. These include:\n\nUsing the KO complex to improve the complexity of th e Bafna et al. PCP\n(e.g.\, the verifier or prover runtimes)\,systematical ly characterizing\nthe coboundary and cosystolic expansion of generalizati ons of KO\ncomplexes\; andimproving existing constructions of agreement te sters by\nusing alternative kinds of tests.\n\nThesis Committee:\n\nRyan O 'Donnell (Chair)\n\nAayush Jain\n\nYang P. Liu\n\nIrit Dinur (Institute fo r Advanced Study)\n\nMadhur Tulsiani (Toyota Technological Institute at Ch icago &\nUniversity of Chicago)\n\nAdditional Information\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c74a54a 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: \nSpeaker: ZHENGYAO LIN\, Ph.D. Student\, Computer Science Dep artment\,\nCarnegie Mellon University\n\nTalk Title: Verifying Asynchronou s Dataflow Compilers\n\nThe paradigm of asynchronous dataflow circuits\, i n which parallel\noperators are dynamically scheduled and data-driven\, un locks\nsubstantial energy efficiency and performance gains in reconfigurab le\ndataflow architectures (RDAs) and dynamic high-level synthesis (HLS)\n toolchains. A key challenge hindering their mainstream adoption is the\ndi fficulty of correct\, efficient\, and general-purpose compilation\ntowards asynchronous dataflow.\n\nIn this proposal\, I present my efforts to appl y formal verification to\nasynchronous dataflow\, with the goal of develop ing an end-to-end\,\nprovably correct dataflow compilation pipeline.\n\nTh esis Committee:\n\nBryan Parno (Chair)\n\nStephanie Balzer\n\nRuben Martin s\n\nBrandon Lucia\n\nMilijana Surbatovich (University of Maryland\, Colle ge Park)\n\nAdditional Information\n\nIn-person and Zoom\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c74a989 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: \nSpeaker: LINGJING KONG\, Ph.D. Student\, Computer Science De partment\,\nCarnegie Mellon University\n\nTalk Title: Causal AI for Transf erable\, Interpretable\, and\nControllable Machine Learning\n\nFoundation models are rapidly becoming capable assistants for\nknowledge work\, but t heir deployment in real settings is limited by\nthree gaps: they do not tr ansfer reliably across environments\, their\ninternal reasoning is opaque\ , and their behavior is hard to control\nprecisely. In this talk\, I argue that these limitations are not only\nabout model size — they are fundam entally about whether learning\ncaptures and leverages the underlying stru cture of the data-generating\nprocess. I use causal thinking as a practica l lens to model what is\ninvariant\, what changes\, and what can be interv ened on\, and I further\nshow how this leads to learning principles that i mprove\ntrustworthiness. I will first present methods for learning unifyin g\nmechanisms from heterogeneous data\, across domains and modalities\, to \nenable reliable transfer and controllable generation. Next\, I will\nsho w how structured concepts can be recovered even from seemingly\nunstructur ed data\, by analyzing and improving self-supervised\nobjectives (such as masking and diffusion) through hierarchical\nlatent-variable models. These concept structures can then be used to\ninterpret generative models and s upport targeted\, multi-level edits.\nFinally\, I connect these two thread s to generalization beyond the\ntraining distribution. I will discuss natu ral conditions for\nextrapolation and a compositional generation framework that improves\nprompt following for novel concept combinations. I will co nclude with\na brief outlook on self-improving world models.\n\nThesis Com mittee:\n\nKun Zhang (Co-chair)\n\nYuejie Chi (Co-chair)\n\nEric Xing (Co- chair)\n\nTom Mitchell\n\nKevin Murphy (Google DeepMind)\n\nAdditional Inf ormation \n\nIn-person and Zoom \n\n \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c74fa80 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: \nSpeaker: KEVIN KUO\, Ph.D. Student\, Computer Science Depart ment\,\nCarnegie Mellon University\n\nTalk Title: Algorithms for Efficient and Safe Collaborative Learning\nSystems\n\nData for AI systems is becomi ng increasingly sparse. Within a decade\,\nLLMs are projected to be traine d on datasets the size of the total\nstock of public human data\, while in dividuals and organizations are\nincreasingly restricting access to their data due to economic and\nprivacy concerns. Collaborative learning has the potential to fuel\ndata-hungry AI systems by enabling access to restricte d sources of\ndata---but only if it can provide meaningful guarantees rega rding data\nprivacy\, quality of service\, and computational cost. This th esis\nstudies three unique ML system architectures that offer data\nprotec tion by design: (1) multi-round federated learning\, (2) model\nmerging-an d-localization\, and (3) proxy tuning. We leverage principles\nfrom model compression and transfer learning to improve the utility\,\nefficiency\, a nd privacy guarantees of these frameworks.\n\nThesis Committee:\n\nVirgini a Smith (Chair)\n\nAditi Raghunathan\n\nGauri Joshi\n\nHolger Roth (NVIDIA )\n\nAdditional Information\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c75014e 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: \nSpeaker: SAGAR BHARADWAJ KALASIBAIL SEETHARAM\, Ph.D. Studen t\, Computer\nScience Department\, Carnegie Mellon University\n\nTalk Titl e: OpenFLAME: Federated Spatial Intelligence\n\nSpatial applications\, i.e .\, applications that tie digital information\nwith the physical world\, h ave improved many of our daily activities\,\nsuch as navigation and ride-s haring. This class of applications also\nholds significant promise of enab ling new industries such as augmented\nreality and robotics. The developme nt of these applications is enabled\nby spatial intelligence systems\, or systems that can provide\nphysically-grounded services such as routing\,  spatial search\, and\nlocalization. Today\, mapping platforms provided b y organizations like\nGoogle and Apple serve as spatial intelligence syste ms. These maps are\ncentralized and primarily cover outdoor spaces. We env ision that\nfuture spatial applications\, such as persistent world-scale a ugmented\nreality and robotics\, would require detailed and precise spati al\nintelligence across indoor and outdoor spaces. The scale of\ncartograp hy efforts required to survey indoor spaces and their privacy\nneeds inhib it existing centralized maps from incorporating such spaces\ninto their pl atform.\n\nThis thesis proposes the design and implementation of OpenFLAME \, a\nfederated spatial intelligence platform built on two core pillars.\n First\, it introduces a federated mapping infrastructure where\nindependen t parties can manage and serve their own maps of physical\nregions. This u nlocks scalability of map management\, isolation\, and\nprivacy of maps. T his is implemented on top of the existing Domain\nName System (DNS)\, whi ch enables us to leverage its existing\ninfrastructure. Second\, it explor es the development of spatial\nservices\, such as search\, routing\, and l ocalization\, by transforming\nraw spatial data (e.g.\, images and videos) of a space into structured\,\nqueryable maps that support these capabilit ies.\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:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c7508a2 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: \nSpeaker: ZHIBO CHEN\, Ph.D. Student\nComputer Science Depart ment\nCarnegie Mellon University\n\nTalk Title: CoLF - A Coinductive Logic al Framework\n\nThe LF logical framework represents judgments as types\, a nd objects\nand derivations as finitary terms. Twelf\, an implementation o f LF\, is\na metalogical framework that incorporates metatheorem checking and a\nlogic programming engine. There is no direct encoding of infinitary \nobjects and derivations in LF and Twelf. In this thesis\, we propose a\n new logical framework CoLF\, building on top of LF\, for encoding\ninfinit ary objects and derivations as infinitary terms. We develop\nthe type the ory and implementation of CoLF. We also propose to\ninvestigate the metath eoretic reasoning principles and a new logic\nprogramming semantics in the presence of infinitary terms.\n\nThesis Committee\n\nFrank Pfenning (Chai r)\n\nKarl Crary\n\nIliano Cervesato\n\nAlberto Momigliano (University of Milan)\n\nAdditional Information \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c750d6b 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: \nSpeaker: BERNARDO SUBERCASEAUX\, Ph.D. Student\nComputer Sci ence Department\nCarnegie Mellon University\n\nTalk Title: SAT Encodings: From Art to Science\n\nAutomated reasoning engines\, and SAT solvers in pa rticular\, have\nbecome a powerful tool for tackling hard combinatorial pr oblems. While\nSAT solvers have improved dramatically\, their effectivenes s still\ndepends critically on how problems are encoded into conjunctive n ormal\nform (CNF). Encoding choices routinely account for runtime differen ces\nof several orders of magnitude\, yet their design remains more art th an\nscience—guided by intuition and hard-won experience rather than a\np rincipled theory. This thesis aims to shed light on the design of\neffecti ve SAT encodings\, from both practical and theoretical\nperspectives.\n\nT he first part is dedicated to the art of encodings. We show how\nclever pr oblem-specific encodings\, together with other automated\nreasoning techni ques\, have allowed us to solve a variety of open\nproblems in discrete ma thematics ranging from graph coloring to\ndiscrete geometry. These encodin gs benefit from mathematical insights\nincorporated via additional constra ints 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 bet ween automated\nreasoning and discrete mathematics. We also apply this art to\ncomputational problems in explainable AI—uncovering patterns in\nde cision trees\, nearest-neighbor classifiers\, and other symbolic\nmodels —demonstrating the transferability of our techniques beyond\nmathematics .\n\nThe second part is dedicated to the foundations of a science of\nenco dings. We present a landscape of theoretical results regarding the\nnumber of clauses and auxiliary variables required to encode several\nbuilding b locks of propositional encodings\, from cardinality\nconstraints to arbitr ary k-CNF functions. We posit that encoding\nboolean functions into CNF wi th as few clauses as possible offers a\nfascinating yet largely unexplored territory for circuit complexity.\nBy leveraging auxiliary variables and wide clauses\, this\nclause-minimization model permits rich combinatorial structures that\nsurpass known lower bounds for circuits. Furthermore\, wh ile\nclause-minimization does not always correlate with solver performance \,\ntheoretical developments in this model have led us to novel encodings\ nthat run faster on practical problems. More broadly\, this thesis aims\nt o establish that the clause-minimization model is not only an elegant\nthe ory\, but also a realistic path towards empirical speedups.\n\nThesis Comm ittee\n\nMarijn Heule (Chair)\n\nJeremy Avigad\n\nRuben Martins\n\nStefan Szeider (Technische Universität Wien)\n\nRyan Williams (Massachusetts In stitute of Technology)\n\nAdditional Information \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c751515 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: \nSpeaker: ANDREW PARK\, Ph.D. Student\nComputer Science Depar tment\nCarnegie Mellon University\n\nTalk Title: Attacking and Designing S ecure Protocols for Database\nSearch\n\nThe increasing reliance on outsour ced storage and cloud-based\ncomputing has made database accesses a fundam ental problem in modern\nsecurity and cryptography. At its core\, the chal lenge of accessing\ndatabases securely is to enable efficient query proces sing over a\n(potentially encrypted) database without leaking private info rmation\nto untrusted parties. Large lines of work have yielded a plethora of\ndifferent solutions such as searchable encryption\, private informati on\nretrieval (PIR)\, and oblivious RAM (ORAM)\, each offering various\ntr adeoffs among efficiency\, functionality\, and privacy. However\, these\ns olutions have yet to find wide-scale adoption due to practical\ninefficien cies. In addition\, their real-world implementations often\ncontain subtle leakage of the underlying private data.\n\nThis dissertation develops a u nified perspective on secure database\nsearch by studying both attacks and designs of new secure protocols\nfor database search. On the attack side\ , we design and implement a\nframework\, Polysys\, for modeling and analyz ing leakage patterns. This\nresult demonstrates an empirical understanding of how theoretical\nprivacy guarantees behave in practice.\n\nOn the cons truction side\, we introduce new protocols for both PIR and\nORAM to motiv ate more real-world adoption of these protocols. For PIR\,\nwe design nove l communication-efficient\, fault-tolerant multi-server\nschemes that also support erasure-coded storage\, providing robustness\nagainst fail-stop o r Byzantine servers. For ORAM\, we present two new\ndesigns for different workload settings. First\, we design a garbled\nRAM (GRAM) scheme which ma tches the interactive state of the art\nscheme and achieves practical impr ovement against the prior state of\nart. Finally\, we propose to construct distribution-aware ORAM schemes\,\nwhich provides ORAM-like security prop erties for a set distribution\nwhile providing better practical efficiency .\n\nOur results highlight the importance of accounting for leakage in\nre al-world settings and considering real-world limitations when\ndesigning s ecure protocols.\n\nThesis Committee\n\nElaine Shi (Co-chair)\n\nWenting Z heng (Co-chair)\n\nAayush Jain\n\nSeny Kamara (MongoDB)\n\nTarik Moataz (M ongoDB)\n\nAdditional Information \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c751d2f 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: \nSpeaker: YONGHAO ZHUANG\, Ph.D. Student\nComputer Science De partment\nCarnegie Mellon University\n\nTalk Title: On Efficient Language Model Post Training with Attention\nDisaggregation\n\nToday's LLM training introduces more stages to further improve the\nmodel quality\, and post-t raining is the most important. Despite the\nlong-context workload imbalanc e\, post-training includes reinforcement\nlearning (RL)\, which iterativel y runs the \"rollout generation - reward\nevaluation - policy update'' pip eline.\n\nThis thesis proposes the concept of attention server\, where the main\npart of attention (core attention) is disaggregated from other\ncom ponents 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 k ernel only needs a subset of the GPU resources to saturate\nits memory ban dwidth demand\, allowing the GPU to utilize the remaining\nresources for c ompute intensive tasks.\n\nThesis Committee\n\nEric Xing (Chair)\n\nTianqi Chen\n\nZhihao Jia\n\nIon Stoica (University of California\, Berkeley)\n\ nHao Zhang (University of California\, San Diego)\n\nAdditional Informatio n\n\nIn Person and Zoom Participation.  See announcement. \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c75dcd0 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: \nSpeaker: SAM ARCH\, Ph.D. Student\nComputer Science Departme nt\nCarnegie Mellon University\n\nTalk Title: Leveraging Optimization-Enab ling Properties of\nUser-Defined Functions for Efficient Database Query Ex ecution\n\nAfter decades of research\, analytical database management syst ems\n(DBMSs) have become remarkably effective at optimizing and executing\ nSQL queries. However\, many users write queries that are not written\nent irely in SQL. Instead\, these queries invoke user-defined functions\n(UDFs )\, external functions written in non-SQL programming languages\nsuch as P ython or PL/SQL. UDFs provide software engineering benefits\nby enabling c ode reuse and by extending the DBMS’s capabilities to\ninclude those of the UDF language. However\, UDFs are inherently\nnon-relational\, which ma kes them challenging for DBMSs to reason about\nand execute efficiently. E ffective optimization is also challenging\nbecause UDF languages are Turin g-complete\, allowing UDFs to be\narbitrarily complex. Although general-pu rpose optimization techniques\ncan improve UDF performance (e.g.\, compila tion and batching)\, they\ntarget arbitrary UDF code and therefore have li mited effectiveness. We\nobserve that the most beneficial UDF optimization s (e.g.\, memoization\nand inlining) leverage key optimization-enabling pr operties of UDFs\n(i.e.\, how users actually use them in practice).\n\nIn this proposal\, we present multiple techniques that leverage\noptimization -enabling properties of UDFs to improve database query\nexecution performa nce. First\, we observe that inlining only the\nrelevant pieces of a UDF i mproves performance\, and leverage UDF\ndecomposability to break UDFs into pieces and hide irrelevant pieces\nthrough outlining. Next\, we observe t hat processing all unique UDF\ninputs simultaneously improves parallelism\ , and leverage UDF\nredundancy to build lightweight indexes during query p rocessing to\navoid repeated UDF invocations.\n\nWe propose extending our preliminary work by observing that enabling\ninter-tuple parallelism of UD Fs improves query execution performance.\nWe plan to leverage UDF pipelini ng\, the observation that UDFs operate\nas a pipeline of data transformati ons over their inputs\, to enable\nfusion and auto-vectorization of pipeli ne stages. Collectively\, the\ntechniques presented in this dissertation w ill enable an analytical\ndatabase system to execute queries that contain UDF calls efficiently.\n\nThesis Committee\n\nAndrew Pavlo (Co-Chair)\n\nT odd C. Mowry (Co-Chair)\n\nJignesh Patel (Co-Chair)\n\nPhillip B. Gibbons\ n\nJoseph M. Hellerstein (University of California\, Berkeley)\n\nAddition al Information\n\nIn Person and Zoom Participation.  See announcement. \ n\n \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c75e4a4 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: \nSpeaker: YASH SAVANI\, Ph.D. Student\nComputer Science Depar tment\nCarnegie Mellon University\n\nTalk Title: Controlled Generation of Foundation Models for Training\n\nThis thesis proposal presents controlled generation methods for\nfoundation models\, focusing on gradient-based st eering to improve\ntraining and robustness. For diffusion and flow models\ , I introduce\nDiffusing Differentiable Representations (NeurIPS 2024)\, w hich guides\nthe training of differentiable representations\, such as Neur al\nRadiance Fields\, by pulling back the score function through the\ndiff erentiable render function. I also present work with Adobe\nResearch on te mporal credit assignment for policy gradient methods\,\nenabling more effe ctive training of flow models via GRPO-style\nreinforcement learning. \n\ nFor large language models\, I present two methods for controlled\ngenerat ion. The first maximizes resource utilization in GRPO-style\nreinforcement learning by selectively dropping low-variance\ntrajectories (in submissio n). The second\, Antidistillation Sampling\n(NeurIPS 2025)\, steers genera tion to defend against distillation\nattacks using precomputed proxy gradi ents. Together\, these\ncontributions establish a unified framework for co ntrolled generation\nacross modalities\, with applications spanning creati ve content\nsynthesis\, model protection\, and efficient training.\n\nThes is Committee\n\nJ. Zico Kolter (Chair)\n\nAviral Kumar\n\nNicholas M. Boff i\n\nKrishna Kumar Singh (Adobe Research)\n\nAdditional Information\n\nIn Person and Zoom Participation.  See announcement. \n\n \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c75ea95 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: \nSpeaker: JOSHUA CLUNE\, Ph.D. Student\, Computer Science Dep artment\,\nCarnegie Mellon University\n\nTalk Title: Leveraging Automated Theorem Provers for Lean Proof\nAutomationThis proposal discusses work tha t builds towards the\ncreation of a hammer for the Lean interactive theore m prover. Said\nwork includes the development of a proof-producing superpo sition\ntheorem prover for Lean\, a tool which interfaces with the cvc5 SM T\nsolver to produce self-contained Lean proof scripts\, and a neural\npre mise selection system. The proposal culminates in the description\nof a pr eliminary hammer for Lean along with discussion of how to\nrefine and impr ove it into a more powerful and robust tool.\n\nThesis Committee:\n\nJerem y Avigad (Chair)\n\nMarijn Heule\n\nBryan Parno\n\nHaniel Barbosa (Univer sidade Federal de Minas Gerais)\n\nIn-person and Zoom\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c75eedd 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: \nSpeaker: ZHIHAO ZHANG\, Ph.D. Student\, Computer Science Dep artment\,\nCarnegie Mellon University\n\nTalk Title: A Path Towards Effici ent Large Language Model Deployment\nthrough Algorithm and System Co-Desig n\n\nRecent advancements in large language models have shown promising\nre sults in diverse downstream tasks by training and test time scaling.\nHowe ver\, the fast-paced development of large models has posed\nsignificant ch allenges to their energy cost and efficient\ndeployment. \n\nTo achieve t his\, my thesis topic is centered around bridging the gap\nbetween the alg orithm-system co-design space for better large model\ndeployment. More spe cifically\, through:\n\nhardware-guided algorithmic explorations for effic ient large language\nmodel inference\, and LLM inference-specific system optimizations to\nfully exploit hardware utilization. \n\nFor algorithmic improvements\, I will present two lines of research\nprojects on Speculat ive Decoding (SpecInfer\, RaLMSpec) and Sparse\nAttention (TidalDecode\, L essisMore).\n\nFor system optimizations\, I will present one project on LL M deployment\nwith MegaKernel (MPK) and one ongoing project that is focusi ng on\ngeneralizing the megakernel runtime to support multi-LLM\ndeployme nt. \n\nBenefiting from the algorithm-system co-optimizations\, the propo sed\nthesis topic is expected to provide an effective solution for reducin g\nthe energy cost and improving the efficiency of LLM deployment in the\n real world.\n\nThesis Committee\n\nZhihao Jia (Chair)\n\nTianqi Chen\n\nDi mitrios Skarlatos\n\nRavi Netravali (Princeton University)\n\nAdditional I nformation\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c75f3df 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: \nSpeaker: MYRA DOTZEL\, Ph.D. Student\nComputer Science Depar tment\nCarnegie Mellon University\n\nTalk Title: Logical Foundations of In termittent Computing\n\nIntermittent computing is gaining popularity in ap plications that rely\non batteryless energy-harvesting devices which exper ience frequent and\narbitrary power failures. To enable correct program re -execution\ndespite these potentially frequent and arbitrary power failure s\,\nruntime support is needed to save and restore necessary state. \n\nI n this talk\, we study the formal foundations of intermittent\ncomputing b y use of type systems to guarantee the correctness of\nprograms prior to t heir deployment\, and runtime systems to facilitate\ncorrect program execu tion\, including support for sequential and\nconcurrent models of executio n. \n\nFirst\, we explore the logical underpinning of sequential\, interm ittent\ncomputing and model checkpoint\, crash\, restore\, and re-executio n\noperations as computation on crash types. We draw inspiration from\nadj oint logic to reason about the relationship between persistent and\ntransi ent memories through (re-)execution\, checkpointing\, and\nrestoration. Us ing crash types\, we show that any correct intermittent\nexecution can be simulated by a continuously-powered execution.\n\nSecond\, we present the first provably-correct system for concurrent\,\nintermittent program execu tion\, which is needed as many embedded\napplications rely on interactions with hardware-triggered interrupts\nand accesses to shared memory. Prior work on concurrent\, intermittent\nexecution has only provided restrictive programming models with no\nformal correctness guarantees. In this talk\, we present a co-designed\nruntime system and type system that together su pport the provably\ncorrect intermittent execution of task-based concurren t programs with\nshared memory. This system promotes a more flexible progr amming model\nand supports a broader spectrum of task re-execution behavio rs than is\nconsidered by prior work. We provide the first formal definiti on and\nproofs of correctness for concurrent\, intermittent execution.    \n\nThesis Committee\n\nLimin Jia (Co-chair)\n\nFarzaneh Derakhshan (Co- chair\, Illinois Institute of Technology)\n\nFrank Pfenning \n\nJan Hoffm ann \n\nBrigitte Pientka (McGill University) \n\n \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c75f938 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: \nSpeaker: KAIYANG ZHAO\, Ph.D. Student\nComputer Science Depa rtment\nCarnegie Mellon University\n\nTalk Title: Architecting Memory Effi ciency in Modern Datacenters\n\nThe proliferation of memory-intensive appl ications\, the rapid\nexpansion of memory capacity to terabyte scales\, an d the slowing of\nDRAM cost scaling have established memory as the critica l bottleneck\nin modern datacenter computing. This inefficiency manifests in two\ndimensions: the cycle efficiency lost to the virtual memory\nabstr action and the escalating financial cost of memory.\n\nFirst\, the virtual memory abstraction is under increasing strain. As\nmemory capacity grows while Translation Lookaside Buffer sizes remain\nstagnant\, address transl ation overhead becomes severe\; internal\nprofiling at hyperscalers reveal s that approximately 20% of CPU cycles\nare stalled on TLB misses. This ov erhead is bound to worsen due to\ninherent TLB scaling limits\, the introd uction of additional page table\nlevels\, vast heterogeneous memory capaci ty\, and the page-level\nsecurity checks required by confidential computin g. Second\, the\nfinancial cost of memory has skyrocketed. Memory now acco unts for\nnearly a quarter of rack power consumption and half of the Total Cost\nof Ownership of a typical datacenter server. In this proposal\, I\n address these challenges through a set of operating system and\narchitectu ral designs.\n\nTo improve cycle efficiency\, I present two completed work s.\nContiguitas creates abundant physical memory contiguity by grouping\nu nmovable allocations in the OS and introducing hardware extensions to\nmig rate pages previously locked for device I/O. This contiguity is\nleveraged to allocate huge pages\, reducing translation overhead and\nyielding up t o 18% performance improvement for production workloads.\nLearned Virtual M emory (LVM) replaces rigid radix page tables with\nlearned indexes tailore d to the application's virtual address space.\nBy leveraging address space regularity\, LVM reduces page walk overhead\nby an average of 44% and ach ieves a 2–27% speedup in execution.\n\nTo improve cost efficiency\, I pr esent two ongoing works. Multi-Tier\ndynamically manages pages across DRAM \, CXL memory\, and SSDs to\nmaximize financial savings by utilizing cheap er tiers within a defined\nperformance loss limit. Equilibria addresses th e challenges of\nmulti-tenant tiering\, ensuring fair memory sharing and m itigating\nnoisy-neighbor interference through flexible placement policies and\nthrashing mitigation.\n\nTogether\, these works provide a comprehens ive solution to improving\nmemory efficiency in datacenters from the persp ectives of both cycle\noverhead and financial cost.\n\nThesis Committee\n\ nDimitrios Skarlatos (Chair)\n\nPhil Gibbons\n\nTodd Mowry \n\nKim Keeton (Google) \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c75fff4 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: \nSpeaker: CAYDEN CODEL\, Ph.D. Student\nComputer Science Depa rtment\nCarnegie Mellon University\n\nTalk Title: Building a Verified SAT Toolchain in Trestle\n\nAutomated reasoning (AR) tools are versatile and p ractically efficient\npieces of software that can solve a wide variety of problems in\nindustry and academia. One of their strengths is their abilit y to\ngenerate proofs checkable by verified software. Even if the AR tools \nthemselves contain bugs (and they often do)\, we can still have a high\n degree of confidence in the correctness of their answers.\n\nHowever\, thi s verified toolchain can be extended further to include\nencodings. Usuall y\, AR tools solve problems that have been encoded\ninto a form that they can understand. This process of encoding can\nintroduce bugs\, meaning tha t the encoded form of the problem no longer\naccurately represents the ori ginal. Bugs are more likely to appear\nwhen the encoding is more complicat ed\, such as when auxiliary logical\nobjects are introduced in order to ma ke the encoding smaller or easier\nfor the AR tool to manipulate. Unfortun ately\, complicated encodings\nare becoming increasingly necessary in orde r to push the boundaries of\nwhat problems AR tools can solve. As a result \, we argue that the\nstandard AR toolchain should now include verified en codings by\ndefault.\n\nIn this thesis\, we will develop an end-to-end ver ified toolchain for\nthe boolean satisfiability problem (SAT) in the Trest le project.\nTrestle currently has a verified SAT proof checker and good s upport\nfor writing verified encodings\, but its encoding tools are compli cated\nand hard to use\, and only a handful of encodings have been verifie d so\nfar. As a result\, we plan to redesign how encodings are written in\ nTrestle\, and to verify new encodings. We also plan to add\nsymmetry-brea king reasoning to Trestle and add features to enable\nend-to-end theorem p roving with the use of SAT solvers.\n\nThesis Committee\n\nMarijn Heule (C hair)\n\nJeremy Avigad\n\nBryan Parno\n\nBenjamin Kiesl-Reiter (Amazon Web Services)\n\nAdditional Information\n\nIn Person and Zoom Participation.   See announcement. \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c76076a 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: \nSpeaker: SARANYA VIJAYAKUMAR\, Ph.D. Student\nComputer Scien ce Department\nCarnegie Mellon University\n\nTalk Title: Protection Bounda ry Integrity: Detecting and Preventing\nSecurity Failures Across Contexts\ n\nModern computational systems deploy technical guardrails to enforce\nse curity\, privacy\, and safety boundaries across increasingly complex\noper ational contexts. While effective within their design contexts\,\nthese me chanisms exhibit systematic vulnerabilities when systems\ntransition betwe en different operational modes: across interaction\nmodalities\, through t emporal evolution\, or when integrating neural and\nsymbolic reasoning. Th is dissertation investigates where\, how\, and why\nsecurity mechanisms fa il at these critical transitions.\n\nFirst\, I demonstrate patterns of bou ndary failure through empirical\nanalysis across multiple domains. My cros s-modal work evaluates such\nfailures in browser-agent safety auditing (Br owserART) and\nauthenticity detection of AI-generated code (CodeFusion). T hrough\nBrowserART\, I show that language models refusing harmful instruct ions\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\n authenticity boundaries require reasoning across representational\nmodalit ies. Second\, I identify temporal vulnerabilities that emerge\nwhen securi ty mechanisms designed for static analysis cannot adapt to\nevolving threa ts. I demonstrate this through MalCentroid\, tracking\nmalware family evol ution while maintaining robustness against\nadversarial obfuscation\, and through graph-based fraud detection\nsystems identifying attack patterns e merging across temporal\ntransaction sequences. Through TRACE\, I achieve successful\nre-identification against Google's Topics API by exploiting\nv ulnerabilities where privacy mechanisms protecting individual\nobservation s fail when adversaries analyze sequential behavioral\npatterns.\n\nFinall y\, I introduce methods to bridge neural-symbolic security\nboundaries. Th rough SMTLayer\, I integrate satisfiability solvers\ndirectly into neural architectures\, achieving substantial data\nefficiency improvements while maintaining formal logical guarantees.\nIn my proposed work\, I introduce verifiable protection mechanisms for\nlanguage models through a game-theor etic prover-verifier framework and\ndevelop multiplicative gating architec tures enabling efficient\nlearning of complex logical structures like XOR gates that standard\narchitectures struggle to represent. This research pr ovides\nfoundations for building protection mechanisms that maintain integ rity\nacross the complex operational transitions required for safe\ndeploy ment of autonomous computational systems.\n\nThesis Committee\n\nChristos Faloutsos (Co-Chair)\n\nMatt Fredrikson (Co-Chair)\n\nSarah Cen\n\nMihai C hristodorescu (Google Research)\n\nAdditional Information \n\n \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c760fcf 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: \nSpeaker: NICOLE FENG\, Ph.D. Student\nComputer Science Depar tment\nCarnegie Mellon University\n\nTalk Title: Robust Algorithms for Win ding Numbers and Signed Distance\n\nThis thesis presents robust algorithms for inside-outside computation\nand curve reconstruction (via winding num bers) and signed distance\ncomputation. These algorithms make geometric in ferences from imperfect\ndata\, where such imperfect data includes noisy\, incomplete\, or\ninaccurate observations or representations of shapes tha t result from\neither acquisition or authoring of geometry. A theme is tha t\nrobustness and versatility can often be achieved by processing smooth\, \nglobally-defined functions encoding the geometry of interest\, that are\ nmore amenable to robust computation than the original\, defective curve\n or surface. For both inside-outside and signed distance computation we\nca n unlock further control over geometry and topology by processing\nhigher- order derivatives of these functions. In many cases\, we can\nalso re-cast our algorithms\, formulated in terms of smooth functions\,\nonto differen t discretizations and geometric data structures. Another\ntheme is that ro bust reconstruction and robust signed distance\ncomputation are closely re lated problems\; towards this end\, we provide\na formalization of their r elationship that justifies the design of our\nalgorithms.\n\nThesis Commit tee\n\nKeenan Crane (Chair)\n\nIoannis Gkioulekas\n\nNancy Pollard \n\nCh ris Wojtan (Institute of Science and Technology Austria)\n\nAdditional Inf ormation \n\n \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c76154b 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: \nSpeaker: HONGHAO LIN\, Ph.D. Student\nComputer Science Depar tment\nCarnegie Mellon University\n\nTalk Title: Advances in Algorithms fo r Massive Data: Optimal Bounds\,\nAdversarial Robustness\, and Data-Driven Insights\n\nWith the rapid growth of massive datasets in areas such as ma chine\nlearning and numerical linear algebra\, classical algorithms are of ten\nno longer feasible. In this thesis proposal\, we develop provably\nef ficient algorithms for various problems in these settings\, such as\nstrea ming and distributed model. Our contributions span three\ndirections:\n\nO ptimal Bounds. We introduce a general technique for lifting dimension\nlow er bounds for real-valued linear sketches to polynomially bounded\ninteger inputs. This leads to the first optimal sketching lower bounds\nfor discr ete data streams in fundamental problems such as frequency\nmoment approxi mation\, operator norm estimation\, and compressed\nsensing. Beyond this\, we also establish nearly-optimal bounds for a\nvariety of streaming and s ketching tasks\, including ℓ p subspace\nsketches for constant dimensio n d\, ℓ p regression in the\narbitrary-partition distributed model\, a nd graph problems such as\napproximating the minimum cut and constructing cut sparsifiers in\nbalanced directed graphs.Adversarial Robustness. While most streaming\nalgorithms are studied in static worst-case models\, many practical\nscenarios involve adaptive adversaries who generate inputs bas ed on\nprevious outputs. We present the first adaptive attack against line ar\nsketches for ℓ p-estimation over turnstile integer streams.\nSpecif ically\, we show that any linear streaming algorithm with\nsketching matri x A ∈ ℤrxn can be broken using only poly(r log n)\nqueries\, with high constant probability. This result highlights\nfundamental limits of robus tness in adaptive streaming. Learning-based\nAlgorithms. Classical algorit hms guarantee correctness in the worst\ncase but often ignore structure in real-world data\, while machine\nlearning methods leverage structure but typically lack guarantees. We\ndesign learning-based algorithms that incor porate machine learning\npredictions to adapt to input distributions\, ach ieving faster\nruntimes\, reduced space\, or improved accuracy. Crucially\ , these\nalgorithms retain rigorous worst-case guarantees even when the\np redictions are imperfect\, bridging the gap between theory and\ndata-drive n practice.  \n\nThesis Committee\n\nDavid P. Woodruff (Chair)\n\nYang P . Liu \n\nRichard Peng\n\nJelani Nelson (University of California\, Berke ley)\n\nIn Person and Zoom Participation.  See announcement. \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c761aea 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: \nSpeaker: WILLIAM ZHANG\, Ph.D. Student\nComputer Science Dep artment\nCarnegie Mellon University\n\nTalk Title: On Holistic Database Op timization via Leveraging\nSimilarity Across Actions\, Workloads\, Configu rations\, and Scenarios\n\nModern database management systems (DBMSs) have evolved to support\nincreasingly sophisticated data-intensive application s\, at the cost of\nsubstantial complexity to configure them for two reaso ns. First\, DBMSs\nexpose a vast configuration space with trillions of pos sibilities that\nencompass system knobs\, physical design (e.g.\, indexes) \, and query\noptions\, amongst others. Second\, these applications are co nstantly\nevolving with changes in data access patterns\, query types\, lo ad\nintensities\, hardware\, and data distributions that necessitate\ncont inuous re-optimization.\n\nTo address these challenges\, decades of autono mous DBMS optimization\nresearch have produced specialized tuning tools to assist human\noperators. Deploying these tools involves a complex multi-s tep\nworkflow where an operator (1) observes the DBMS’s behavior\, (2)\n selects tools based on the objectives and their expertise\, (3)\nconfigure s them with an isolated environment\, (4) orchestrates their\nexecution to obtain recommendations\, and (5) reviews those\nrecommendations before de ployment. This cumbersome process results in\nsuboptimal configurations an d slow adaptation to evolving\napplications’ workloads due to isolated s pecialized tools\,\ninefficient reuse of prior tuning knowledge\, and the fallible human\nfactor.\n\nThis proposal presents techniques for addressin g those limitations\nwith similarity to enable holistic database optimizat ion. First\, we\npresent a holistic tuning tool that optimizes multiple DB MS aspects\nsimultaneously by using action similarity to organize actions into\nneighborhoods conducive to exploration. We then present a framework\ nthat assists tuners in adapting to environment changes by leveraging\nwor kload and configuration similarity to re-mix historical knowledge.\n\nWe p ropose to extend our preliminary work by transforming the\nhuman-centric t uning workflow into an agentic process through scenario\nsimilarity. We wi ll first investigate contextualizing deployments and\ncreating semantic to ol interfaces. We will then design an orchestrator\nthat learns to select and deploy relevant tuning tools to obtain\nvalidated recommendations. Wit h these efforts\, the agentic process\nwill enable holistic DBMS optimizat ion throughout its lifetime. \n\nThesis Committee:\n\nAndrew Pavlo (Chair )\n\nJignesh Patel \n\nVincent Conitzer \n\nImmanuel Trummer (Cornell Un iversity)\n\nAdditional Information \n\n \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c7620d0 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: \nSpeaker: BAILEY MILLER\, Ph.D. Student\nComputer Science Dep artment\nCarnegie Mellon University\n\nTalk Title: Stochastic Geometry Pri mitives\n\nNumerical computing on complex geometry faces two core challeng es:\nrepresenting geometry and performing computation on it.\nDiscretizati on—voxels\, meshes\, global solves—works until geometry\nis too detail ed or uncertain to resolve. To overcome these\nlimitations\, we propose a complementary paradigm—stochastic graphics\nprimitives (SGPs)—that use randomness to avoid discretization in\nboth representation and computatio n.\n\nFirst\, we’ll survey SGPs in graphics today: Monte Carlo rendering as\nan algorithmic primitive that interacts with geometry via local\nquer ies\, and participating-media models as distributional\nrepresentations th at replace explicit particle interactions with\nfree-flight sampling. Buil ding on these ideas\, we’ll show how the\nsame principles extend beyond light transport to Monte Carlo PDE\nsolvers that handle a range of boundar y conditions using only local\ngeometric queries\, and stochastic solid re presentations that move past\nmicroparticle media to prior-free\, uncertai nty-aware geometry. These\nprimitives are modular and differentiable\, ena bling inverse\nreconstruction and optimization-driven shape design without remeshing.\n\nCrucially\, we’ll position these methods as general-purpo se\nprimitives: black-box operators for physics simulation (elliptic and\n transport PDEs)\, geometric computation (harmonic coordinates\,\ndistance- driven queries\, shape optimization)\, and machine learning\n(differentiab le PDE layers or neural PDE surrogates supervised by\nstochastic operators ). In this view\, SGPs provide a common API in\nplace of meshes and global solves\, so the same primitives serve\nsimulation\, geometry processing\, and learning.\n\nFinally\, we’ll outline current limits—hyperbolic an d nonlinear\nPDEs—and a path forward via hybrid neural–Monte Carlo met hods that\niteratively refine a neural surrogate under supervision while\n preserving the geometric scalability and robustness of Monte Carlo PDE\nso lvers. I’ll close with practical\, more expressive stochastic\nsurface m odels and a roadmap toward more general-purpose SGPs.\n\nThesis Committee\ n\nIoannis Gkioulekas (Chair)\n\nKeenan Crane\n\nNicholas Boffi\n\nRavi Ra mamoorthi (University of California San Diego)\n\nMathieu Desbrun (École Polytechnique / Inria Paris-Saclay)\n\nAdditional Information\n\nIn Person and Zoom Participation.  See announcement. \n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c762654 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: \nSpeaker: DAIYAAN ARFEEN\, Ph.D. Student\, Computer Science D epartment\,\nCarnegie Mellon University\n\nTalk Title: Designing Scalable DNN Training Systems to Overcome\nAlgorithmic Constraints\n\nLLM training requires massive amounts of compute due to large model\nand dataset sizes\ , so it is not unusual to train LLMs on tens or\nhundreds of thousands of GPUs to complete training in a reasonable\namount of time (days or weeks). However\, GPU failures (which are\ncommon at these scales) and data-depen dencies (introduced by the\ntraining algorithms) can lead to severe GPU un derutilization.  \n\nIn this talk\, we present distributed LLM training systems which are\nefficient and fault-tolerant at these scales. We first present\nNonuniform-tensor-parallelism (NTP)\, a technique which increases the\nfault-tolerance of tensor-parallel training\, thereby reducing the\n blast-radius of GPU failures. NTP enables scale-up training with\nlittle-t o-no loss in training efficiency from realistic rates of GPU\nfailures. Ne xt we present PipeFill\, a system for recovering GPU\nutilization (lost du e to scale-out training) by filling pipeline\nbubbles with third-party lat ency-insensitive jobs. We will discuss how\nPipeFill could be extended to support filling pipeline bubbles with\nonline inference jobs\, which are l atency-sensitive.\n\nThesis Committee\n\nGreg Ganger (Chair)\n\nZhihao Jia \n\nPhillip B. Gibbons\n\nDheevatsa Mudigere (NVIDIA)\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c762af2 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: \nSpeaker: MARGARIDA FERREIRA\, Ph.D. Student\, Computer Scien ce\nDepartment\, Carnegie Mellon University\n\nTalk Title: Synthesis of St ateful Programs from Execution Traces\n\nExecution traces are a valuable s ource of information in modern\ncomputing systems. They are continuously c ollected and used for system\ndebugging\, monitoring\, and optimization. T hey capture behavior across\ndiverse scenarios\, from routine operations t o edge cases. This thesis\ninvestigates how execution traces can serve as specifications for\nprogram synthesis\, enabling reverse engineering and a nalysis of\ncomplex systems and automation of traditionally manual tasks w ithout\nexplicit user input.\n\nThis proposal presents three synthesis fra meworks\, Abagnale\, Syren\,\nand HyGLAD\, that illustrate the challenges of this problem on multiple\napplications and how we overcome them. Abagna le reverse-engineers the\nbehavior of congestion control algorithms (CCAs) from network traces.\nNetwork traces contain no information about the imp lementation 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 \nof executions\, making trace filtering and parallelization paramount to\ nAbagnale's viability. Syren allows users to generate arbitrary\nprograms from partial traces that contain some of the function calls\nmade by the p rogram. Syren uses optimizing rewrites to introduce\ncontrol flow in the p rogram. These optimizing rewrites track the data\nused in the functions vi sible in the trace\, which is then used to\ngenerate function calls not vi sible in the trace using an\nexample-based syntax-guided synthesizer. HyGL AD synthesizes\nregex-based anomaly filters that flag deviations from a sy stem'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 it s\nexecution.\n\nAs future work\, we propose to develop a fourth synthesis approach to\nautomate data-aware business processes. We will use logs col lected\nfrom human-executed processes as traces and synthesize implementat ions\nthat model the task logic\, filtering out inconsistencies and errors \nunavoidable in human-generated logs.\n\nThesis Committee\n\nRuben Martin s (Co-chair)\n\nInês Lynce (Co-Chair\, Instituto Superior Técnico)\n\nJu stine Sherry\n\nFraser Brown\n\nJoão F. Ferreira (Instituto Superior Téc nico)\n\nNate Foster (Cornell University)\n\nAdditional Information\n\nIn Person and Zoom Participation.  See announcement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c774c4d 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: \nSpeaker: ALEXANDER KOUJIANOS GOLDBERG\, Ph.D. Student\, Comp uter Science\nDepartment\, Carnegie Mellon University\n\nTalk Title: Impro ving Decision-Making from Distributed Human\nEvaluations\n\nSocially impor tant decisions—from scientific funding\, to college\nadmissions and job hiring—rely on ratings or rankings supplied by\nmultiple human evaluator s. These judgments are prone to noise\, bias\,\nand strategic manipulation \, and there is seldom an objective ground\ntruth against which to determi ne their quality. The goal of this\nthesis is to understand and mitigate s uch errors in distributed human\nevaluation in order to make better decisi ons. Towards this end\, we\nboth conduct controlled experiments in review processes and\ndevelop principled algorithms with provable guarantees.  \n\nIn particular\, we conduct large-scale experiments at peer\nreview co nferences to expose sources of error in evaluation and\nidentify opportuni ties for improvement. Then\, we develop a method for\nselecting top candi dates on the basis of uncertain evaluations\,\nproviding a principled inst antiation of a \"peer review lottery.\"\nFinally\, we design privacy-pres erving algorithms for releasing\nanonymized time-series and graph data\, w hich can enable more\ntransparency into review processes while preserving participant\nanonymity.\n\nThesis Committee\n\nGiulia Fanti (Co-chair)\n\n Nihar B. Shah (Co-chair)\n\nTom Mitchell\n\nJohn Ioannidis (Stanford Unive rsity)\n\nAdditional Information\n\nIn Person and Zoom Participation.  Se e announcement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c775119 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: \nSpeaker: MINGKUAN XU\, Ph.D. Student\, Computer Science Depa rtment \,\nCarnegie Mellon University\n\nTalk Title: Optimization and Simu lation of Quantum Circuits\n\nOptimizing quantum circuits and simulating t hem at scale remain\ncritical bottlenecks: manual design of quantum circui t optimizations\nis labor-intensive and device-specific\, while simulators struggle with\nexponential resource costs. This thesis delivers tools to tackle these\nchallenges. \n\nFirst\, I introduce Quartz\, a superoptimiz er that automates the\ngeneration and verification of circuit transformati ons for arbitrary\nquantum gate sets. By systematically exploring small ci rcuits and\nemploying an automated theorem prover (Z3)\, Quartz discovers both\nexpert-designed and novel optimizations\, outperforming hand-tuned\n optimizers across various gate sets. \n\nNext\, I present Atlas\, a distr ibuted GPU-based simulator that\nhierarchically partitions circuits to exp loit available data\nparallelism while minimizing communication costs\, ru nning over 2×\nfaster than state-of-the-art GPU simulators. Atlas minimiz es\ncommunication overhead via integer linear programming to allocate\n\"n earby\" gates to \"nearby\" GPUs and maximizes throughput through\ndynamic programming for kernel scheduling. \n\nFinally\, I propose an initial fo rmal verification framework to certify\neach application of transformation -based optimizers like Quartz\,\npaving the way for full correctness guara ntees. Together\, these\ncontributions advance automated\, scalable\, and reliable quantum\ncomputing workflows for emerging devices. \n\nThesis Co mmittee\n\nZhihao Jia (Co-chair)\n\nUmut A. Acar (Co-chair)\n\nRyan O'Donn ell\n\nYongshan Ding (Yale University)\n\n \n\nAdditional Information\n\n In Person and Zoom Participation.  See announcement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c7755fd 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: \nSpeaker: MADHUSUDHAN REDDY PITTU\, Ph.D. Student\, Computer Science\nDepartment\, Carnegie Mellon University\n\nTalk Title: Fairness\, Diversity\, Explainability\, and Robustness for\nAlgorithmic Decision-mak ing\n\nFairness\, diversity\, explainability\, and robustness are key chal lenges\nin computational decision-making\, impacting machine learning\, re source\nallocation\, and data analysis. Balancing these principles with\ne fficiency presents significant computational and structural\nchallenges. T his proposal investigates algorithmic approaches for\ndiverse selection\, fair allocation\, interpretable clustering\,\nconstrained subspace approxi mation\, and comparison-based optimization.\nTogether\, these directions c ontribute to more equitable\,\nrepresentative\, interpretable\, and robust algorithmic decision-making\nunder structural and informational constrain ts. \n\nThesis Committee\n\nDavid Woodruff (Chair)\n\nAnupam Gupta\n\nPra sad Tetali\n\nMohit Singh (Georgia Institute of Technology)\n\nOla Svensso n (EPFL)\n\nAdditional Information\n\nIn Person and Zoom Participation.  See announcement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c775a35 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: \nSpeaker: SHAWN SHUOSHUO CHEN\, Ph.D. Student\, Computer Scie nce\nDepartment\, Carnegie Mellon University\n\nTalk Title: Reshaping Data Center Networks with Reconfigurability\n\nData center networks are fundam ental to cloud computing—they tightly\ncouple compute and storage with h igh bandwidth and low latency. The\ndemand for data center network bandwid th is continuously growing\,\ndriven by the proliferation of data-intensiv e applications like AI/ML\nand video streaming. However\, electrical packe t switches struggle to\ndeliver the total bandwidth required by the growin g demands because a\n“plateauing” Moore’s Law limits I/O density and high-speed\nmemory capacity. Moreover\, the sheer scale of modern data ce nter\nnetworks makes electrical packet-switched networks increasingly\nexp ensive and power-hungry. Reconfigurable optical switching\ntechnology is a promising alternative\, offering the potential for\nhigher bandwidth\, re duced energy consumption\, and runtime\nreconfigurability. Reconfigurable data center networks (RDCNs) combine\nthe benefits of both optical and pac ket switches to accommodate\ndiverse traffic patterns and enhance network performance. \n\nThis thesis addresses the limitations of current network designs in\nRDCNs by revisiting underlying assumptions and redesigning co re\nnetwork components\, focusing on transport\, traffic engineering\, and \ntopology. First\, we present Time-division TCP (TDTCP)\, a new transport \nprotocol that adapts to the fluctuating bandwidth and latency in\ndemand -oblivious RDCNs by maintaining independent network states for\neach time- division multiplexed path. Second\, we tackle traffic\nengineering in dema nd-aware RDCNs with approaches that help implement\ncomplex traffic engine ering solutions in switches with minimum\nprecision loss. Third\, we propo se a flexible machine learning job\nscheduling mechanism for reconfigurabl e clusters based on torus\ntopologies\, ensuring optimal job performance w hile mitigating resource\nfragmentation. Together\, these innovations aim to unlock the full\npotential of RDCNs\, achieving higher performance\, co st-efficiency\, and\nscalability for future data center workloads. \n\nTh esis Committee\n\nSrinivasan Seshan (Chair)\n\nPeter Steenkiste\n\nTim Det tmers\n\nMinlan Yu (Harvard University)\n\nAdditional Information\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c775f74 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: \nSpeaker: WAN SHEN LIM\, Ph.D. Student\, Computer Science Dep artment\,\nCarnegie Mellon University\n\nTalk Title: Database Gyms: Toward s Autonomous Database Tuning\n\nDatabase management systems (DBMSs) are th e foundation of modern\ndata-intensive applications. But as more features are developed to\nsupport new workloads\, they become increasingly complex and difficult\nto configure. Decades of research on autonomous DBMS confi guration\nhave largely produced advisory tools that still rely on human\ne xpertise for their deployment into database tuning pipelines. Using\nthese tools involves a multi-step process where a human operator (1)\ndetermine s an optimization objective\, (2) selects a suitable tool to\nimprove the objective\, (3) sets up and configures the DBMS to run a\nparticular workl oad\, (4) runs the workload to collect telemetry\, (5)\nuses the collected telemetry to calibrate the tool\, and (6) operates\nthe tool to obtain re commendations\, which the operator must then\nreview and apply. Because of the ad-hoc nature of these pipelines\,\nthey require significant human ef fort to set up\, extend\, and deploy.\nMoreover\, these tools are difficul t to compose and swap.\n\nThis proposal presents the database gym\, an int egrated framework that\nsystematizes and automates the DBMS configuration pipeline. The gym\neliminates repetition in the setup and operation of suc h pipelines by\nproviding a set of reusable\, interoperable\, and intercha ngeable\ncomponents that simplify the development and integration of ML-dr iven\nDBMS configuration tools. It leverages its complete control over the \ntuning process to enable optimizations that require end-to-end\nknowledg e. First\, it eliminates step-level repetition by skipping over\nredundant computation during telemetry collection to reduce the\nlatency of the tun ing pipeline. Next\, it eliminates pipeline-level\nrepetition by reusing p ast experience to improve tool performance. For\nexample\, it adapts model s of DBMS behavior to account for how operator\nsemantics differ across DB MS versions. \n\nWe propose to extend our preliminary work by developing a tool for\nDBMS upgrades that uses version-aware models to predict perfor mance\nimprovements and regressions\, addressing another database\nadminis tration task with significant human involvement. Lastly\, we\nwill leverag e recent advances in agentic artificial intelligence to\norchestrate tools on behalf of a human operator. These efforts will\ntransform the database gym from a platform for developing and\ndeploying DBMS configuration tool s into an autonomous database\nadministrator for production environments.  \n\nThesis Committee\n\nAndrew Pavlo (Chair)\n\nJignesh Patel\n\nDavid A ndersen\n\nLin Ma (University of Michigan)\n\nAdditional Information\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c776536 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: \nSpeaker: CASPAR OESTERHELD\, Ph.D. Student\, Computer Scienc e\nDepartment\, Carnegie Mellon University\n\nTalk Title: New foundational ideas for cooperative AI\n\nMy doctoral research addresses two fundamenta l obstacles to beneficial\noutcomes from strategic interactions between mu ltiple parties:\nstrategic incentives against cooperation (as in the Priso ner's\nDilemma) and the multiplicity of solutions (sometimes called the\ne quilibrium selection problem). As AI systems are increasingly\ninvolved in consequential decision making processes on behalf of human\nprincipals\, understanding how to achieve desirable outcomes in\nmulti-agent AI setting s becomes 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 coo perative outcomes.      \n\nThree primary research directions form the core of this dissertation.\nFirst\, the concept of safe Pareto improveme nts provides a rigorous\nframework for improving outcomes without resolvi ng equilibrium\nselection problems. Unlike traditional solution concepts\, safe Pareto\nimprovements make qualitative assumptions about pairs of gam es rather\nthan individual games. This sometimes allows us to prefer playi ng one\ngame over another\, without any judgment about how each of the\nin dividual games is played. Second\, the concept of program\nequilibrium e xplores how the use of mutually transparent\ndecision-making algorithms ca n allow for cooperation. Third\, my\nresearch on so-called Newcomb-like  decision problems takes\ninspiration from philosophical branches of decisi on theory. I\ninvestigate how cooperation can be achieved when different p arties\ndeploy similar AI systems.\n\nCurrent and planned work extends the se directions through several\nprojects\, including: connecting program eq uilibrium with mediated\nequilibrium\; exploring sequential program/mediat ed equilibrium-type\nsettings\; investigating the relationship between sel f-locating beliefs\nand decision theory\; developing theoretical foundatio ns for safe\nPareto improvements\, as well as analyzing safe Pareto improv ements in\na new setting. I've also started to implement some of these\nth eoretical ideas in language models to test their practical\napplicability.  \n\nThesis Committee\n\nVincent Conitzer (Chair)\n\nTuomas Sandholm\n\nF ei Fang\n\nStuart Russell (University of California\, Berkeley)\n\nBen Lev instein (University of Illinois at Urbana-Champaign)\n\nAdditional Informa tion\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c776aa0 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: \nSpeaker: JEFF XU\, Ph.D. Student\, Computer Science Departme nt\, Carnegie\nMellon University\n\nTalk Title: Spectral Techniques for Av erage-Case Complexity and Beyond\n\nIn recent years\, algorithmic challeng es 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 p roblems\, the best-known\nefficient algorithms are often suboptimal\, givi ng rise to information\nvs. computation gaps\, discrepancies between what is theoretically\npossible given the amount of information and what can be attained via\nefficient algorithms. One fundamental question is how we ca n provide\nrigorous evidence of hardness to show that such gaps are\ninsur mountable for efficient computation. \n\nWe propose to provide rigorous e vidence via the lens of the\nSum-of-Squares (SoS) algorithms\, a hierarchy of semidefinite\nprogrammings. Unlike several other popular models in the average-case\nsetting (eg. low-degree polynomials/statistical-query/ over lap-gap).\nSum-of-Squares algorithms are known to capture various optimal\ nalgorithms in both the average and worst-case setting\, and therefore\npr ovide one of the strongest form of hardness. \n\nIn this talk\, I will il lustrate that average-case SoS hardness usually\nboils down to the study o f spectral techniques\, specifically the study\nof random matrices with co rrelated input\, and how a refined\nunderstanding of such matrices gives r ise to the resolution of key\naverage-case complexity questions including sparse graph\nindependent-set\, densest-k subgraph\, and coloring. Finally \, I will\ntalk about some exciting challenges in the future along this\nd irection\, and specifically how they boil down again to\nsimple-to-state\, self-contained questions about random matrices\, and\nexplore the applica tions beyond average-case hardness.\n\nThesis Committee\n\nPravesh K. Koth ari (Chair)\n\nAayush Jain\n\nRyan O’Donnell\n\nMadhur Tulsiani (Toyota Technical Institute at Chicago / University of\nChicago)\n\nAdditional Inf ormation\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c77d9a2 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: \nSpeaker: JOSHUA NATHANIEL WILLIAMS\, Ph.D. Student\, Compute r Science\nDepartment\, Carnegie Mellon University\n\nTalk Title: Understa nding Generative Image Modeling Through Discrete\nCounterfactual Prompt Op timization\n\nIt is well understood that generative models can exhibit\nre presentational biases across various social groups. Without explicit\ncond itioning\, the vast majority of airplane pilots will be male and\nthe vast majority of bank tellers will be female. While much of the\nexisting work focuses on hypothesis-driven investigations into these\nbiases\, in this proposed thesis\, we focus on discovery of new and\nunexpected patterns in how these models represent people. We show\nthrough the lens of counterfa ctual explainability – processes that\nfind minimal input changes that a lter a model's output – a framework\nfor hypothesis generation in order to reveal surprising patterns in\nhow text-to-image models align textual i nput with socially meaningful\ngroup memberships.\n\nWe establish a formal \, mathematical distinction between counterfactual\nexplanations and adver sarial examples\, which enables the development\nof novel distance metrics and optimization strategies for identifying\nhuman-readable counterfactua l prompts. Our approach employs discrete\noptimization techniques\, includ ing an adapter for computing gradients\nacross embeddings from diverse mod els. Furthermore\, we evaluate\ndiscrete prompt optimization methods and d emonstrate that additional\nregularization is crucial for generating coher ent and human-like\nprompts. This work lays the foundation for more nuance d understanding\nof representational biases in generative models and offer s tools for\ntheir systematic exploration.\n\nThesis Committee\n\nZico Kol ter (Chair)\n\nAditi Raghunathan\n\nHoda Heidari\n\nSarah Laszlo (Visa)\n\ n \n\nAdditional Information\n\nIn Person and Zoom Participation.  See a nnouncement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c77df06 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: \nSpeaker: LONG PHAM\, Ph.D. Student\, Computer Science Depart ment\,\nCarnegie Mellon University\n\nTalk Title: Hybrid Resource-Bound An alyses of Programs\n\nResource-bound analysis aims to infer symbolic bound s of worst-case\nresource usage (e.g.\, running time\, memory\, and energy ) of programs as\nfunctions of program inputs. Resource analysis has numer ous\napplications\, including job scheduling in cloud computing and\npreve ntion of side-channel attacks. Various resource analysis\ntechniques have been developed\, and they have unique strengths and\nweaknesses that compl ement each other. (Automatic) static resource\nanalysis\, which analyzes t he source code of programs\, is sound: if it\nsuccessfully infers a cost b ound\, it is guaranteed to be a valid\nbound. However\, every static analy sis technique is incomplete: there\nexists a program that the analysis tec hnique cannot handle. Meanwhile\,\ndata-driven analysis\, which statistica lly analyzes cost measurements\nobtained by running programs on many input s\, can infer a candidate\ncost bound for any program. However\, it does n ot guarantee soundness\nof inference results. \n\nTo overcome limitations of individual analysis techniques\, I propose\nhybrid resource analysis\, which integrates two complementary analysis\ntechniques to retain their s trengths while mitigating their respective\nweaknesses. The user first spe cifies which analysis techniques are\nused to analyze which code fragments and quantities. Hybrid analysis\nthen performs its constituent analysis t echniques on their respective\ncode fragments and quantities. Finally\, th eir inference results are\ncombined into an overall cost bound. \n\nThe d evelopment of hybrid resource analysis has been driven by the\ndesire to g o beyond Automatic Amortized Resource Analysis (AARA)\, a\nstate-of-the-ar t type-based static resource analysis technique. I\nstart by proving polyn omial-time completeness of AARA. I next\nintroduce Bayesian data-driven an alysis\, which conducts Bayesian\ninference on cost measurements to infer a posterior distribution of\nsymbolic cost bounds. I then present the firs t hybrid resource\nanalysis\, Hybrid AARA\, followed by a discussion of it s limitations. To\novercome these limitations\, I introduce the second hyb rid resource\nanalysis\, resource decomposition. I additionally describe S wiftlet\,\nwhich instantiates the resource-decomposition framework with AA RA and\nBayesian resource analysis. \n\nFinally\, for proposed work\, my collaborators and I plan to develop\ndata-driven-analysis for statisticall y inferring not only a worst-case\nsymbolic cost bound but also a worst-ca se input generator\, which is a\nprogram generating worst-case program inp uts of various sizes. \n\nThesis Committee\n\nJan Hoffmann (Chair)\n\nFer as Saad\n\nMatt Fredrikson\n\nFrancois Pottier (Inria Paris Centre)\n\nAdd itional Information\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c77e48b 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: \nSpeaker: HOJIN PARK\, Ph.D. Student\, Computer Science Depar tment\,\nCarnegie Mellon University\n\nTalk Title: Cost-Efficient Storage and Caching in Public Clouds\n\nPublic clouds are widely adopted for their scalability\, flexibility\,\nand reduced operational overhead\, but optim izing costs while\nmaintaining performance remains a significant challenge . This thesis\naddresses the problems of reducing storage cluster costs in public\nclouds and minimizing cross-cloud/region data access costs by\nex ploiting the elasticity and diversity of public cloud resources\ncombined with real-time workload monitoring. \n\nFirst\, this work addresses the c hallenge of reducing storage cluster\ncosts in public clouds through Mimir \, an automated system that\nleverages heterogeneous storage types to dete rmine storage cluster\nconfigurations that reduce costs while meeting work load performance\nrequirements. Next\, this thesis introduces Macaron\, an \nauto-configuring caching system designed for cross-cloud/region data\nac cess. By dynamically adjusting cache capacity based on workload\ncharacter istics\, Macaron minimizes remote data access costs and\nensures low laten cy. Utilizing the object storage for caching storage\ntype\, Macaron demon strates substantial cost savings compared to\nexisting cross-cloud/region data access approaches. \n\nBuilding on Macaron\, I propose a novel prefe tching design for\ncross-region data access in public clouds that includes an object\ngrouping-based prefetching algorithm and dynamic cache space\n allocation for demand-requested and prefetched data. This design aims\nto mitigate cache pollution\, reduce wasted prefetches\, and improve\ndata ac cess latency while minimizing additional costs. \n\nBy addressing cost an d performance optimization in public cloud\nstorage and cross-cloud/region data access systems\, this thesis\nenables reducing costs of utilizing pu blic cloud resources for storage\nand caching. \n\nThesis Committee\n\nGe orge Amvrosiadis (Co-Chair)\n\nGregory R. Ganger (Co-Chair)\n\nJignesh M. Patel\n\nCarlo Curino (Microsoft Research)\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c77e965 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: \nSpeaker: ANUP AGARWAL\, Ph.D. Student\, Computer Science Dep artment\,\nCarnegie Mellon University\n\nTalk Title: Designing Network Con trol Algorithms with Performance\nGuarantees\n\nControl algorithms\, such as those used in congestion control (CC) and\nadaptive-bitrate (ABR) strea ming\, make critical decisions that\ninfluence performance\, user experien ce\, and revenue in networked\napplications. Despite their importance\, th ese algorithms are often\ndeveloped through heuristics and intuition\, lea ding to implicit\nassumptions about network environments and a lack of for mal guarantees\nabout their performance. The result is anywhere from silen t to\nembarrassing performance degradation (e.g.\, the recent Netflix\nliv estream of Paul vs Tyson).\n\nIn this proposed thesis\, we design tools (b oth mathematical and\ncomputational) that make formal performance guarante es possible.\nNetwork control algorithms often operate in partially observ able\nenvironments\, e.g.\, they do not explicitly know the network topolo gy\,\nrouting\, link capacities\, or what other flows they share the netwo rk\nwith. The mathematical tools allow us to reason about what information \nalgorithms may infer from their partial observations. The\ncomputational tools build on these mathematical tools to semi-automate\nthe design of c ontrol algorithms\, using techniques from program\nsynthesis\, and game th eory. By combining our tools with techniques in\nnetwork calculus and form al methods\, we precisely state performance\nobjectives and environment as sumptions\, enabling us to construct\nproofs about the performance of the designed control algorithms.\n\nThrough this work\, we design new CC algor ithms that provide\nperformance bounds on networks where existing algorith ms struggle to\nguarantee even 1% utilization. Our systematic methodology also led us\nto discover and prove new fundamental tradeoffs in congestion control\,\nincluding a tradeoff between loss and convergence time on netw orks\nwith jitter and short buffers\, and a tradeoff between fairness and\ nrobustness vs. latency and generality of CC algorithms.\n\nThe majority o f the completed work deals with single-agent congestion\ncontrol. In the p roposed work\, we extend our tools to reason about\nmulti-agent control en vironments and ABR algorithms. \n\nThesis Committee\n\nSrinivasan Seshan (Chair)\n\nVyas Sekar\n\nJustine Sherry\n\nPhilip Brighten Godfrey (Univer sity of Illinois Urbana-Champaign)\n\n \n\nAdditional Information\n\nIn P erson and Zoom Participation.  See announcement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c77ee8d 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: \nSpeaker: ASHER TROCKMAN\, Ph.D. Student\, Computer Science D epartment\,\nCarnegie Mellon University\n\nTalk Title: Mimetic Initializat ion for Deep Neural Networks\n\nWhile neural network weights are typically initialized randomly from\nunivariate distributions\, pre-trained weights often have\nvisually-discernible multivariate structure. We propose a tec hnique\ncalled \"mimetic initialization\" that aims to replicate such stru ctures\nwhen initializing convolutional networks (CNNs)\, Transformers\, a nd\nState Space Models (SSMs). For CNNs\, we handcraft a class of\nmultiva riate Gaussian distributions to initialize filters for\ndepthwise convolut ional layers\; for Transformers\, we initialize the\nquery and key weights for self-attention layers such that their\nproduct approximates the ident ity\; and for SSMs\, we initialize layers\nto approximate simple linear at tention. Mimetic initialization\nsubstantially reduces training time and i ncreases final accuracy on\nvarious common small-scale benchmarks.\n\nOur technique enables us to almost close the gap between untrained and\npre-tr ained Vision Transformers on small datasets like CIFAR-10\,\nachieving up to a 6% gain in accuracy through initialization alone.\nFor convolutional networks like ConvMixer and ConvNeXt\, we observe\nimprovements in accurac y and reductions in training time\, even when\nconvolutional filters are f rozen (untrained) after initialization. For\nSSMs\, mimetic initialization substantially improves generalization\nabilities on synthetic language ta sks like copying and associative\nrecall. Overall\, our findings suggest t hat the benefits of\npre-training can be separated into two components: se rving as a good\ninitialization and storing transferable knowledge\, with the former\nbeing simple enough to (at least partially) capture by hand in \nclosed-form.\n\nThesis Committee\n\nZico Kolter (Chair)\n\nAlbert Gu\n\n Aditi Raghunathan\n\nSébastien Bubeck (OpenAI)\n\n \n\nAdditional Inform ation\n\nIn Person and Zoom Participation.  See announcement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c77f3b3 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: \nSpeaker: EMRE YOLCU\, Ph.D. Student\, Computer Science Depar tment\,\nCarnegie Mellon University\n\nTalk Title: Weak Extended Resolutio n and Nonautomatability in Proof\nComplexity\n\nThe satisfiability problem for propositional logic (SAT) has been a\ncentral topic in computer scien ce for many decades. It is arguably the\ncanonical NP-complete problem: re ductions 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 proble m instead. This strategy\nturns out to be surprisingly effective thanks to the effectiveness of\nimplementations of heuristic algorithms for SAT\, c ommonly known as SAT\nsolvers. Those solvers are expected to output proofs to certify their\nanswers\, and in this sense they are proof search algor ithms. Proof\ncomplexity\, the branch of computational complexity that stu dies 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\" ends of a spectrum: those motivated by\nSAT solving\, aiming to improve h euristic proof search\, and those\narising from computational complexity\, aiming to show that proof\nsearch is hard in the worst case. In particula r\, we focus on the\nfollowing two lines of research: proof complexity of a family of\nsystems that we refer to as weak extended resolution systems and the\nautomatability problem from computational complexity. The first\n involves proof systems that formalize restricted versions of the\nability to make assumptions that hold without loss of generality\,\ncommonly used informally to shorten proofs. The second is the question\nof whether effic ient proof search is possible in the worst case. We\ngive a complete descr iption 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 syste ms in a black-box manner\; we give\nan example application and propose an approach to lift hardness\nresults from weaker to stronger proof systems.  \n\nThesis Committee \n\nMarijn J. H. Heule (Chair)\n\nJeremy Avigad\n\ nRyan O'Donnell\n\nSamuel R. Buss (University of California San Diego)\n\n Additional Information\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c77f90e 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: \nSpeaker: NUNO SABINO\, Ph.D. Student\, Computer Science Depa rtment\,\nCarnegie Mellon University\n\nTalk Title: Improving Code-Injecti on Vulnerability Detection &\nConfirmation in JS Programs via Program Anal ysis\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\nwebp age. On the backend\, arbitrary code execution (ACE) and arbitrary\ncomman d injection (ACI) enable attackers to execute arbitrary code or\ncommands on the server. Exploiting such vulnerabilities can lead to\nsevere consequ ences\, including unauthorized access to sensitive data\nand even full sys tem compromise.\n\nEach potential flow identified by these tools traces a program path\nwhere attacker-controlled input\, such as a URL\, reaches a sensitive\nfunction that may lead to arbitrary code execution. DTA require s\nfinding a concrete input that demonstrates a potential flow in the\ntar get application\, but prior work fails to thoroughly explore program\npath s. In the backend\, these tools miss ACI and ACE that require\ninputs with complex structure. We develop a novel type- and\nstructure-aware fuzzing technique to explore Node.js packages\, and an\nenumerator to synthesize s yntactically valid payloads for ACE\nvulnerabilities. Incorporating these components on prior work\nNodeMedic led to finding 2257 potential flows an d confirm\nvulnerabilities in 766 Node.js packages.\n\nA unique challenge in exploring frontend code is that program behavior\nmay depend on user ac tions on the webpage. To address this\, we develop\na fuzzer to interact w ith the target webpage and evaluated it against\n43\,436 popular pages. Fu rthermore\, we found that including optional\nGET parameters in the target URL uncovers significantly more DOM-XSS\nvulnerabilities. This led us to use dynamic symbolic execution to\nautomatically synthesize GET parameters satisfying program\nconstraints. Compared to our replication of prior wor k DOMsday\, the\nfuzzer increases potential DOM-XSS flows found by 37% and confirms 57%\nmore vulnerabilities.\n\nFinally\, we find that non-exploit able potential flows may still hint\ntowards real vulnerabilities that req uire additional steps to confirm\,\nsuch as bypassing sanitization measure s and extending the attacker’s\ncapabilities by executing other program parts. Thus\, we propose the\ndesign and implementation of exploration str ategies that efficiently\nexplores the program to discover an exploitable path\, using\ninformation from a given potential flow that we assume to ha ve 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\, Universidade do Porto)\n\nLujo Bauer\n\nRuben Martins\n\nJosé Fragoso (In stituto Superior Técnico)\n\nCristian-Alexandru Staicu (CISPA Helmholtz C enter for Information\nSecurity)\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c77feec 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: \nSpeaker: LONG PHAM \, Ph.D. Student\, Computer Science Depar tment\,\nCarnegie Mellon University\n\nTalk Title: Hybrid Resource-Bound A nalyses of Programs\n\nResource-bound analysis aims to infer symbolic boun ds of worst-case\nresource usage (e.g.\, running time\, memory\, and energ y) of programs as\nfunctions of program inputs. Resource analysis has nume rous\napplications\, including job scheduling in cloud computing and\nprev ention of side-channel attacks. Various resource analysis\ntechnique have been developed\, and they have unique strengths and\nweaknesses that compl ement each other. (Automatic) static resource\nanalysis\, which analyzes t he source code of programs\, is sound: if it\nsuccessfully infers a cost b ound\, it is guaranteed to be a valid\nbound. However\, every static analy sis technique is incomplete: there\nexists a program that the analysis tec hnique cannot handle. Meanwhile\,\ndata-driven analysis\, which statistica lly analyzes cost measurements\nobtained by running programs on many input s\, can infer a candidate\ncost bound for any program. However\, it does n ot guarantee soundness\nof inference results. \n\nTo overcome limitations of individual analysis techniques\, I propose\nhybrid resource analysis\, which integrates two complementary analysis\ntechniques to retain their s trengths while mitigating their respective\nweaknesses. The user first spe cifies which analysis techniques are\nused to analyze which code fragments and quantities. Hybrid analysis\nthen performs its constituent analysis t echniques on their respective\ncode fragments and quantities. Finally\, th eir inference results are\ncombined into an overall cost bound. \n\nThe d evelopment of hybrid resource analysis has been driven by the\ndesire to g o beyond Automatic Amortized Resource Analysis (AARA)\, a\nstate-of-the-ar t type-based static resource analysis technique. I\nstart by proving polyn omial-time completeness of AARA. I next\nintroduce Bayesian data-driven an alysis\, which conducts Bayesian\ninference on cost measurements to infer a posterior distribution of\nsymbolic cost bounds. I then present the firs t hybrid resource\nanalysis\, Hybrid AARA\, followed by a discussion of it s limitations. To\novercome these limitations\, I introduce the second hyb rid resource\nanalysis\, resource decomposition. I additionally describe S wiftlet\,\nwhich instantiates the resource-decomposition framework with AA RA and\nBayesian resource analysis. Finally\, for proposed work\, my\ncoll aborators and I plan to develop data-driven-analysis for\nstatistically in ferring not only a worst-case symbolic cost bound but\nalso a worst-case i nput generator\, which is a program generating\nworst-case program inputs of various sizes. \n\nThesis Committee\n\nJan Hoffmann (Chair)\n\nFeras S aad\n\nMatt Fredrikson\n\nNadia Polikarpova (University of California\, Sa n Diego)\n\n \n\nAdditional Information\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c780731 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: \nSpeaker: BENJAMIN STOLER\, Ph.D. Student\, Computer Science Department\,\nCarnegie Mellon University\n\nTalk Title: Towards Robust Aut onomous Driving and Social Robot\nNavigation via Enhanced Data Utilization \n\nAutonomous robots—including self-driving vehicles\, sidewalk deliver y\nrobots\, and more—must navigate among humans in a safe and\nsocially- compliant manner. Current approaches for building and\nevaluating such aut onomous systems rely on data-driven techniques\;\nhowever\, a generalizati on gap emerges\, as methods trained in these\ntraditional paradigms are un able to cope with unexpected real-world\nscenarios. Therefore\, this thesi s aims to develop improved evaluation\nsettings and methodologies to incre ase and assess robustness in\nautonomous robot navigation against these ch allenges. This thesis\nproposal describes several completed works that ass ess and improve\ndifferent facets of robustness in autonomy:\n\nFor robust ness against perception errors affecting downstream motion\nprediction\, w e construct a framework for converting top-down\npedestrian trajectory dat asets into a more challenging first-person\nview perspective. We then deve lop 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 ch aracterization method which\nleverages counterfactual probes to find hidde n safety-relevant\nscenarios in large datasets. We then address the induce d\ngeneralization gap by incorporating the characterizations into\ndownstr eam trajectory prediction models' inductive biases.For\nrobustness against adversarial\, safety-critical scenarios\, we develop\na reactive\, skill- based adversary policy which leverages a learned\,\nmulti-faceted critical ity objective to perturb existing scenarios. We\nthen train ego policies i n a closed-loop manner against these\ngenerated scenarios\, demonstrating improved downstream ego\nperformance.\n\nThis proposal concludes by outlin ing and discussing proposed works to\nfurther advance robustness in autono mous navigation. These works\ninclude enhancements in scenario characteriz ation and\nout-of-distribution generalization\, as well as novel formulati ons of\nrealism as an objective in safety-critical generation. \n\nThesis Committee\n\nJean Oh (Chair)\n\nSebastian Scherer\n\nReid Simmons\n\nJona than Francis (Bosch Center for Artificial Intelligence)\n\n \n\nAdditiona l Information\n\nIn Person and Zoom Participation.  See announcement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c780feb 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: \nSpeaker: JOSEPH E. REEVES\, Ph.D. Student\, Computer Science Department\,\nCarnegie Mellon University\n\nTalk Title: Cardinality Const raints in Satisfiability Solving\n\nAutomated reasoning (AR) engines solve problems represented in\nmathematics and logic stemming from a wide range of domains including\nhardware and software verification\, cryptography\, and cloud security.\nBoolean satisfiability (SAT) solvers drive much of t he reasoning\nbehind many AR engines\, but their input format\, a formula in\npropositional logic\, can be limiting. High-level constraints must\nbe  encoded into sets of simpler constraints\, clauses\, and finding\na go od encoding often requires expert knowledge. We propose\nextending the in put of SAT solvers to include cardinality constraints\,\nmoving encoding q uestions from the user-side to the solver-side.\nCardinality constraints a re a frequently occurring type high-level\nconstraint that represent count ing\, e.g.\, “at least k packages must\nbe delivered” or “you can w ork from home at most one day of the\nweek”.\n\nIn this proposal we di scuss four research problems arising from a\ncardinality-based input. Firs t\, we will develop a cardinality\nconstraint extraction tool that will co nvert previously encoded\nproblems into a cardinality-based normal form\, providing backwards\ncompatibility for our solving techniques. Second\, we will engineer\ndynamic cardinality constraint encoding into the top-tier SAT solver\nCaDiCaL to improve performance on problems with many cardinali ty\nconstraints. Third\, we will explore the ways in which parallel solvin g\ntechniques can leverage information within cardinality constraints to\n achieve better problem partitioning. Fourth\, we will equip the\nextractio n and solving with end-to-end proof checking through\nmodifications to exi sting proof systems and proof checkers. Our goal\nin investigating these f our research problems is to support the claim\nthat a cardinality-based fo rmat should be the standard input format\nfor modern SAT solvers.\n\nThesi s Committee\n\nMarijn Heule (Chair)\n\nRandal Bryant\n\nRuben Martins\n\nA rmin Biere (University of Freiburg) \n\nAdditional Information\n\nIn Pers on and Zoom Participation.  See announcement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c78164f 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: \nSpeaker: MENG-CHIEH (JEREMY) LEE\, Ph.D. Student\, Computer Science\nDepartment\, Carnegie Mellon University\n\nTalk Title: Explainabl e Mining of Graphs and Time Series: Algorithms\nand Applications\n\nGiven a social network\, how can we predict the connections between\nusers and d etermine whether they are based on shared hobbies or common\nfriends? Simi larly\, how can we identify anomalies in time series data\nand explain why they are suspicious? Although recent machine learning\nmodels with improv ed performance are being developed\, they are often\nblack-box methods tha t are difficult to interpret. This leads us to\nexplainable artificial int elligence (XAI)\, which offers valuable\ninsights through its explanations .   \n\nIn this thesis proposal\, we introduce carefully designed explai nable\nmethods tailored for graph and time series data\, with diverse\napp lications. Each method we proposed is either inherently\nexplainable\, or provides explanations for the data or decisions it\nmakes.  \n\nThesis C ommittee \n\nChristos Faloutsos (Co-Chair)\n\nLeman Akoglu (Co-Chair)\n\n Geoffrey Gordon\n\nNina Mishra (Amazon)\n\nAdditional Information\n\nIn Pe rson and Zoom Participation.  See announcement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c782343 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: \nSpeaker: JUN-TING HSIEH\, Ph.D. Student\, Computer Science D epartment\,\nCarnegie Mellon University\n\nTalk Title: Spectral Algorithms for Optimization beyond the\nAverage-Case\n\nSpectral algorithms involve using the eigenvalues and eigenvectors of\nmatrices derived from the input for algorithm design and analysis.\nThese techniques have achieved remark able success across a wide range\nof computational problems. In particular \, through the study of random\nmatrices\, spectral methods have been wide ly used to solve problems in\naverage-case complexity\, where the input is drawn from some random\nmodel. \n\nIn this proposal\, we explore the rob ustness of spectral algorithms for\nhybrids between worst-case and average -case input models. Many\nexisting algorithms tend to “overfit” to the specific randomness\nof the input – they fail even with slight perturba tions of the input\nmodels. First\, we show that spectral algorithms succe ed in both\nrefuting semirandom constraint satisfaction problems (CSPs) an d\nsolving semirandom planted instances\, generalizing results previously\ nknown only for fully random CSPs. Second\, we demonstrate how upper\nboun ds on the second eigenvalue of the adjacency matrix suffice for\nfinding l arge independent sets in 3-colorable graphs\, extending\nexisting results for random 3-colorable graphs.\n\nFinally\, for future work\, we aim to ex tend such ideas to worst-case\ninstances by understanding the minimal assu mptions necessary for\nalgorithmic success. Moreover\, we will explore the limitations of\nspectral algorithms and investigate formal connections be tween\nspectral algorithms and low-degree polynomials of the input. \n\nT hesis Committee \n\nPravesh K. Kothari (Carnegie Mellon University/Prince ton University)\n\nRyan O'Donnell\n\nJason Li\n\nVenkatesan Guruswami (Uni versity of California\, Berkeley)\n\nDavid Steurer (ETH\, Zürich)\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c78282f 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: \nSpeaker: ADITI KABRA\, Ph.D. Student\, Computer Science Depa rtment\,\nCarnegie Mellon University\n\nTalk Title: Verified Control Envel ope Synthesis for Hybrid Systems\n\nMany cyber-physical systems\, such as trains\, planes\, and self-driving\ncars\, are safety-critical but difficu lt to reason about. Formal\nverification can provide strong safety guarant ees\, but most industrial\ncontrollers are too complex to formally verify. Safe control envelopes\ncharacterize families of safe controllers and are used to monitor\nuntrusted controllers on verifiable abstractions of cont rol systems\nthat isolate the parts relevant to safety without the full co mplexity\nof a specific control implementation\, at runtime. They can put complex\ncontrollers\, even when machine learning based\, within the reach of\nformal guarantees. But correct control envelopes are still hard to\nd esign because the control engineer needs to identify correct control\ncond itions that tell the controller what to do right now to stay safe\nat all times in the future by anticipating the behavior of the system\nover compl ex dynamics and an uncountably infinite state space. \n\nThis thesis prop oses to provide synthesis techniques to automatically\nsynthesize provably correct control conditions\, greatly reducing the\nmanual effort required for control envelope design. It aims to scale\nsynthesis to complexity of real-world systems. The input of the\nsynthesis tool is a sketch of the c ontrol envelope in a hybrid system\nshowing what kind of control behavior is physically possible. The tool\nfills in the blanks of the sketch by syn thesizing control conditions\nusing hybrid system game theory. The output is a provably correct\nsymbolic control envelope. Existing controller synt hesis techniques do\nnot solve control envelope synthesis because control envelopes have\nthe higher-order constraint of permitting as many valid co ntrol\nsolutions as possible. \n\nCompleted work provides the algorithm C ESAR (Control Envelope\nSynthesis via Angelic Refinement) which solves a c lass of problems\nwhere a set of systematic game refinements allows automa tic control\nenvelope synthesis. Proposed work generalizes synthesis to a broad\nclass of systems (characterized by admitting a natural representati on\nin differential game logic) and develops a system that allows users to \nprovide the human intuition based insights that\, together with\nautomat ed reasoning\, can complete the control envelope synthesis\nprocess in mor e complex cases. \n\nThesis Committee\n\nAndré Platzer (Co-chair\, Carne gie Mellon University/Karlsruhe\nInstitute of Technology)\n\nStefan Mitsch (Co-chair\, Carnegie Mellon University/DePaul University)\n\nEunsuk Kang\ n\nArmando Solar-Lezama (Massachusetts Institute of Technology)\n\n \n\n Additional Information\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c783870 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: \nSpeaker: MINGXUN ZHOU\, Ph.D. Student\, Computer Science Dep artment\,\nCarnegie Mellon University\n\nTalk Title: Practical Private Inf ormation Retrieval and Searching with\nSublinear Cost\nMathJax.Hub.Config( {\ntex2jax: {\ninlineMath: [ ['$'\,'$']\, [\"\\\\(\"\,\"\\\\)\"] ]\,\nproc essEscapes: true\n}\n})\;\n\nPrivate Information Retrieval (PIR) is a long -studied cryptographic\nprimitive that allows a user to retrieve informati on from a public\ndatabase without revealing the query to the service pro vider.\nClassically\, PIR was studied in a setting without any preprocessi ng\,\nand this setting is known to have inherent limitations that the tota l\ncomputation cost per query must be linear in the size of the database\n to achieve privacy. This limitation is the fundamental barrier for\nscalin g PIR to large databases and building practical product systems\nbased on PIR. Pioneered by Beimel\, Ishai and Malkin (Crypto 2000) and\nCorrigan-Gi bbs and Kogan (Eurocrypt 2020)\, the preprocessing PIR\nparadigm has been shown to overcome the linear computation cost\nbarrier. Nonetheless\, prio r works on preprocessing PIR remain mostly\nin the theoretical space due t o their use of heavy cryptographic\nprimitives and/or convoluted algorithm ic constructions.\n\nAchieved Results: We proposed a practical single-serv er PIR\nconstruction in the preprocessing setting\, named Piano (S P 2023) \,\nthat achieved sublinear query cost based on lightweight cryptographic\ nprimitives. Piano achieved $\\tilde O(\\sqrt{n})$ amortized\ncommunicatio n and computation per query given a database of size n \,\nand only requir ed $\\tilde O(\\sqrt{n})$ client storage. Notably\, it is\nalso concretely efficient – for a 100GB database of 1.6 billion\nentries\, Piano takes only 12ms online computation time on a single\nCPU-core. Subsequently\, we improved the construction and obtained a\nnew practical PIR scheme\, Quar terPIR (Eurocrypt 2024)\, that reduced\nthe online communication cost to $ \\tilde O(n^{1/4})$ per query\, while\nmaintaining competitive practical p erformances. Proposed Direction:\nNearly all existing PIR constructions ar e designed for point accesses\nin an array-type database\, while many prac tical information retrieval\nsystems like search engines do need more adva nced access algorithms to\nsupport semantic and similarity queries. We pro pose to construct a\nprivate search algorithm that can handle semantic/sim ilarity queries\nwith sublinear communication and computation query costs based on our\npractical PIR constructions and graph-based Nearest Neighbor Search\n(NNS) algorithms. This construction will be the first private sea rch\nalgorithm that achieves sublinear query cost\, and it has the potenti al\nto support multi-modal search queries including text\, image\, voice a nd\nvideo search.\n\nThesis Committee: \n\nElaine Shi (Co-chair)\n\nGiuli a Fanti (Co-chair)\n\nBryan Parno\n\nDavid Wu (University of Texas at Aust in)\n\nAdditional Information\n\nIn Person and Zoom Participation. See ann ouncement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c785154 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: \nSpeaker: AFONSO TINOCO\, Ph.D. Student\, Computer Science De partment\,\nCarnegie Mellon University\n\nTalk Title: Towards Practical an d Verifiable Distributed Systems:\nApplications of Oblivious Algorithms\, Garbled Circuits and Formal\nMethods+\n\nIn my research\, I want to design and develop practically efficient and\nprovably secure distributed system s. To this end\, I combine applied\ncryptography and formal verification t ools. The goal of this proposal\nis to provide primitives that can be used in distributed systems\, as\nwell as methodologies to verify consensus pr otocols\, to ensure the\nsecurity\, efficiency\, and correctness of distri buted systems.\nSpecifically\, the research focuses on three main areas: p ractical\nimplementations of oblivious algorithms for Trusted Execution\nE nvironments (TEEs)\; practical and verified implementations of Garbled\nRA M\; and methodologies to verify safety and liveness of consensus\nprotocol s. \n\nTEEs can be used to offer efficient crash fault nodes with\nconfid ential computations\; however\, most TEEs implementations leak the\npage-l evel memory access pattern to the host machine where the TEE is\nrunning. Therefore\, to guarantee confidential computations\, TEE\nprograms need no t only correct implementations but also to be memory\ntrace-oblivious. The re has been extensive theoretical research in\noblivious algorithms\; howe ver\, there is a gap with practical\nimplementations\, particularly in the TEE setting. In this proposal\, we\naim to close this gap\, providing an oblivious data structure library\nakin to C++'s STL\, and extending it wit h oblivious graph algorithms. \n\nTEEs require trust in the hardware manu facturer and a certain level of\nhardware/software integrity. In scenarios where this isn't possible\,\nGarbled Circuits can be used to provide equi valent secure processor\nguarantees based on cryptographic assumptions. To achieve an efficient\nGarbled Circuit processor\, Garbled RAM is necessar y\, and recent\ntheoretical advancements suggest using tristate circuits t o implement\nit. In this proposal\, we aim to achieve concretely more effi cient\nGarbled RAM constructions\, as well as provide methodologies to ver ify\nthe correctness of tristate circuits. \n\nFinally\, while TEEs and G arbled RAM aim to achieve secure\ncomputations\, ensuring the correctness of the underlying protocols\nthat use them is critical. We have previously developed a python DSL\nto verify safety properties of distributed system protocols. In this\nproposal\, we aim to extend this framework to verify liveness\nproperties of distributed system protocols\, focusing on proof\n automation and generalization.  \n\nThesis Committee: \n\nElaine Shi (C o-chair)\n\nRodrigo Rodrigues (Co-chair\, University of Lisbon\, Instituto Superior\nTécnico)\n\nBryan Parno\n\nPedro Adão (University of Lisbon\, Instituto Superior Técnico)\n\nJosé Fragoso (University of Lisbon\, Ins tituto Superior Técnico)\n\nAndrew Miller (University of Illinois Urbana- Champaign)\n\n \n\nAdditional Information\n\nIn Person and Zoom Participa tion. See announcement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c786556 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: \nSpeaker: BRIAN ZHANG\, Ph.D. Student\, Computer Science Depa rtment\,\nCarnegie Mellon University\n\nTalk Title: New Solution Concepts\ , Algorithms\, and Applications for\nExtensive-Form Games: Learning\, Corr elation\, Communication\, and Common\nKnowledge\n\nComputational game theo ry 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 recre ational and practical applications.\nIt has been instrumental in enabling superhuman AI from recreational\ngames such as two-player zero-sum games c hess\, go\, and heads-up poker\nto multiplayer games such as six-player po ker and Hanabi\, and even in\ngames involving human language such as Diplo macy. It has also\nempowered a growing range of non-recreational applicati ons\, such as\ntrading\, machine learning robustness and safety\, negotiat ion\, conflict\nresolution\, mechanism design\, information design\, secur ity\, political\ncampaigning\, and self-driving cars. \n\nThis thesis pus hes the boundary on computational game theory\,\nespecially in imperfect-i nformation sequential (extensive-form) games\,\nwhich are most prevalent i n practical applications both in zero-sum\ngames and beyond. We present ne w theoretical concepts and frameworks\,\nstate-of-the-art and often provab ly optimal algorithms for computing\nand learning equilibria\, and new way s to apply such algorithms to\nreal-world problems\, including problems in economics such as mechanism\nand information design.\n\nThe thesis contai ns four parts.\n\nI)  We develop new solution concepts and state-of-the-a rt complexity\nresults for adversarial team games. Among other results\, w e compute\nexact solutions to several variants of the popular game The\nRe sistance: Avalon with up to six players.\n\nII)  We develop an algorithmi c framework for generalized mechanism\ndesign that covers sequential mecha nism design\, sequential information\ndesign\, optimal correlated equilibr ia and more for the first time\, and\nreduces them to zero-sum games. This enables computation using any\nzero-sum game solving technique\, includin g deep reinforcement\nlearning.\n\nIII)  We develop the fastest learning algorithms for minimizing\nregret against linear and low-degree deviations \, which are the\ntightest solution concepts known to be efficiently learn able in games.\n\nIV)  We develop new techniques for subgame solving that work 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 knowled ge\,\ncurrently the best bot—for the game of dark chess. \n\nThesis Com mittee\n\nTuomas Sandholm (Chair)\n\nVincent Conitzer\n\nZico Kolter\n\nKe vin Leyton-Brown (University of British Columbia)\n\nAdditional Informatio n\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c78754c 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: \nSpeaker: ARJUN LAKSMIPATHY\, Ph.D. Student\, Computer Scienc e\nDepartment\, Carnegie Mellon University\n\nTalk Title: Contact Areas fo r Dexterous Manipulation\n\nHumans use their hands to effortlessly manipul ate objects of\narbitrarily complex geometries and physical properties eve ry day\;\nhowever\, adapting such manipulations to dexterous robots and vi rtual\ncharacters is an extremely difficult task. Understanding the ways i n\nwhich humans exploit contact to perform these manipulations has the\npo tential to greatly advance progress towards this goal. \n\nUnsurprisingly \, research efforts have analyzed contact in the context\nof dexterous man ipulation for decades. We now have numerous metrics\nfor evaluating grasp quality in terms of contacts\, efficient means of\ncomputing contact in ph ysical simulation\, and countless strategies\nexploiting contact correspon dences 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 cont acts in the real world are much more complicated. Instead\,\nreal bodies i nterface with one another via areas of contact which\ngreatly vary with th e geometries of contacting surfaces. If we wish to\nmodel the complexities of manipulations as they actually occur\, then\nwe must progress beyond s uch simplifying assumptions and deal with the\nmessy nature of reality. Th is thesis aims to do so by presenting\nframeworks and algorithms for the m odeling\, capture\, mutation\, and\nexploitation of contact areas. Our int ention is to establish the\nfoundations necessary to elevate contact areas to first-class\nprimitives and demonstrate their inherent value across a range of\npractical applications in dexterous manipulation and adjacent\nd omains.    \n\nFirst\, we introduce three novel models of contact areas alongside\noperations supported by each model which are fundamentally des igned to\nrun on real geometries rather than simple primitive shapes. Seco nd\, we\nintroduce a low cost approach for capturing human contacts from t he\nreal world. Then\, using these models\, we introduce: a new set of\nin tuitive artist tools for drafting high quality grasps\, a novel\nmotion re targeting pipeline for dexterous manipulations\, a novel\ncontact-driven c ontrol framework for dexterous robot hands\, and two\npractical extensions of our work. The contributions in this thesis are\nnot intended to be the last words\, but rather important first steps\ndesigned to promote future research in contact area modeling.\n\nThesis Committee\n\nNancy S. Pollar d (Chair)\n\nJessica K. Hodgins\n\nKeenan Crane\n\nC. Karen Liu (Stanford University)\n\nAdditional Information\n\nIn Person and Zoom Participation.   See announcement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c78884e 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: \nSpeaker: RUNTIAN ZHAI\, Ph.D. Student\, Computer Science Dep artment\,\nCarnegie Mellon University\n\nTalk Title: Learning Generalizabl e and Transferable Representations\nwith Big Models\n\nMachine learning ha s shifted to a new paradigm driven by\nrepresentation learning and foundat ion models\, big encoders that\nextract useful features from data. This th esis studies how big models\nlearn good representations\, and especially f ocuses on two aspects:\ngeneralization and transferability. For generaliza tion\, the problem is\nwhy big foundation models wouldn’t overfit as cla ssical theory\nsuggests.\n\nMy work proves a generalization bound that wor ks for big models\, by\nviewing them as algorithmic models instead of data models. For\ntransferability\, my work focuses on reweighting\, the most popular\nclass of methods. This talk will focus on one issue with reweight ing\nthat is its sensitivity to outliers\, and propose a solution that\nsi gnificantly improves the performance and stability of reweighting.\nFinall y\, I will propose two future work\, feature learning for tabular\ndata\, and combining multiple sources of prior knowledge.\n\nThesis Committee:\n\ nPradeep Ravikumar (Co-chair)\n\nZico Kolter (Co-chair)\n\nAndrej Risteski \n\nYuandong Tian (Meta AI)\n\nAdditional Information\n\nIn Person and Zoo m Participation. See announcement.\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c789452 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: \nSpeaker: SUHAS JAYARAM SUBRAMANYA\, Ph.D. Student\, Computer Science\nDepartment\, Carnegie Mellon University\n\nTalk Title: Efficient job-resource co-adaptivity for deep learning\nworkloads on large heteroge neous GPU clusters\n\nThe training performance of a deep learning (DL) tra ining job is\ndetermined by the number\, type and arrangement of the alloc ated GPU\nresources\, and the job parameters (like batch size and learning rate)\nused for execution. Modern clusters for DL training contain tens o f\nthousands of GPUs of many types\, and a cluster scheduler allocates\nGP Us to training jobs to maximize collective training progress in the\nclust er. Existing DL cluster schedulers cannot handle the large space\nof adapt ivity choices (i.e.\, combined space of GPU allocations and job\nparameter s) for large\, heterogeneous GPU clusters — many are not\nheterogeneity- aware\, few are adaptivity-aware\, and none scale to large\nclusters witho ut sacrificing allocation fidelity and cluster\nefficiency. \n\nIn this t hesis\, we introduce (a) a scheduler to facilitate efficient\njob-resource adaptivity for DL training jobs on large heterogeneous\nGPU clusters\, an d (b) a method to scale optimization-based scheduling\nto much larger clus ter sizes without sacrificing allocation fidelity\nand resource efficiency . Our adaptivity-aware scheduler\, Sia\, uses GPU\nresources judiciously t o learn a job's training performance across\ndifferent GPU types\, and con tinuously co-optimizes the GPU allocation\nand job execution parameters to maximize cluster-wide training\nprogress in heterogeneous GPU clusters. W e then scale Sia to large\ncluster sizes by modeling the scheduling policy as a continuous\noptimization problem. We show that it is possible to aug ment the\ninterface between a scheduler and the optimization problem solve r to\nefficiently track changes to the scheduling problem arising from\nch anging cluster conditions like job arrivals\, departures and phase\nchange s. We develop a prototype solver with the augmented interface\nfor the Sia scheduling policy that can efficiently recover allocations\nfor very larg e clusters. As an additional contribution\, we observe\nthat many other re source-allocation problems can also be formulated as\ncontinuous optimizat ion problems and can be solved both quickly and\nefficiently using our pro posed solver. \n\nThesis Committee:\n\nGreg Ganger (Chair)\n\nZhihao Jia\ n\nVirginia Smith\n\nAmar Phanishayee (Meta)\n\n \n\nAdditional Informati on\n DTSTAMP:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c78ab45 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:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c78ad82 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:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c78af5e 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:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c78b144 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:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c78b317 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:20260705T081607Z END:VEVENT BEGIN:VEVENT UID:6a4a12c78c725 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:20260705T081607Z END:VEVENT END:VCALENDAR