Title
Topic
-
‘On Tolerance of Discrete Systems With Respect to Transition Perturbations’
“Control systems should enforce a desired property for both expected/modeled situations as well as unexpected/unmodeled environmental situations. Existing methods focus on designing controllers to enforce the desired property only when the environment behaves as expected. However, these methods lack discussion on how the system behaves when the environment is perturbed. In this paper, we propose an approach for analyzing discrete-state control systems with respect to their tolerance against environmental perturbations.” Find the paper and full list of authors in Discrete Event Dynamic Systems.
-
‘Code Coverage Criteria for Asynchronous Programs’
“Asynchronous software often exhibits complex and error-prone behaviors that should be tested thoroughly. … Traditional code coverage criteria do not adequately reflect completion, interactions and error handling of asynchronous operations. This paper proposes novel test adequacy criteria for measuring: (i) completion of asynchronous operations in terms of both successful and exceptional execution, (ii) registration of reactions for handling both possible outcomes and (iii) execution of said reactions through tests.” Find the paper and full list of authors in the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering.
-
‘Increasing the Responsiveness of Web Applications by Introducing Lazy Loading’
“Front-end developers want their applications to contain no more code than is needed in order to minimize the amount of time that elapses between visiting a web page and the page becoming responsive. However, front-end code is typically written in JavaScript … and tends to rely heavily on third-party packages. … One way to combat such bloat is to lazily load external packages on an as-needed basis. … In this work, we propose an approach for automatically introducing lazy loading of third-party packages in JavaScript applications.” Find the paper and authors list in the 2023 IEEE International Conference on Automated…
-
‘Testing the Limits of Neural Sentence Alignment Models on Classical Greek and Latin Texts and Translations’
“The Greek and Latin classics, like many other ancient texts, have been widely translated into a variety of languages over the past two millennia. … Aligning the corpus of classical texts and translations at the sentence and word level would provide a valuable resource for studying translation theory, digital humanities and natural language processing (NLP). … This paper evaluates and examines the limits of such state-of-the-art models for cross-language sentence embedding and alignment of ancient Greek and Latin texts with translations into English, French, German and Persian.” Find the paper and authors list in the Computational Humanities Research Conference 2023…
-
‘Automatic Collation for Diversifying Corpora: Commonly Copied Texts as Distant Supervision for Handwritten Text Recognition’
“Handwritten text recognition (HTR) has enabled many researchers to gather textual evidence from the human record. … To build generalized models for Arabic-script manuscripts, perhaps one of the largest textual traditions in the pre-modern world, we need an approach that can improve its accuracy on unseen manuscripts and hands without linear growth in the amount of manually annotated data. We propose Automatic Collation for Diversifying Corpora (ACDC), taking advantage of the existence of multiple manuscripts of popular texts.” Find the paper and full list of authors in the Computational Humanities Research Conference 2023 proceedings.
-
‘Proving Calculational Proofs Correct’
“Teaching proofs is a crucial component of any undergraduate-level program that covers formal reasoning. We have developed a calculational reasoning format and refined it over several years of teaching a freshman-level course, ‘Logic and Computation,’ to thousands of undergraduate students. In our companion paper, we presented our calculational proof format [and] gave an overview of the calculational proof checker (CPC) tool that we developed. … In this paper, we dive deeper into the implementation details of CPC, highlighting how proof validation works, which helps us argue that our proof checking process is sound.” Find the paper and authors list at…
-
‘Verification of GossipSub in ACL2s’
“GossipSub is a popular new peer-to-peer network protocol designed to disseminate messages quickly and efficiently by allowing peers to forward the full content of messages only to a dynamically selected subset of their neighboring peers (mesh neighbors) while gossiping about messages they have seen with the rest. Peers decide which of their neighbors to graft or prune from their mesh locally and periodically using a score for each neighbor. … In this paper, we present a detailed description of our model.” Find the paper and full list of authors at ArXiv.
-
‘Using Counterexample Generation and Theory Exploration To Suggest Missing Hypotheses’
“Newcomers to ACL2 are sometimes surprised that ACL2 rejects formulas that they believe should be theorems. … Counterexample generation (cgen) is a technique that helps by giving the user a number of counterexamples (and also witnesses) to the formula, e.g., letting the user know that the intended theorem is false when X is equal to 10. In this paper we describe a tool called DrLA that goes further by suggesting additional hypotheses that will make the theorem true.” Find the paper and full list of authors at ArXiv.
-
‘A Case Study in Analytic Protocol Analysis in ACL2’
“When verifying computer systems we sometimes want to study their asymptotic behaviors, i.e., how they behave in the long run. In such cases, we need real analysis, the area of mathematics that deals with limits and the foundations of calculus. In a prior work, we used real analysis in ACL2s to study the asymptotic behavior of the RTO computation. … In this paper, we explore different approaches to proving the above result in ACL2(r) and ACL2s, from the perspective of a relatively new user to each.” Find the paper and full list of authors at ArXiv.
-
‘AIM: Automatic Interrupt Modeling for Dynamic Firmware Analysis’
“The security of microcontrollers, which drive modern IoT and embedded devices, continues to raise major concerns. Within a microcontroller (MCU), the firmware is a monolithic piece of software that contains the whole software stack, whereas a variety of peripherals represent the hardware. As MCU firmware contains vulnerabilities, it is ideal to test firmware with off-the-shelf software testing techniques, such as dynamic symbolic execution and fuzzing. … In this paper, we present AIM — a generic, scalable, and hardware-independent dynamic firmware analysis framework that supports unemulated MCU peripherals by a novel interrupt modeling mechanism.” Find the paper and full authors list…
-
‘OAuth 2.0 Redirect URI Validation Falls Short, Literally’
“OAuth 2.0 requires a complex redirection trail between websites and Identity Providers (IdPs). In particular, the ‘redirect URI’ parameter included in the popular Authorization Grant Code flow governs the callback endpoint that users are routed to, together with their security tokens. The protocol specification, therefore, includes guidelines on protecting the integrity of the redirect URI. … We analyze the OAuth 2.0 specification in light of modern systems-centric attacks and reveal that the prescribed redirect URI validation guidance exposes IdPs to path confusion and parameter pollution attacks.” Find the paper and authors list in the 39th Annual Computer Security Applications Conference…
-
‘Immunizing Backdoored PRGs’
“A backdoored Pseudorandom Generator (PRG) is a PRG which looks pseudorandom to the outside world, but a saboteur can break PRG security by planting a backdoor into a seemingly honest choice of public parameters, pk, for the system. Backdoored PRGs became increasingly important due to revelations about NIST’s backdoored Dual EC PRG, and later results about its practical exploitability. … Unfortunately, we show that simple standard model proposals of (including the XOR function) provably do not work in our setting.” Find the paper and full list of authors at Cryptology ePrint Archive.
-
‘EVORA: Deep Evidential Traversability Learning for Risk-Aware Off-Road Autonomy’
“Traversing terrain with good traction is crucial for achieving fast off-road navigation. Instead of manually designing costs based on terrain features, existing methods learn terrain properties directly from data via self-supervision, but challenges remain to properly quantify and mitigate risks due to uncertainties in learned models. This work efficiently quantifies both aleatoric and epistemic uncertainties by learning discrete traction distributions and probability densities of the traction predictor’s latent features.” Find the paper and full list of authors at ArXiv.
-
‘How To Evaluate Blame for Gradual Types, Part 2’
“Equipping an existing programming language with a gradual type system requires two major steps. The first and most visible one in academia is to add a notation for types and a type checking apparatus. The second, highly practical one is to provide a type veneer for the large number of existing untyped libraries. … When programmers create such typed veneers for libraries, they make mistakes that persist and cause trouble. … This paper provides a first, surprising answer to this [dilemma] via a rational-programmer investigation.” Find the paper and full list of authors in the proceedings of the ACM on…
-
‘How Profilers Can Help Navigate Type Migration’
“Sound migratory typing envisions a safe and smooth refactoring of untyped code bases to typed ones. However, the cost of enforcing safety with run-time checks is often prohibitively high, thus performance regressions are a likely occurrence. … In principal though, migration could be guided by off-the-shelf profiling tools. To examine this hypothesis, this paper follows the rational programmer method and reports on the results of an experiment on tens of thousands of performance-debugging scenarios via seventeen strategies for turning profiler output into an actionable next step.” Find the paper and authors list in the proceedings of the ACM on Programming…
-
‘Content-Based Search for Deep Generative Models’
“The growing proliferation of customized and pretrained generative models has made it infeasible for a user to be fully cognizant of every model in existence. To address this need, we introduce the task of content-based model search: given a query and a large set of generative models, finding the models that best match the query. As each generative model produces a distribution of images, we formulate the search task as an optimization problem to select the model with the highest probability of generating similar content as the query.” Find the paper and authors list in SIGGRAPH Asia 2023 Conference Papers.
-
‘Concept Sliders: LoRA Adaptors for Precise Control in Diffusion Models’
“We present a method to create interpretable concept sliders that enable precise control over attributes in image generations from diffusion models. Our approach identifies a low-rank parameter direction corresponding to one concept while minimizing interference with other attributes. A slider is created using a small set of prompts or sample images; thus slider directions can be created for either textual or visual concepts. Concept Sliders are plug-and-play: they can be composed efficiently and continuously modulated, enabling precise control over image generation.” Find the paper and full list of authors at ArXiv.
-
‘Local Computation Algorithms for Maximum Matching: New Lower Bounds’
“We study local computation algorithms (LCA) for maximum matching. An LCA does not return its output entirely, but reveals parts of it upon query. For matchings, each query is a vertex v; the LCA should return whether v is matched — and if so to which neighbor — while spending a small time per query. In this paper, we prove that any LCA that computes a matching that is at most an additive of ϵn smaller than the maximum matching in n-vertex graphs of maximum degree Δ must take at least Δ^Ω(1/ε) time.” Find the paper and full list of authors at ArXiv.
-
‘Exponentially Faster Massively Parallel Maximal Matching’
” The study of approximate matching in the Massively Parallel Computations (MPC) model has recently seen a burst of breakthroughs. Despite this progress, we still have a limited understanding of maximal matching which is one of the central problems of parallel and distributed computing. … In this work, we close this gap by providing a novel analysis of an extremely simple algorithm, which is a variant of an algorithm conjectured to work by Czumaj, Lacki, Madry, Mitrovic, Onak, and Sankowski.” Find the paper and full list of authors at the Journal of the ACM.
-
‘An Alternative to Regulation: The Case for Public AI’
“Can governments build AI? In this paper, we describe an ongoing effort to develop ‘public AI’ — publicly accessible AI models funded, provisioned and governed by governments or other public bodies. Public AI presents both an alternative and a complement to standard regulatory approaches to AI, but it also suggests new technical and policy challenges. We present a roadmap for how the ML research community can help shape this initiative and support its implementation and how public AI can complement other responsible AI initiatives.” Find the paper and full list of authors at ArXiv.
-
‘Future Lens: Anticipating Subsequent Tokens From a Single Hidden State’
“We conjecture that hidden state vectors corresponding to individual input tokens encode information sufficient to accurately predict several tokens ahead. More concretely, in this paper we ask: Given a hidden (internal) representation of a single token at position t in an input, can we reliably anticipate the tokens that will appear at positions ≥t+2? … We find that, at some layers, we can approximate a model’s output with more than 48% accuracy with respect to its prediction of subsequent tokens through a single hidden state.” Find the paper and full list of authors at ArXiv.
-
‘Accomodating User Expressivity While Maintaining Safety for a Virtual Alcohol Misuse Counselor’
“Client-centered counseling, in which individuals are prompted to talk about their behavior, is the standard treatment for Alcohol misuse. However, open-ended conversations with virtual agent counselor raise potential safety concerns if the agent misunderstands and provides erroneous advice. … We present a hybrid dialog system that uses a machine-learning model to generate responses to individual client speech combined with a rule-based approach to transition through structured counseling sessions.” Find the paper and full list of authors in the proceedings of the 23rd ACM International Conference on Intelligent Virtual Agents.
-
‘Influencing Health-Related Decision Making and Therapeutic Alliance With Robot Mobility and Deixis’
“Recent trends and developments in robotics have enabled socially assistive mobile robotic platforms to be deployed in everyday human lives. These robots have the ability to navigate to a user’s location and engage in multimodal interactions to serve a variety of purposes such as promoting health behavior change. … We found that robot mobility, proxemics and deictic and verbal cuing have significant positive effects on compliance with the robot’s food recommendations and resulting nutritional quality of assembled meals.” Find the paper and full list of authors in the 32nd IEEE International Conference on Robot and Human Interactive Communication proceedings.
-
‘Keeping Users Engaged During Repeated Administration of the Same Questionnaire: Using [LLMs] to Reliably Diversify Questions’
“Standardized, validated questionnaires are vital tools in HCI research and healthcare, offering dependable self-report data. However, their repeated use in longitudinal or pre-post studies can induce respondent fatigue, impacting data quality via response biases and decreased response rates. We propose utilizing large language models (LLMs) to generate diverse questionnaire versions while retaining good psychometric properties. … Our findings highlight the potential of LLM-generated variants to invigorate questionnaires, fostering engagement and interest without compromising validity.” Find the paper and full list of authors at ArXiv.
-
‘Augmented Reality as a Visualization Technique for Scholarly Publications in Astronomy: An Empirical Evaluation’
“We present a mixed methods user study evaluating augmented reality (AR) as a visualization technique for use in astronomy journal publications. This work is motivated by the highly spatial nature of scientific visualizations employed in astronomy. … In this 52-person user study, we evaluate two AR approaches … as spatial 3D visualization techniques, as compared to a baseline 3D rendering on a phone. We identify a significant difference in mental and physical workload between the two AR conditions in men and women.” Find the paper and full list of authors in the 2023 IEEE Visualization and Visual Analytics proceedings.
-
‘Conversational Assessment of Mild Cognitive Impairment with Virtual Agents’
“Over 55 million adults worldwide have dementia, a syndrome characterized by deterioration in cognitive functioning. Screening for mild cognitive impairment is important to identify dementia early to facilitate diagnosis and initiate treatment that may modify the disease trajectory. However, standard cognitive screening tools are time-consuming, require expert administration, and make people feel as if they are being tested and are thus potentially stigmatizing. … We explored cognitive ability assessments using virtual agents, in which assessments are made during conversational dialogues.” Find the paper and full list of authors in the proceedings of the 23rd ACM International Conference on Intelligent Virtual…
-
‘Changing Parent Attitudes Towards HPV Vaccination by Including Adolescents in Multiparty Counseling Using Virtual Agents’
“Parental permission is required for medical care for children, and decisions may be made without incorporating children’s views, even for adolescents. We explore the impact of including adolescents in virtual agent-based multiparty health counseling to promote Human Papillomavirus (HPV) vaccination. … We found significant pre-post increases in parent intent to vaccinate their adolescent for both versions of the agent.” Find the paper and full list of authors in the proceedings of the 23rd ACM International Conference on Intelligent Virtual Agents.
-
‘Multiple Toddler Tracking in Indoor Videos’
“Multiple toddler tracking (MTT) involves identifying and differentiating toddlers in video footage. While conventional multi-object tracking (MOT) algorithms are adept at tracking diverse objects, toddlers pose unique challenges due to their unpredictable movements, various poses, and similar appearance. Tracking toddlers in indoor environments introduces additional complexities such as occlusions and limited fields of view. In this paper, we address the challenges of MTT and propose MTTSort, a customized method built upon the DeepSort algorithm.” Find the paper and full list of authors at ArXiv.
-
‘A Unified Approach for Resilience and Causal Responsibility With Integer Linear Programming (ILP) and LP Relaxations’
“What is a minimal set of tuples to delete from a database in order to eliminate all query answers? This problem is called ‘the resilience of a query’ and is one of the key algorithmic problems underlying various forms of reverse data management, such as view maintenance, deletion propagation and causal responsibility. A long-open question is determining the conjunctive queries (CQs) for which resilience can be solved in PTIME. We shed new light on this problem by proposing a unified Integer Linear Programming (ILP) formulation.” Find the paper and authors list in the ACM on Management of Data conference proceedings.