Update people + publication + news

richwill28 · richwill28 · commit 1d2428a70722 · 2025-10-01T15:33:39.000+08:00
diff --git a/content/authors/hongyi.huang/_index.md b/content/authors/hongyi.huang/_index.md
@@ -9,8 +9,10 @@ last_name: Huang
 # Organizational groups that you belong to (for People widget)
 #   Set this to `[]` or comment out if you are not using People widget.
 user_groups:
-  - Alumni
+  - Undergraduate Students
 
-alumni: BComp, 2025
+link: https://www.linkedin.com/in/hongyi-huang-7b103021b/
+
+alumni: BComp, 2026
 
 ---
diff --git a/content/authors/hongyi.huang/avatar.png b/content/authors/hongyi.huang/avatar.png
diff --git a/content/authors/theodore.lim/_index.md b/content/authors/theodore.lim/_index.md
diff --git a/content/authors/theodore.lim/avatar.png b/content/authors/theodore.lim/avatar.png
diff --git a/content/news/2024-06-26-alexey.md b/content/news/2024-06-26-alexey.md
@@ -2,5 +2,4 @@
 date: 2024-06-26
 ---
 
-
 **Alexey Paznikov** joins us as a Research Fellow!
diff --git a/content/news/2024-08-12-new-members.md b/content/news/2024-08-12-new-members.md
@@ -2,5 +2,4 @@
 date: 2024-08-16
 ---
 
-
 PhD student **Zihan Zhou**, and undergraduate students **Arsyad Kamili**, **Jed Koh Jin Keat**, **Ramanathan Kumarappan**, **Bryan Lim** and **David Zhu** join us!
