Title
Topic
-
‘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.
-
‘Zero-Shot Referring Expression Comprehension via Structural Similarity Between Images and Captions’
“Zero-shot referring expression comprehension aims at localizing bounding boxes in an image corresponding to provided textual prompts, which requires: (i) a fine-grained disentanglement of complex visual scene and textual context, and (ii) a capacity to understand relationships among disentangled entities. Unfortunately, existing large vision-language alignment (VLA) models, e.g., CLIP, struggle with both aspects so cannot be directly used for this task. To mitigate this gap, we leverage large foundation models to disentangle both images and texts into triplets in the format of (subject, predicate, object).” Find the paper and full list of authors at ArXiv.
-
‘Through the Looking Glass: The Role of Virtual Mirrors in Shaping Empathy in Virtual Reality Perspective Taking’
“In this study, we explored the effect of seeing one’s avatar in a virtual mirror during a virtual reality (VR) perspective taking experience. Participants were divided into two groups, with one experiencing the VR environment with the presence of a mirror showcasing their avatar and the other without. … However, a notable difference emerged in terms of empathy; participants who viewed their avatars in the mirror exhibited reduced empathic responses. These findings illuminate the nuanced dynamics of self-representation in virtual environments.” Find the paper and list of authors in the proceedings of the 22nd International Conference on Mobile and Ubiquitous…
-
‘Point and Select: Effects of Multimodal Feedback on Text Entry Performance in Virtual Reality’
“The current study examined the effects of visual, auditory, and haptic feedback on VR text entry performance and perceived mental workload across two experiments. In Experiment 1, the feedback was presented as users were pointing from one key to another, dubbed pointing feedback. … In Experiment 2, the feedback was provided when users selected the keys by pressing the trigger on the controller, dubbed selection feedback. … These results indicate that the usability of VR text entry tasks changes as a function of when and how feedback is provided.” Find the paper and authors list in the International Journal of…
-
‘Strata Fee Management in Condominiums via Smart Contracts’
“Condominiums and similar properties use a stratum to manage daily operations, and owners fund it through strata fees. While existing strata fee management systems may be able to handle such funds, such systems could be more inherently transparent. It is possible to leverage the digital ledger from blockchain networks and smart contracts to build a fully transparent strata fee management system. This paper proposes designing a strata fee management system based on a smart contract in the Ethereum network.” Find the paper and full list of authors in the Journal of Theoretical and Applied Electronic Commerce Research.
-
‘Query Efficient Weighted Stochastic Matching’
“In this paper, we study the weighted stochastic matching problem. Let G=(V,E) be a given edge-weighted graph and let its realization G be a random subgraph of G that includes each edge e∈E independently with a known probability pe. The goal in this problem is to pick a sparse subgraph Q of G without prior knowledge of G’s realization, such that the maximum weight matching among the realized edges of Q (i.e. the subgraph Q∩) in expectation approximates the maximum weight matching of the entire realization G.” Find the paper and full list of authors at ArXiv.