News People Research Courses Seminars Github
show-table
Patrick LaFontaine Some cool synthesis talk WANG 1004
Chris Wagner Using Property-Driven Reductions to Verify Distributed Systems Automatically WANG 1004
Satnam Singh TBD TBD
Michael Borkowski Mechanizing Refinement Types (POPL'24) WANG 1004
Rachit Nigam Modular Abstractions for Hardware Design WANG 1004
Danning ReSym: Harnessing LLMs to Recover Variable and Data Structure Symbols from Stripped Binaries (CCS 2024 Practice talk) LWSN 3102A/B
Adhitha Dias SparseAuto: An Auto-Scheduler for Sparse Tensor Computations Using Recursive Loop Nest Restructuring (OOPSLA 2024 Practice talk) WANG 1004
Ning Luo Privacy-preserving SAT solving with zero-knowledge proofs LAWSON 3102
Mingshuai Chen Reasoning about loopy probabilistic programs BHEE 317
Ben, Milind, and Other Faculty Field-Specific RCR Training Roundtable LWSN 3102A/B
Julia Belyakova Decidable subtyping for the Julia language (PLDI'24) LWSN 3102A/B
Ben Delaware Inaugural PurPL Seminar Lawson 3102
Vidush Singhal Optimizing Layout Of Recursive Datatypes with Marmoset WANG 1004
Durga Mandarapu Arkade: k-Nearest Neighbor Search With Non-Euclidean Distances using GPU Ray Tracing LWSN 3102A/B
Syed Usman Leo: Online ML-based Traffic Classification at Multi-Terabit Line Rate WANG 1004
Jenna DiVincenzo Gradual Verification: Assuring Programs Incrementally LWSN 3102A/B
Samia Kabir Is Stack Overflow Obsolete? An Empirical Study of the Characteristics of ChatGPT Answers to Stack Overflow Questions WANG 1004
Patrick LaFontaine Coverage-based Synthesis LWSN 3102A/B
Yuantian Ding Enhanced Enumeration of Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations LWSN 3102A/B
Sishuai Gong Efficient Kernel Concurrency Testing through Scalable Kernel Behavior Analysis WANG 1004
Durga Mandarapu Discrete Collision Detection using GPU Ray Tracing LWSN 3102A/B
Qianchuan Ye Language-based Techniques for Policy-Agnostic Oblivious Computation LWSN 3102A/B
Guannan Wei Types and Metaprogramming for Correct, Safe, and Performant Software Systems WANG 1004
Mikail Khan Interactive VSA Synthesis LWSN 3102A/B
Ben Delaware Welcome Back! WANG 1004
Jacob Laurel Scott (UIUC) Abstractly Interpreting Differentiable Programming WANG 1004
Julia Belyakova Julia: Practical Restrictions for a Scientific-Computing Language LWSN 3102A/B
Dulani Wijayarathne and Vickrant Sreekanth PEAVS: Parallel Encrypted Arithmetic Vector Scheduling for Optimized FHE Computations WANG 1004
David Deng Reachability Types with Destructive Effects WANG 1004
Sriram Sankaranarayanan Learning Switched Models from Data LWSN 3102A/B
Ashish Mishra Hegel: A Component-based Synthesis in Sparse Libraries WANG 1004
Artem Pelenitsyn Type Stability in Julia: A Simple and Efficient Optimization Technique LWSN 3102A/B
Ziyang Li(UPenn) Scallop, a Language for Neurosymbolic Programming WANG 1004
Shao-Yu Huang RTSS Practice Talk: RTailor: Parameterizing Soft Error Resilience for Mixed-Criticality Real-Time Systems LWSN 3102A/B
Yuchen Zhou MICRO Practice Talk: SweepCache: Intermittence-Aware Cache on the Cheap LWSN 3102A/B
Jianping Zeng Persistent Processor Architecture WANG 1004
Robert Rand Quantum Computing from a PL Perspective LWSN 3102A/B
Yao Li 'Shallower' Embeddings for Mechanized Reasoning LWSN 3102
Yifeng Di Software Entity Recognition with Noise-Robust Learning LWSN 3102
Paschal Amusuo Systematically Detecting Packet Validation Vulnerabilities in Embedded Network Stacks LWSN 3102A/B
Shangshu Qian Vicious Cycles in Distributed Software Systems MSEE 239
Ben Delaware Welcome Back! LWSN 3102A/B
Qianchuan Ye Taype: a Policy-Agnostic Language for Oblivious Computation' LAWSON 3102
Robert Dickerson KestRel: Relational Verification using E-Graphs for Program Alignment LAWSON 3102
Vani Nagarajan RT-kNNS Unbound: Using RT Cores to Accelerate Unrestricted Neighbor Search LAWSON 3102
Yongwei Yuan Trace-Guided Inductive Synthesis of Recursive Functional Programs (virtual) LAWSON 3102
Zhe Zhou Covering All the Bases: Type-based Verification of Test Input Generators LAWSON 3102
Wenxin Jiang An Empirical Study of Pre-Trained Model Reuse in the Hugging Face Deep Learning Model Registry LAWSON 3102
Jan Vitek Reusing Just-in-Time Compiled Code LAWSON 3102
Nan Jiang KNOD: Domain Knowledge Distilled Tree Decoder for Automated Program Repair Impact of Code Language Models on Automated Program Repair WANG 1004
Vani Nagarajan RT-DBSCAN: Accelerating DBSCAN using Ray Tracing Hardware WANG 1004
Zikang Co-learning Planning and Control Policies Using Differentiable Formal Task Constraints LAWSON 3102
Qianchuan Taype: a Policy-Agnostic Language for Oblivious Computation WANG 1004
Zhe Type-based Verification of Test Input Generators LAWSON 3102
Dan Plyukhin A Language For Low-Latency Distributed Systems (WIP) WANG 1004
Yuqun Zhang Demystifying Fuzzing Strategies LAWSON 3102
Raghav Coyote: A Compiler for Vectorizing Encrypted Arithmetic Circuits WANG 1004
Oliver Diamonds and Rust LAWSON 3102
Caleb Helbling Juniper: a Functional Reactive Programming Language for the Arduino WANG 1004
Jonathan Rosenthal DisGUIDE: Disagreement-Guided Data-Free Model Extraction LAWSON 3102
Kirshanthan Sundararajah Abstractions for Taming Irregularity at the Top WANG 1004
Yanjun Wang Comparative Synthesis: Learning Near-Optimal Network Designs by Query LWSN 3012
Guannan Wei Compiling and Controlling Symbolic Execution WANG 1004
Rob Dickerson Modular Deductive Verification of Relational ∀∃ Properties LAWSON 3102
Charitha Saumya Merging Similar Control-Flow Regions in LLVM for Performance and Code Size Benefits LAWSON 3102
Everyone Elevator Pitch Roundtable WANG 1004
Chris Wagner Process Cutoffs for Safety Verification of Parameterized Client-Server Systems LAWSON 3102
Ashish Mishra Specification-Guided Component-Based Synthesis from Effectful Libraries WANG 1004
Yongwei Yuan Trace-guided Example-based Synthesis of Recursive Programs LAWSON 3102
Favonia Building a Proof Assistant WANG 1004
Anxhelo Xhebraj What If We Don’t Pop the Stack? The Return of Second-Class Values LAWSON 3102
Adhitha Dias SparseLNR: Accelerating Sparse Tensor Computations Using Loop Nest Restructuring WANG 1004
Wenxin Deep Learning Model Reengineering: An Exploratory Case Study on Computer Vision Zoom
Xin and Efe Exploiting Input Sanitization for Regex Denial of Service Zoom
Jiannan Wang EAGLE: Creating Equivalent Graphs to Test Deep Learning Libraries Zoom
Favonia Logarithm and Program Testing Zoom
Yuan Tian Interactive SQL Query Synthesis via Structured Explanations Zoom
Ian Sweet Toward a Probabilistically Oblivious Language for Secure Multiparty Computation Zoom
Akash Lal Learning-based Concurrency Testing Zoom
Qianchuan Scrap your boilerplate definitions in 10 lines of Ltac! Zoom
Qianchuan Oblivious Algebraic Data Types Zoom
Chris Wagner Bounded Verification of Doubly-Unbounded Parameterized Systems Zoom
Peter Goodman Dr. Lojekyll - The Mr. Hyde of Datalog Engines Zoom
Pedro Abreu A Mixed Embedding of OCaml GADTs in Coq Zoom
Chaitanya Parallel Gibbon: reconciling parallelism and dense data representations Zoom
Zhe Zhou Data-Driven Abductive Inference of Library Specifications Zoom
Kia Multi-modal Program Inference: a Marriage of Pre-trained Language Models and Component-based Synthesis Zoom
Nouraldin Jaber QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems Zoom
Raghav Malik Vectorized Secure Evaluation of Decision Forests Zoom
Charitha Saumya CFM: SIMT Thread Divergence Reduction by Melding Similar Control-Flow Regions in GPGPU Programs Zoom
Caleb Helbling Solving the Funarg Problem with Static Types Zoom
Nan Jiang CURE: Code-Aware Neural Machine Translation for Automatic Program Repair Zoom
Qianchuan Ye Oblivious Algebraic Data Types Zoom
Chris Wagner Modeling and Verification for (Multi-)Parameterized Systems Zoom
Kirshanthan Sundararajah Skewing Recursion for Fun and Profit Zoom
Kia Rahmani Repairing Serializability Bugs in Distributed Database Programs via Automated Schema Refactoring Zoom
Pedro da Costa Abreu Translating GADTs from OCaml to Coq Zoom
Raghav Malik Vectorizing Secure Evaluation of Decision Forests Zoom
Charitha Saumya Gusthinna Waduge Merging Similar Control Flow for SIMT Divergence Reduction in GPGPUs Zoom
Yanjun Wang Reasoning About Recursive Tree Traversals Zoom
Walt Woods (Galois) Understanding de facto formats through grammar inference, and why reinforcement learning might help Zoom
Aviral Goel On the Design, Implementation, and Use of Laziness in R Zoom
Supun Abeysinghe Generative Programming for Constructing Efficient End-to-End Data Science Pipelines Zoom
Elena Glassman Increasing the Power of [Human+Program Synthesis] through Interface Design Zoom
Rob Dickerson Relational Reasoning with Specifications Zoom
Roopsha Samanta MANTIS: Semantics-driven Inductive Program Synthesis Zoom
James Bornholt Program Synthesis in the Small Zoom
Kirshanthan Sundararajah PolyRec: Composable, Sound Transformations of Nested Recursion and Loops Zoom
Ilya Sergey CoSplit: Practical Smart Contract Sharding with Static Program Analysis Zoom
Shaz Qadeer Reifying Concurrent Programs Zoom
Chris Wagner and Nouraldin Jaber Discover[i] Zoom
Anmol Sahoo Replicated Datatypes Zoom
Pedro Abreu Freer Monads LWSN 3102A/B
Qianchuan Ye LWSN 3102A/B
Logan Kulinski LWSN 3102A/B
Eric Bond LWSN 3102A/B
Chris Wagner SQLizer LWSN 3102A/B
Nouralidn Jaber Discover[i] LWSN 3102A/B
Rob Dickerson Automated API Migration LWSN 3102A/B
Fei Wang Learn 2QBF CEGAR Solver Heuristics via Graph Neural Networks LWSN 3102A/B
Yuanjing Shi Building transactional support on top of Apache Cassandra LWSN 3102A/B
Laith Saed Sound, Fine-Grained Traversal Fusion for Heterogeneous Trees LWSN 3102A/B
Dan Zheng Swift for TensorFlow, a first-class language for machine learning LWSN 3102A/B
Youyou Cong Handling Delimited Continuations with Dependent Types LWSN 3102A/B
Rishabh Singh Neural Meta Program Synthesis LWSN 3102A/B
Gowtham Kaki Safe Replication for Bounded Concurrency Verification LWSN 3102A/B
MWPLS Break LWSN 3102A/B
David Perry Semantic Clustering of Programming Assignments via Model Counting and Value Variations LWSN 3102A/B
Kirshanthan Sundararajah Scheduling Transformations and Dependence Tests for Recursive Programs LWSN 3102A/B
POPL Rebuttal Round Table LWSN 3102A/B
Guannan Wei Refunctionalization of Abstract Abstract Machine LWSN 3102A/B
Fei Wang Lantern, a Machine Learning framework built on Delimited Continuations and Staging LWSN 3102A/B
David Perry Semantic Clustering of Programming Assignments via Model Counting and Value Variations LWSN 3102A/B
Open Open WANG 1004
Open Open LWSN 3102A/B
Open Open TBD
Open Open LWSN 3102A/B
Open Open WANG 1004
Open Open LWSN 3102A/B
Eric Bond Quantum Programming - Theory and Practice LWSN 3102A/B
Nathan Burow CFIXX: Object Type Integrity WANG 1004
Cancelled Cancelled LWSN 3102A/B
Kenneth Adam Miller Probabilistically Convergent Minimal Superset Disassembly WANG 1004
Fei Wang Learning SAT solver heuristics with Deep Reinforcement Learning in the style of Alpha(Go) Zero LWSN 3102A/B
Kiarash Rahmani Anomalie-guided Incremental Program Repair WANG 1004
Guannan Wei Precise Reasoning with Structured Heaps and Collective Operations à la Map/Reduce LWSN 3102A/B
Ben Delaware Spring 2018 Kickoff LWSN 3102A/B
Shengwei An Robust Example-based Synthesis WANG 1004
Thomas Wahl Stabilizing Numeric Programs against Platform Uncertainties LWSN 3102A/B
Dan Zheng DLVM: A Compiler Framework for Deep Learning DSLs WANG 1004
Andrew Appel Verifiable C, a logic and tool for deductive verification of the correctness of C programs LWSN 3102A/B
Everybody Ongoing Work Roundtable WANG 1004
James Decker Flare: A Brief Look into Optimizing UDFs in Spark LWSN 3102A/B
Kanjing Huang DRYADSYNTH : A Concolic SyGuS Solver WANG 1004
Laith Sakka Tree Fuser: A Framework for Analyzing and Fusing General Recursive Tree Traversals LWSN 3102A/B
Cyrus Omar Toward Semantic Foundations for Live Programming Environments LWSN 3102A/B
Yanjun Wang A Decidable Logic for Tree Data-Structures with Measurements WANG 1004
Kenneth Adam Miller The Case for Quantum Computing: Basics Techniques and Applications LWSN 3102A/B
Nikhil Hegde SPIRIT: A Framework for Creating Distributed Recursive Tree Applications EE 317
Gowtham Kaki Mergeable Types LWSN 3102A/B
Suyash Optimizing Recursive Task Parallel Programs LWSN 3102A/B
Zach Tatlock Automated Formal Verification for Border Gateway Protocol Configurations LWSN 3102
Fei Dependent Types for Scala LWSN 3102
James and Greg Flare: Optimizing UDFs in Spark LWSN 3102A/B
Krish Locality Transformations for Nested Recursive Iteration Spaces MSEE 239
Leo Osvald Gentrification Gone too Far? Affordable 2nd-Class Values for Fun and (Co-)Effect LWSN 3102A/B
Nathan H Burow Context Flow Integrity LWSN 3102A/B
Kia Rahmani Synthesis of Runtime Systems for Weak Consistency Enforcement LWSN 3102A/B
Scott Carr Optimizations in the Rust Compiler EE 317
Tiark, Ben, Roopsha POPL 2017 LWSN 3102A/B
Ben Spring Semester Kickoff HAAS 111