diff --git a/content/news/2024-08-12-ourp-zheng-han.md b/content/news/2024-08-12-ourp-zheng-han.md
@@ -0,0 +1,5 @@
+---
+date: 2024-08-12
+---
+
+**Zheng Han** has been awarded the [NUS Outstanding Undergraduate Researcher Prize (OURP)](https://www.comp.nus.edu.sg/cug/honour/uni-award/) (AY2023/2024) for his work on efficient decrease-and-conquer algorithms for linearizability monitoring of concurrent data structures. Congratulations, Zheng Han!
diff --git a/content/news/2024-11-01-richard.md b/content/news/2024-11-01-richard.md
@@ -0,0 +1,5 @@
+---
+date: 2024-11-01
+---
+
+**Richard Willie** joins us as a Research Assistant!
diff --git a/content/news/2024-11-19-papers.md b/content/news/2024-11-19-papers.md
@@ -2,7 +2,6 @@
 date: 2024-11-19
 ---
 
-
 Papers accepted:
 
 1. [The Decision Problem for Regular First-Order Theories (POPL'25)](https://arxiv.org/pdf/2410.17185)
diff --git a/content/news/2025-08-11-ourp-jed.md b/content/news/2025-08-11-ourp-jed.md
@@ -0,0 +1,5 @@
+---
+date: 2025-08-11
+---
+
+**Jed** has been awarded the [NUS Outstanding Undergraduate Researcher Prize (OURP)](https://www.comp.nus.edu.sg/bytes/outstanding-undergraduate-researcher-prize-ourp-for-ay2024-2025/) (AY2024/2025) for his work on property testing trace closures of regular languages. Congratulations, Jed!
diff --git a/content/news/2025-09-01-michael.md b/content/news/2025-09-01-michael.md
@@ -0,0 +1,5 @@
+---
+date: 2025-09-01
+---
+
+**Michael Schwarz** joins us as a Research Fellow!
diff --git a/content/publication/2025/Efficient Decrease-And-Conquer Linearizability Monitoring/index.md b/content/publication/2025/Efficient Decrease-And-Conquer Linearizability Monitoring/index.md
@@ -0,0 +1,47 @@
+---
+title: "Efficient Decrease-And-Conquer Linearizability Monitoring"
+authors:
+- zheng.han.lee
+- umang
+date: "2025-08-16T00:00:00Z"
+
+# Publication type.
+# Accepts a single type but formatted as a YAML list (for Hugo requirements).
+# Enter a publication type from the CSL standard.
+publication_types: ["paper-conference"]
+
+# Publication name and optional abbreviated publication name.
+publication: "The ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications"
+publication_short: "OOPSLA 2025"
+
+abstract: |-
+    Linearizability has become the de facto correctness specification for implementations of concurrent data structures. While formally verifying such implementations remains challenging, linearizability monitoring has emerged as a promising first step to rule out early problems in the development of custom implementations, and serves as a key component in approaches that stress test such implementations. In this work, we investigate linearizability monitoring -- check if an execution history of an implementation is linearizable. While this problem is intractable in general, a systematic understanding of when it becomes tractable has remained elusive. We revisit this problem and first present a unified `decrease-and-conquer' algorithmic framework for linearizability monitoring. At its heart, this framework asks to identify special linearizability-preserving values in a given history -- values whose presence yields an equilinearizable sub-history when removed, and whose absence indicates non-linearizability. We prove that a polynomial time algorithm for the problem of identifying linearizability-preserving values, yields a polynomial time algorithm for linearizability monitoring, while conversely, intractability of this problem implies intractability of the monitoring problem. We demonstrate our framework's effectiveness by instantiating it for several popular data types -- sets, stacks, queues and priority queues -- deriving polynomial time algorithms for each, with the unambiguity restriction, where each insertion to the underlying data structure adds a distinct value. We optimize these algorithms to achieve the optimal log-linear time complexity by amortizing the cost of solving sub-problems through efficient data structures. Our implementation and evaluation on publicly available implementations show that our approach scales to large histories and outperforms existing tools.
+
+featured: false
+
+# links:
+# - name: ""
+#   url: ""
+url_pdf: https://arxiv.org/abs/2410.04581
+url_code:
+url_dataset: ''
+url_poster: ''
+url_project: ''
+url_slides: ''
+url_source: ''
+url_video: ''
+
+# Associated Projects (optional).
+#   Associate this publication with one or more of your projects.
+#   Simply enter your project's folder or file name without extension.
+#   E.g. `internal-project` references `content/project/internal-project/index.md`.
+#   Otherwise, set `projects: []`.
+projects: []
+
+# Slides (optional).
+#   Associate this publication with Markdown slides.
+#   Simply enter your slide deck's filename without extension.
+#   E.g. `slides: "example"` references `content/slides/example/index.md`.
+#   Otherwise, set `slides: ""`.
+slides: ""
+---
diff --git a/content/publication/2025/Efficient Timestamping for Sampling-Based Race Detection/index.md b/content/publication/2025/Efficient Timestamping for Sampling-Based Race Detection/index.md
@@ -0,0 +1,50 @@
+---
+title: "Efficient Timestamping for Sampling-Based Race Detection"
+authors:
+- Minjian Zhang
+- daniel.lim
+- Mosaad Al Thokair
+- umang
+- Mahesh Viswanathan
+date: "2025-06-13T00:00:00Z"
+
+# Publication type.
+# Accepts a single type but formatted as a YAML list (for Hugo requirements).
+# Enter a publication type from the CSL standard.
+publication_types: ["paper-conference"]
+
+# Publication name and optional abbreviated publication name.
+publication: "46th ACM SIGPLAN Conference on Programming Language Design and Implementation"
+publication_short: "PLDI 2025"
+
+abstract: |-
+    Dynamic race detection based on the happens before (HB) partial order has now become the de facto approach to quickly identify data races in multi-threaded software. Most practical implementations for detecting these races use timestamps to infer causality between events and detect races based on these timestamps. Such an algorithm updates timestamps (stored in vector clocks) at every event in the execution, and is known to induce excessive overhead. Random sampling has emerged as a promising algorithmic paradigm to offset this overhead. It offers the promise of making sound race detection scalable. In this work we consider the task of designing an efficient sampling based race detector with low overhead for timestamping when the number of sampled events is much smaller than the total events in an execution. To solve this problem, we propose (1) a new notion of freshness timestamp, (2) a new data structure to store timestamps, and (3) an algorithm that uses a combination of them to reduce the cost of timestamping in sampling based race detection. Further, we prove that our algorithm is close to optimal -- the number of vector clock traversals is bounded by the number of sampled events and number of threads, and further, on any given dynamic execution, the cost of timestamping due to our algorithm is close to the amount of work any timestamping-based algorithm must perform on that execution, that is it is instance optimal. Our evaluation on real world benchmarks demonstrates the effectiveness of our proposed algorithm over prior timestamping algorithms that are agnostic to sampling.
+
+featured: false
+
+# links:
+# - name: ""
+#   url: ""
+url_pdf: https://dl.acm.org/doi/pdf/10.1145/3729252
+url_code:
+url_dataset: ''
+url_poster: ''
+url_project: ''
+url_slides: ''
+url_source: ''
+url_video: ''
+
+# Associated Projects (optional).
+#   Associate this publication with one or more of your projects.
+#   Simply enter your project's folder or file name without extension.
+#   E.g. `internal-project` references `content/project/internal-project/index.md`.
+#   Otherwise, set `projects: []`.
+projects: []
+
+# Slides (optional).
+#   Associate this publication with Markdown slides.
+#   Simply enter your slide deck's filename without extension.
+#   E.g. `slides: "example"` references `content/slides/example/index.md`.
+#   Otherwise, set `slides: ""`.
+slides: ""
+---
diff --git a/content/publication/2025/Program Skeletons for Automated Program Translation/index.md b/content/publication/2025/Program Skeletons for Automated Program Translation/index.md
@@ -0,0 +1,50 @@
+---
+title: "Program Skeletons for Automated Program Translation"
+authors:
+- Bo Wang
+- tianyu.li
+- Ruishi Li
+- umang
+- Prateek Saxena
+date: "2025-06-13T00:00:00Z"
+
+# Publication type.
+# Accepts a single type but formatted as a YAML list (for Hugo requirements).
+# Enter a publication type from the CSL standard.
+publication_types: ["paper-conference"]
+
+# Publication name and optional abbreviated publication name.
+publication: "46th ACM SIGPLAN Conference on Programming Language Design and Implementation"
+publication_short: "PLDI 2025"
+
+abstract: |-
+    Translating software between programming languages is a challenging task, for which automated techniques have been elusive and hard to scale up to larger programs. A key difficulty in cross-language translation is that one has to re-express the intended behavior of the source program into idiomatic constructs of a different target language. This task needs abstracting away from the source language-specific details, while keeping the overall functionality the same. In this work, we propose a novel and systematic approach for making such translation amenable to automation based on a framework we call program skeletons. A program skeleton retains the high-level structure of the source program by abstracting away and effectively summarizing lower-level concrete code fragments, which can be mechanically translated to the target programming language. A skeleton, by design, permits many different ways of filling in the concrete implementation for fragments, which can work in conjunction with existing data-driven code synthesizers. Most importantly, skeletons can conceptually enable sound decomposition, i.e., if each individual fragment is correctly translated, taken together with the mechanically translated skeleton, the final translated program is deemed to be correct as a whole. We present a prototype system called SKEL embodying the idea of skeleton-based translation from Python to JavaScript. Our results show promising scalability compared to prior works. For 9 real-world Python programs, some with more than about 1k lines of code, 95% of their code fragments can be automatically translated, while about 5% require manual effort. All the final translations are correct with respect to whole-program test suites.
+
+featured: false
+
+# links:
+# - name: ""
+#   url: ""
+url_pdf: https://dl.acm.org/doi/pdf/10.1145/3729287
+url_code:
+url_dataset: ''
+url_poster: ''
+url_project: ''
+url_slides: ''
+url_source: ''
+url_video: ''
+
+# Associated Projects (optional).
+#   Associate this publication with one or more of your projects.
+#   Simply enter your project's folder or file name without extension.
+#   E.g. `internal-project` references `content/project/internal-project/index.md`.
+#   Otherwise, set `projects: []`.
+projects: []
+
+# Slides (optional).
+#   Associate this publication with Markdown slides.
+#   Simply enter your slide deck's filename without extension.
+#   E.g. `slides: "example"` references `content/slides/example/index.md`.
+#   Otherwise, set `slides: ""`.
+slides: ""
+---

-Original file line number
+Diff line change
@@ @@ -0,0 +1,5 @@ @@
 +---
 +date: 2024-08-12
 +---
++
 +**Zheng Han** has been awarded the [NUS Outstanding Undergraduate Researcher Prize (OURP)](https://www.comp.nus.edu.sg/cug/honour/uni-award/) (AY2023/2024) for his work on efficient decrease-and-conquer algorithms for linearizability monitoring of concurrent data structures. Congratulations, Zheng Han!