30 citations · 97 across the 29 of their papers we have counts for
30 papers
Certified but Private: Scalable Zero-Knowledge Proofs for Neural Network Guarantees
Youwei Zhong, Ben Merbaum, Timos Antonopoulos +4
With the growing deployment of machine learning models, formal guarantees of the robustness and fairness of these models have become increasingly important in safety-critical and l…
Learning GR(1) Specifications from Traces
Sam Nicholas Kouteili, William Fishell, Mark Santolucito +1
Constrained specification mining enables the automatic discovery of desired properties from system traces. Generalized Reactivity of Rank 1, or GR(1), is a fragment of LTL with pol…
Report on the Designing Accountable Software Systems Workshop
Catherine Albiston, Travis Breaux, Kat Dearstyne +13
The Workshop on Designing Accountable Software Systems (DASS) was convened in November 2024 with support from the U.S. National Science Foundation to engage a wide range of current…
Learning How to Cube
Ferhat Erata, Sam Kouteili, Thanos Typaldos +4
Despite the effectiveness of Cube-and-Conquer (C&C) for solving challenging Boolean Satisfiability (SAT) problems, no prior work has shown that transformer-based models can learn e…
Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications
Sam Nicholas Kouteili, William Fishell, Christian Scaff +2
Mining specifications from execution traces presents an automated way of capturing characteristic system behaviors. However, existing approaches are largely restricted to Boolean a…
A Systematic Study of Time Limit Exceeded Errors in Online Programming Assignments
Jialu Zhang, Jialiang Gu, Wangmeiyu Zhang +5
Online programming platforms such as Codeforces and LeetCode attract millions of users seeking to learn to program or refine their skills for industry interviews. A major challenge…
Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
John Kolesar, Shan Ali, Timos Antonopoulos +1
Zero-knowledge (ZK) protocols enable software developers to provide proofs of their programs' correctness to other parties without revealing the programs themselves. Regular expres…
NeuroStrata: Harnessing Neurosymbolic Paradigms for Improved Design, Testability, and Verifiability of Autonomous CPS
Xi Zheng, Ziyang Li, Ivan Ruchkin +2
Autonomous cyber-physical systems (CPSs) leverage AI for perception, planning, and control but face trust and safety certification challenges due to inherent uncertainties. The neu…
Learning Randomized Reductions
Ferhat Erata, Orr Paradise, Thanos Typaldos +4
Randomized self-reductions (RSRs) express using evaluated at random correlated points, enabling self-correcting programs, instance-hiding protocols, and applications in…
Scheherazade: Evaluating Chain-of-Thought Math Reasoning in LLMs with Chain-of-Problems
Stephen Miner, Yoshiki Takashima, Simeng Han +4
Benchmarks are critical for measuring Large Language Model (LLM) reasoning capabilities. Some benchmarks have even become the de facto indicator of such capabilities. However, as L…
Systematic Use of Random Self-Reducibility against Physical Attacks
Ferhat Erata, TingHung Chiu, Anthony Etim +7
This work presents a novel, black-box software-based countermeasure against physical attacks including power side-channel and fault-injection attacks. The approach uses the concept…
Quantum Circuit Reconstruction from Power Side-Channel Attacks on Quantum Computer Controllers
Ferhat Erata, Chuanqi Xu, Ruzica Piskac +1
The interest in quantum computing has grown rapidly in recent years, and with it grows the importance of securing quantum circuits. A novel type of threat to quantum circuits that…
Testing learning-enabled cyber-physical systems with Large-Language Models: A Formal Approach
Xi Zheng, Aloysius K. Mok, Ruzica Piskac +5
The integration of machine learning (ML) into cyber-physical systems (CPS) offers significant benefits, including enhanced efficiency, predictive capabilities, real-time responsive…
Analyzing Intentional Behavior in Autonomous Agents under Uncertainty
Filip Cano Córdoba, Samuel Judson, Timos Antonopoulos +5
Principled accountability for autonomous decision-making in uncertain environments requires distinguishing intentional outcomes from negligent designs from actual accidents. We pro…
'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions
Samuel Judson, Matthew Elacqua, Filip Cano +4
Principled accountability in the aftermath of harms is essential to the trustworthy design and governance of algorithmic decision making. Legal theory offers a paramount method for…
Towards Automated Detection of Single-Trace Side-Channel Vulnerabilities in Constant-Time Cryptographic Code
Ferhat Erata, Ruzica Piskac, Victor Mateu +1
Although cryptographic algorithms may be mathematically secure, it is often possible to leak secret information from the implementation of the algorithms. Timing and power side-cha…
Repairing Bugs in Python Assignments Using Large Language Models
Jialu Zhang, José Cambronero, Sumit Gulwani +4
Students often make mistakes on their introductory programming assignments as part of their learning process. Unfortunately, providing custom repairs for these mistakes can require…
Automated Feedback Generation for Competition-Level Code
Jialu Zhang, De Li, John C. Kolesar +2
Competitive programming has become a popular way for programmers to test their skills. Large-scale online programming contests attract millions of experienced programmers to compet…
IVeri: Privacy-Preserving Interdomain Verification
Ning Luo, Qiao Xiang, Timos Antonopoulos +3
In an interdomain network, autonomous systems (ASes) often establish peering agreements, so that one AS (agreement consumer) can influence the routing policies of the other AS (agr…
ETAP: Energy-aware Timing Analysis of Intermittent Programs
Ferhat Erata, Arda Goknil, Eren Yıldız +4
Energy harvesting battery-free embedded devices rely only on ambient energy harvesting that enables stand-alone and sustainable IoT applications. These devices execute programs whe…
Can Pre-trained Language Models be Used to Resolve Textual and Semantic Merge Conflicts?
Jialu Zhang, Todd Mytkowicz, Mike Kaufman +2
Program merging is standard practice when developers integrate their individual changes to a common code base. When the merge algorithm fails, this is called a merge conflict. The…
Succinct Explanations With Cascading Decision Trees
Jialu Zhang, Yitan Wang, Mark Santolucito +1
The decision tree is one of the most popular and classical machine learning models from the 1980s. However, in many practical applications, decision trees tend to generate decision…
Grammar Filtering For Syntax-Guided Synthesis
Kairo Morton, William Hallahan, Elven Shum +2
Programming-by-example (PBE) is a synthesis paradigm that allows users to generate functions by simply providing input-output examples. While a promising interaction paradigm, synt…
Synthesizing Functional Reactive Programs
Bernd Finkbeiner, Felix Klein, Ruzica Piskac +1
Functional Reactive Programming (FRP) is a paradigm that has simplified the construction of reactive programs. There are many libraries that implement incarnations of FRP, using ab…