bluuebunny/crossref_metadata_2025 huggingface dataset:
Clinical Outcome of Endoscopically Assisted Mini-open Carpal Tunnel Release
Authors: IIJIMA Junichi , TAJIRI Yasuto
Published: October 2024

Background: Carpal tunnel syndrome (CTS) can be treated surgically. Although the minimally invasive open surgical method is widely used, it is not possible to directly visualise the entire length of the carpal tunnel, especially the proximal end, which is on the side away from the skin incision. In this study, we performed a mini-open carpal tunnel release with endoscopic assistance to release the entire length of the carpal tunnel under direct vision and investigated the treatment outcomes.

Methods: The surgical method included an incision of ≤2 cm in the palm, cutting of the transverse carpal ligament under direct vision and cutting of the forearm fascia under endoscopic vision. A uniquely designed sheath was used for the endoscopic resection. We investigated the sex, age, medical history, symptoms, examination findings, anaesthesia method, operation time, thenar motor branch variation, postoperative complications, presence or absence of pillar pain and final examination findings of the target patients.

Results: A total of 100 hands (85 patients) were included. Anatomical variations of the thenar motor branches were observed in 19 hands. At the final follow-up, hand numbness improved in all patients, while mild numbness was observed in 25 hands. The abductor pollicis brevis muscle improved in all patients with paresis, but 8 of the 27 hands remained completely paralysed. Pillar pain was observed in 36 hands at 8 weeks postoperative, but the condition improved in all patients. The clinical outcomes of this study were good with no cases of major complications or reoperation.

Conclusions: The minimally invasive open surgical method described here can be reliably used to release the forearm fascia proximal to the carpal tunnel. The thenar motor branch can also be confirmed under direct visualisation, making it a relatively safe and useful approach.

Level of Evidence: Level Ⅳ (Therapeutic)
Protocol to Develop a Core Outcomes Set for Peripheral Nerve Injury
Authors: DY Christopher J. , HOROWITZ Roy S. , BROGAN David M.
Published: October 2024

Background: Advances in treatment philosophies and microsurgical techniques for peripheral nerve injuries (PNI) have led to improved outcomes. However, lack of standardisation in the evaluation of clinical outcomes after PNI treatment precludes the ability to compare reconstruction methods, such as nerve transfer, nerve grafting, free functioning muscle transfers and tendon transfers. To this end, our goal is to work collaboratively to establish a core outcome set to evaluate outcomes after PNI.

Methods: The protocol for this arc of work, delineated in this manuscript, consists of two phases: (1) conducting a systematic review of how outcomes are currently reported following PNI and (2) a Delphi process to gain consensus on the measures to include in the core outcome set for PNI. In the Delphi process, two online rounds will be used to gather consensus on the importance of each outcome measure. A final round will be conducted in person to discuss and resolve measures for which there is not yet consensus and to finalise the core outcomes set.

Conclusions: Through this process, a common standard for reporting outcomes after PNI will be created, facilitating collaboration and future research.
Special Issue on Conversational Information Seeking
Authors: Lei Wenqiang , Hong Richang , Zamani Hamed , Budzianowski Pawel , Murdock Vanessa , Yilmaz Emine
Published: October 2024

In this article, we provide an overview of ACM TWEB’s Special Issue on Conversational Information Seeking. It highlights both research and practical applications in this field. The article also discusses the future potential of conversational information seeking technology.
VarLifter: Recovering Variables and Types from Bytecode of Solidity Smart Contracts
Authors: Li Yichuan , Song Wei , Huang Jeff
Published: October 2024

Since funds or tokens in smart contracts are maintained through specific state variables, contract audit, an effective means for security assurance, particularly focuses on these variables and their related operations. However, the absence of publicly accessible source code for numerous contracts, with only bytecode exposed, hinders audit efforts. Recovering variables and their types from Solidity bytecode is thus a critical task in smart contract analysis and audit, yet this is a challenging task because the bytecode loses variable and type information, only with low-level data operated by stack manipulations and untyped memory/storage accesses. The state-of-the-art smart contract decompilers miss identifying many variables and incorrectly infer the types for many identified variables. To this end, we propose VarLifter, a lifter dedicated to the precise and efficient recovery of typed variables. VarLifter interprets every read or written field of a data region as at least one potential variable, and after discarding falsely identified variables, it progressively refines the variable types based on the variable behaviors in the form of operation sequences. We evaluate VarLifter on 34,832 real-world Solidity smart contracts. VarLifter attains a precision of 97.48% and a recall of 91.84% for typed variable recovery. Moreover, VarLifter finishes analyzing 77% of smart contracts in around 10 seconds per contract. If VarLifter is used to replace the variable recovery modules of the two state-of-the-art Solidity bytecode decompilers, 52.4%, and 74.6% more typed variables will be correctly recovered, respectively. The applications of VarLifter to contract decompilation, contract audit, and contract bytecode fuzzing illustrate that the recovered variable information improves many contract analysis tasks.
A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code
Authors: Simonnet Julien , Lemerre Matthieu , Sighireanu Mihaela
Published: October 2024

We tackle the problem ofchecking non-proof-carrying code, i.e. automatically proving type-safety (implying in our type system spatial memory safety) of low-level C code or of machine code resulting from its compilation without modification. This requires a precise static analysis that we obtain by having a type system which (i) is expressive enough to encode common low-level idioms, like pointer arithmetic, discriminating variants by bit-stealing on aligned pointers, storing the size and the base address of a buffer in distinct parts of the memory, or records with flexible array members, among others; and (ii) can be embedded in an abstract interpreter. We propose a new type system that meets these criteria. The distinguishing feature of this type system is a nominal organization of contiguous memory regions, which (i) allows nesting, concatenation, union, and sharing parameters between regions; (ii) induces a lattice over sets of addresses from the type definitions; and (iii) permits updates to memory cells that change their type without requiring one to control aliasing. We provide a semantic model for our type system, which enables us to derive sound type checking rules by abstract interpretation, then to integrate these rules as an abstract domain in a standard flow-sensitive static analysis. Our experiments on various challenging benchmarks show that semantic type-checking using this expressive type system generally succeeds in proving type safety and spatial memory safety of C and machine code programs without modification, using only user-provided function prototypes.
Sensitivity by Parametricity
Authors: Lobo-Vesga Elisabet , Russo Alejandro , Gaboardi Marco , Cortiñas Carlos Tomé
Published: October 2024

The work of Fuzz has pioneered the use of functional programming languages where types allow reasoning about the sensitivity of programs. Fuzz and subsequent work (e.g., DFuzz and Duet) use advanced technical devices like linear types, modal types, and partial evaluation. These features usually require the design of a new programming language from scratch—a significant task on its own! While these features are part of the classical toolbox of programming languages, they are often unfamiliar to non-experts in this field. Fortunately, recent studies (e.g., Solo) have shown that linear and complex types in general, are not strictly needed for the task of determining programs’ sensitivity since this can be achieved by annotating base types with static sensitivity information. In this work, we take a different approach. We propose to enrich base types with information about the metric relation between values, and we present the novel idea of applying
parametricity
to derive direct proofs for the sensitivity of functions. A direct consequence of our result is that
calculating and proving
the sensitivity of functions is reduced to simply type-checking in a programming language with support for polymorphism and type-level naturals. We formalize our main result in a calculus, prove its soundness, and implement a software library in the programming language Haskell–where we reason about the sensitivity of canonical examples. We show that the simplicity of our approach allows us to exploit the type inference of the host language to support a limited form of sensitivity inference. Furthermore, we extend the language with a privacy monad to showcase how our library can be used in practical scenarios such as the implementation of differentially private programs, where the privacy guarantees depend on the sensitivity of user-defined functions. Our library, called Spar, is implemented in less than 500 lines of code.
FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions
Authors: Lin Zhengyao , Gancher Joshua , Parno Bryan
Published: October 2024

Coarse-grained reconfigurable arrays (CGRAs) have gained attention in recent years due to their

promising power efficiency compared to traditional von Neumann architectures.

To program these architectures using ordinary languages such as C,

a dataflow compiler must transform the original sequential, imperative program

into an equivalent dataflow graph, composed of dataflow operators running

in parallel.

This transformation is challenging since the asynchronous nature of dataflow

graphs allows out-of-order execution of operators, leading to behaviors not present in the original imperative programs.

We address this challenge by developing a translation validation technique for dataflow compilers

to ensure that the dataflow program has the same behavior as the original imperative program

on all possible inputs and schedules of execution.

We apply this method to a state-of-the-art dataflow compiler targeting the RipTide CGRA architecture.

Our tool uncovers 8 compiler bugs where the compiler outputs incorrect dataflow

graphs, including a data race that is otherwise hard to discover via testing.

After repairing these bugs, our tool verifies the correct compilation of all programs in the RipTide benchmark suite.
Crabtree: Rust API Test Synthesis Guided by Coverage and Type
Authors: Takashima Yoshiki , Cho Chanhee , Martins Ruben , Jia Limin , Păsăreanu Corina S.
Published: October 2024

Rust type system constrains pointer operations, preventing bugs such as use-after-free. However, these constraints may be too strict for programming tasks such as implementing cyclic data structures. For such tasks, programmers can temporarily suspend checks using the unsafe keyword. Rust libraries wrap unsafe code blocks and expose higher-level APIs. They need to be extensively tested to uncover memory-safety bugs that can only be triggered by unexpected API call sequences or inputs. While prior works have attempted to automatically test Rust library APIs, they fail to test APIs with common Rust features, such as polymorphism, traits, and higher-order functions, or they have scalability issues and can only generate tests for a small number of combined APIs. We propose Crabtree, a testing tool for Rust library APIs that can automatically synthesize test cases with native support for Rust traits and higher-order functions. Our tool improves upon the test synthesis algorithms of prior works by combining synthesis and fuzzing through a coverage- and type-guided search algorithm that intelligently grows test programs and input corpus towards testing more code. To the best of our knowledge, our tool is the first to generate well-typed tests for libraries that make use of higher-order trait functions. Evaluation of Crabtree on 30 libraries found four previously unreported memory-safety bugs, all of which were accepted by the respective authors.
Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types
Authors: Boruch-Gruszecki Aleksander , Ghosn Adrien , Payer Mathias , Pit-Claudel Clément
Published: October 2024

Modern software needs fine-grained compartmentalization, i.e., intra-process isolation. A particularly important reason for it are supply-chain attacks, the need for which is aggravated by modern applications depending on hundreds or even thousands of libraries. Object capabilities are a particularly salient approach to compartmentalization, but they require the entire program to assume a lack of ambient authority. Most of existing code was written under no such assumption; effectively, existing applications need to undergo a rewrite-the-world migration to reap the advantages of ocap. We propose
gradual compartmentalization
, an approach which allows gradually migrating an application to object capabilities, component by component in arbitrary order, all the while continuously enjoying security guarantees. The approach relies on runtime authority enforcement and tracking the authority of objects the type system. We present Gradient, a proof-of-concept gradual compartmentalization extension to Scala which uses Enclosures and Capture Tracking as its key components. We evaluate our proposal by migrating the standard XML library of Scala to Gradient.
PolyJuice: Detecting Mis-compilation Bugs in Tensor Compilers with Equality Saturation Based Rewriting
Authors: Zhou Chijin , Qian Bingzhou , Go Gwihwan , Zhang Quan , Li Shanshan , Jiang Yu
Published: October 2024

Tensor compilers are essential for deploying deep learning applications across various hardware platforms. While powerful, they are inherently complex and present significant challenges in ensuring correctness. This paper introduces PolyJuice, an automatic detection tool for identifying mis-compilation bugs in tensor compilers. Its basic idea is to construct semantically-equivalent computation graphs to validate the correctness of tensor compilers. The main challenge is to construct equivalent graphs capable of efficiently exploring the diverse optimization logic during compilation. We approach it from two dimensions. First, we propose arithmetic and structural equivalent rewrite rules to modify the dataflow of a tensor program. Second, we design an efficient equality saturation based rewriting framework to identify the most simplified and the most complex equivalent computation graphs for an input graph. After that, the outcome computation graphs have different dataflow and will likely experience different optimization processes during compilation. We applied it to five well-tested industrial tensor compilers, namely PyTorch Inductor, OnnxRuntime, TVM, TensorRT, and XLA, as well as two well-maintained academic tensor compilers, EinNet and Hidet. In total, PolyJuice detected 84 non-crash mis-compilation bugs, out of which 49 were confirmed with 20 fixed.
Weighted Context-Free-Language Ordered Binary Decision Diagrams
Authors: Sistla Meghana , Chaudhuri Swarat , Reps Thomas
Published: October 2024

This paper presents a new data structure, called
Weighted Context-Free-Language Ordered BDDs
(WCFLOBDDs), which are a hierarchically structured decision diagram, akin to Weighted BDDs (WBDDs) enhanced with a procedure-call mechanism. For some functions, WCFLOBDDs are exponentially more succinct than WBDDs. They are potentially beneficial for representing functions of type B

n

→
D
, when a function’s image
V
⊆
D
has many different values. We apply WCFLOBDDs in quantum-circuit simulation, and find that they perform better than WBDDs on certain benchmarks. With a 15-minute timeout, the number of qubits that can be handled by WCFLOBDDs is 1-64× that of WBDDs(and 1-128× that of CFLOBDDs, which are an unweighted version of WCFLOBDDs). These results support the conclusion that for this application—from the standpoint of problem size, measured as the number of qubits—WCFLOBDDs provide the best of both worlds: performance roughly matches whichever of WBDDs and CFLOBDDs is better.(From the standpoint of running time, the results are more nuanced.)
FPCC: Detecting Floating-Point Errors via Chain Conditions
Authors: Yi Xin , Yu Hengbiao , Chen Liqian , Mao Xiaoguang , Wang Ji
Published: October 2024

Floating-point arithmetic is notorious for its rounding errors, which can propagate and accumulate, leading to unacceptable results. Detecting inputs that can trigger significant floating-point errors is crucial for enhancing the reliability of numerical programs. Existing methods for generating error-triggering inputs often rely on costly shadow executions that involve high-precision computations or suffer from false positives. This paper introduces chain conditions to capture the propagation and accumulation of floating-point errors, using them to guide the search for error-triggering inputs. We have implemented a tool named FPCC and evaluated it on 88 functions from the GNU Scientific Library, as well as 21 functions with multiple inputs from previous research. The experimental results demonstrate the effectiveness and efficiency of our approach: (1) FPCC achieves 100% accuracy in detecting significant errors for the reported rank-1 inputs, while 72.69% rank-1 inputs from the state-of-the-art tool ATOMU can trigger significant errors. Overall, 99.64% (1049/1053) of the inputs reported by FPCC can trigger significant errors, whereas only 19.45% (141/723) of the inputs reported by ATOMU can trigger significant errors; (2) FPCC exhibits a 2.17x speedup over ATOMU in detecting significant errors; (3) FPCC also excels in supporting functions with multiple inputs, outperforming the state-of-the-art technique. To facilitate further research in the community, we have made FPCC available on GitHub at https://github.com/DataReportRe/FPCC.
Minotaur: A SIMD-Oriented Synthesizing Superoptimizer
Authors: Liu Zhengyang , Mada Stefan , Regehr John
Published: October 2024

A superoptimizing compiler—-one that performs a meaningful search of the program space as part of the optimization process—-can find optimization opportunities that are missed by even the best existing optimizing compilers. We created Minotaur: a superoptimizer for LLVM that uses program synthesis to improve its code generation, focusing on integer and floating-point SIMD code. On an Intel Cascade Lake processor, Minotaur achieves an average speedup of 7.3% on the GNU Multiple Precision library (GMP)’s benchmark suite, with a maximum speedup of 13%. On SPEC CPU 2017, our superoptimizer produces an average speedup of 1.5%, with a maximum speedup of 4.5% for 638.imagick. Every optimization produced by Minotaur has been formally verified, and several optimizations that it has discovered have been implemented in LLVM as a result of our work.
A Typed Multi-level Datalog IR and Its Compiler Framework
Authors: Klopp David , Erdweg Sebastian , Pacak André
Published: October 2024

The resurgence of Datalog in the last two decades has led to a multitude of new Datalog systems.

These systems explore novel ideas for improving Datalog's programmability and performance, making important contributions to the field.

Unfortunately, the individual systems progress at a much slower pace than the overall field, because improvements in one system are rarely ported to other systems.

The reason for this rift is that each system provides its own Datalog dialect with specific notation, language features, and invariants, enabling specific optimization and execution strategies.

This paper presents the first compiler framework for Datalog that can be used to support any Datalog frontend language and to target any Datalog backend.

The centerpiece of our framework is a novel typed multi-level Datalog IR that supports IR extensions and guarantees executability.

Existing Datalog systems can provide a compiler frontend that translates their Datalog dialect to the extended IR.

The IR is then progressively lowered toward core Datalog, allowing optimizations at each level.

At last, compiler backends can target different Datalog solvers.

We have implemented the compiler framework and integrated 4 Datalog frontends and 3 Datalog backends, using 16 IR extensions.

We also formalize the IR's flexible type system, which is bidirectional, flow-sensitive, bipolar, and uses three-valued typing contexts.

The type system simultaneously validates type compatibility and precisely tracks bindings of logic variables while permitting IR extensions.
Lexical Effect Handlers, Directly
Authors: Ma Cong , Ge Zhaoyi , Lee Edward , Zhang Yizhou
Published: October 2024

Lexically scoping effect handlers is a language-design idea that equips algebraic effects with a modular semantics: it enables local-reasoning principles without giving up on the control-flow expressiveness that makes effect handlers powerful. However, we observe that existing implementations risk incurring costs akin to the run-time search for dynamically scoped handlers. This paper presents a compilation strategy for lexical effect handlers, adhering to the lexical scoping principle and targeting a language with low-level control over stack layout. Key aspects of this approach are formalized and proven correct. We embody the ideas in a language called Lexa: the Lexa compiler translates high-level effect handling to low-level stack switching. We evaluate the Lexa compiler on a set of benchmarks; the results suggest that it generates efficient code, reducing running-time complexity from quadratic to linear in some cases.
Drowzee: Metamorphic Testing for Fact-Conflicting Hallucination Detection in Large Language Models
Authors: Li Ningke , Li Yuekang , Liu Yi , Shi Ling , Wang Kailong , Wang Haoyu
Published: October 2024

Large language models (LLMs) have revolutionized language processing, but face critical challenges with security, privacy, and generating hallucinations — coherent but factually inaccurate outputs. A major issue is fact-conflicting hallucination (FCH), where LLMs produce content contradicting ground truth facts. Addressing FCH is difficult due to two key challenges:
1)
Automatically constructing and updating benchmark datasets is hard, as existing methods rely on manually curated static benchmarks that cannot cover the broad, evolving spectrum of FCH cases.
2)
Validating the reasoning behind LLM outputs is inherently difficult, especially for complex logical relations. To tackle these challenges, we introduce a novel logic-programming-aided metamorphic testing technique for FCH detection. We develop an extensive and extensible framework that constructs a comprehensive factual knowledge base by crawling sources like Wikipedia, seamlessly integrated into Drowzee. Using logical reasoning rules, we transform and augment this knowledge into a large set of test cases with ground truth answers. We test LLMs on these cases through template-based prompts, requiring them to provide reasoned answers. To validate their reasoning, we propose two semantic-aware oracles that assess the similarity between the semantic structures of the LLM answers and ground truth. Our approach automatically generates useful test cases and identifies hallucinations across six LLMs within nine domains, with hallucination rates ranging from 24.7% to 59.8%. Key findings include LLMs struggling with temporal concepts, out-of-distribution knowledge, and lack of logical reasoning capabilities. The results show that logic-based test cases generated by Drowzee effectively trigger and detect hallucinations. To further mitigate the identified FCHs, we explored model editing techniques, which proved effective on a small scale (with edits to fewer than 1000 knowledge pieces). Our findings emphasize the need for continued community efforts to detect and mitigate model hallucinations.
Model Checking Distributed Protocols in Must
Authors: Enea Constantin , Giannakopoulou Dimitra , Kokologiannakis Michalis , Majumdar Rupak
Published: October 2024

We describe the design and implementation of Must, a framework for

modeling and automatically verifying distributed systems. Must

provides a concurrency API that supports multiple communication

models, on top of a mainstream programming language, such as Rust.

Given a program using this API, Must verifies it by means of a

novel, optimal dynamic partial order reduction algorithm that

maintains completeness and optimality for all communication models

supported by the API.

We use Must to design and verify models of distributed systems in

an industrial context. We demonstrate the usability of Must's API

by modeling high-level system idioms (e.g., timeouts, leader

election, versioning) as abstractions over the core API, and

demonstrate Must's scalability by verifying systems employed in

production (e.g., replicated logs, distributed transaction management

protocols), the verification of which lies beyond the capacity of

previous model checkers.
QuAC: Quick Attribute-Centric Type Inference for Python
Authors: Wu Jifeng , Lemieux Caroline
Published: October 2024

Python’s dynamic typing facilitates rapid prototyping and underlies its popularity in many domains. However, dynamic typing reduces the power of many static checking and bug-finding tools. Python type annotations can make these tools more useful. Type inference tools aim to reduce developers’ burden of adding them. However, existing type inference tools struggle to support dynamic features, infer correct types (especially container type parameters and non-builtin types), and run in reasonable time. Inspired by Python’s duck typing, where the attributes accessed on Python expressions characterize their implicit interfaces, we propose QuAC (Quick Attribute-Centric Type Inference for Python). At its core, QuAC collects attribute sets for Python expressions and leverages information retrieval techniques to predict classes from these attribute sets. It also recursively predicts container type parameters. We evaluate QuAC’s performance on popular Python projects. Compared to state-of-the-art non-LLM baselines, QuAC predicts types with high accuracy complementary to those predicted by the baselines while not sacrificing coverage. It also demonstrates clear advantages in predicting container type parameters and non-builtin types and reduces run times. Furthermore, QuAC is nearly two orders of magnitude faster than an LLM-based method while covering nearly half of its errorless non-trivial type predictions. It is also significantly more consistent at predicting container type parameters and non-builtin types than the LLM-based method, regardless of whether the project has ground-truth type annotations.
Semantic-Type-Guided Bug Finding
Authors: Qian Kelvin , Smith Scott , Stride Brandon , Weng Shiwei , Wu Ke
Published: October 2024

In recent years, there has been an increased interest in tools that establishincorrectnessrather than correctness of program properties. In this work we build on this approach by developing a novel methodology to prove incorrectness ofsemantic typingproperties of functional programs, extending the incorrectness approach to the model theory of functional program typing. We define a semantic type refuter which refutes semantic typings for a simple functional language. We prove our refuter is co-recursively enumerable, and that it is sound and complete with respect to a semantic typing notion. An initial implementation is described which uses symbolic evaluation to efficiently find type errors over a functional language with a rich type system.
Unifying Static and Dynamic Intermediate Languages for Accelerator Generators
Authors: Kim Caleb , Li Pai , Mohan Anshuman , Butt Andrew , Sampson Adrian , Nigam Rachit
Published: October 2024

Compilers for accelerator design languages (ADLs) translate high-level languages into application-specific hardware. ADL compilers rely on a hardware
control interface
to compose hardware units. There are two choices:
static
control, which relies on cycle-level timing; or
dynamic
control, which uses explicit signalling to avoid depending on timing details. Static control is efficient but brittle; dynamic control incurs hardware costs to support compositional reasoning. Piezo is an ADL compiler that unifies static and dynamic control in a single intermediate language (IL). Its key insight is that the IL’s static fragment is a
refinement
of its dynamic fragment: static code admits a subset of the run-time behaviors of the dynamic equivalent. Piezo can optimize code by combining facts from static and dynamic submodules, and it opportunistically converts code from dynamic to static control styles. We implement Piezo as an extension to an existing dynamic ADL compiler, Calyx. We use Piezo to implement a frontend for an existing ADL, a systolic array generator, and a packet-scheduling hardware generator to demonstrate its optimizations and the static–dynamic interactions it enables.
Validating SMT Solvers for Correctness and Performance via Grammar-Based Enumeration
Authors: Winterer Dominik , Su Zhendong
Published: October 2024

We introduce ET, a grammar-based enumerator for validating SMT solver correctness and performance. By compiling grammars of the SMT theories to algebraic datatypes, ET leverages the functional enumerator FEAT. ET is highly effective at bug finding and has many complimentary benefits. Despite the extensive and continuous testing of the state-of-the-art SMT solvers Z3 and cvc5, ET found 102 bugs, out of which 76 were confirmed and 32 were fixed. Moreover, ET can be used to understand the evolution of solvers. We derive eight grammars realizing all major SMT theories including the booleans, integers, reals, realints, bit-vectors, arrays, floating points, and strings. Using ET, we test all consecutive releases of the SMT solvers Z3 and CVC4/cvc5 from the last six years (61 versions) on 8 million formulas, and 488 million solver calls. Our results suggest improved correctness in recent versions of both solvers but decreased performance in newer releases of Z3 on small timeouts (since z3-4.8.11) and regressions in early cvc5 releases on larger timeouts. Due to its systematic testing and efficiency, we further advocate ET's use for continuous integration.
SIGecom Winter Meeting 2023 Highlights
Authors: Ryu Emily , Zhou Chenghan , Bahrani Maryam
Published: October 2024

The third annual ACM SIGecom Winter Meeting took place on February 22, 2023. Organized by Scott Kominers and Matt Weinberg, this year's meeting brought together researchers from economics, computer science, and adjacent fields to focus on Web3, blockchains, and cryptocurrencies. The virtual meeting included talks from and discussions with leading experts on getting into the research space, interesting technical questions, and exciting challenges and opportunities that lie ahead. The day also included interactive exercises that gave participants the opportunity to gain hands-on experience and have fun with NFTs.
Report on the 2nd ACM Conference on Equity and Access in Algorithms, Mechanisms, and Optimization (EAAMO 2022)
Authors: Falcettoni Elena , Machuve Dina , Wilder Bryan , Zhou Angela
Published: October 2024

The second annual ACM Conference on Equity and Access in Algorithms, Mechanisms, and Optimization (EAAMO'22) was held from October 6-9 at George Mason University in Arlington, VA, USA. This was the first in-person version of the conference: the first event was held virtually in 2021. The conference builds on a line of workshops on Mechanism Design for Social Good (MD4SG) held previously at the ACM Conference on Economics and Computation, and is affiliated with the broader MD4SG initiative. In both 2022 and 2021, SIGecom was a sponsor of the conference. EAAMO aims to highlight work where techniques from algorithms, optimization, and mechanism design, along with insights from the social sciences and humanistic studies, can help improve equity and access to opportunity for historically disadvantaged and underserved communities. A key goal of the conference is to bridge research and practice in this area. Accordingly, we aimed to foster an interdisciplinary community, including researchers from a computer science, operations research, economics, policy, and more, as well as practitioners and policymakers working in areas related to inequality. The conference featured contributed papers and posters as well invited keynote talks, a panel discussion, a doctoral consortium, and community-building activities and social events.
Mechanism Design with Predictions: An Annotated Reading List
Authors: Balkanski Eric , Gkatzelis Vasilis , Tan Xizhi
Published: October 2024

A surge of recent work has focused on analyzing the performance of algorithms guided by predictions, aiming to enhance their worst-case performance guarantees with improved guarantees when the predictions are accurate. This "learning-augmented" framework was recently also extended to mechanism design settings involving strategic agents and we provide an overview of these results.
Leveraging Reviews: Learning to Price with Buyer and Seller Uncertainty
Authors: Guo Wenshuo , Haghtalab Nika , Kandasamy Kirthevasan , Vitercik Ellen
Published: October 2024

Customers can access hundreds of reviews for a single product in online marketplaces. Buyers often use reviews from other customers that share their type---such as height for clothing or skin type for skincare products---to estimate their values, which they may not know a priori. Customers with few relevant reviews may hesitate to purchase except at a low price, so for the seller, there is a tension between setting high prices and ensuring that there are enough reviews so buyers can confidently estimate their values. Simultaneously, sellers may use reviews to gauge the demand for items they wish to sell. In this work, we study this pricing problem in an online setting where the seller interacts with a set of buyers of finitely many types, one by one, over a series of
T
rounds. At each round, the seller first sets a price. Then, a buyer arrives and examines the reviews of the previous buyers with the same type, which reveal those buyers' ex-post values. Based on the reviews, the buyer decides to purchase if they have good reason to believe their ex-ante utility is positive. Crucially, the seller does not know the buyer's type when setting the price, nor even the distribution over types. We provide a no-regret algorithm that the seller can use to obtain high revenue. When there are
d
types, after
T
rounds, our algorithm achieves a problem-independent
Õ
(
T
2/3
d
1/3
) regret bound. However, when the smallest probability
q
min
that any given type appears is large, specifically when
q
min
∈ Ω(
d
−2/3
T
−1/3
), the same algorithm achieves a [EQUATION] regret bound. We complement these upper bounds with matching lower bounds in both regimes, showing that our algorithm is minimax optimal up to lower-order terms.

This is a summary of work that won the
Exemplary AI Track Paper Award
at EC'24.
Assortment Optimization: An Annotated Reading Assortment
Authors: Ma Will
Published: October 2024

Which varieties or brands of a product should a retailer stock on its shelf? Carrying a large variety caters to more customers' needs, but could cannibalize the sales of high-end brands and also cause an inventory nightmare. Assortment optimization aims to formalize these tradeoffs, with the basic problem being as follows. There is a universe of brands
j
∈
U
, each with a market-accepted price

r
j
.

For any
S
⊆
U
, a function
ϕ
(
j, S
) indicates the probability that a representative customer from the population would purchase
j
when given the choice from
assortment S
, under the market prices. The optimization problem is to maximize the average revenue per customer, i.e.

[EQUATION] (1)

possibly with constraints on
S
due to shelf size. Assortment optimization started out by showing how to efficiently find the optimal
S
from the exponentially many possibilities, under well-established parametric forms for the function
ϕ
that are called (
discrete) choice models.
Since then, the literature has developed choice models of its own that are specialized for assortment optimization. The basic problem has also been extended, and connected with topics such as online algorithms, machine learning, and mechanism design that are mainstream in the Economics and Computation community, with a vast horizon for future directions.

This is an annotated reading list about assortment optimization, that aims to provide broad coverage while facing a "cardinality constraint" on the number of papers in the assortment.
Recent Trends in Information Elicitation
Authors: Frongillo Rafael , Waggoner Bo
Published: October 2024

This note provides a survey for the Economics and Computation community of some recent trends in the field of information elicitation. At its core, the field concerns the design of incentives for strategic agents to provide accurate and truthful information. Such incentives are formalized as
proper scoring rules
, and turn out to be the same object as
loss functions
in machine-learning settings, providing many connections. More broadly, the field concerns the design of mechanisms to obtain information from groups of agents and aggregate it or use it for decision making. Recently, work on information elicitation has expanded and been connected to online no-regret learning, mechanism design, fair division, and more.
VeriFog: A Generic Model-based Approach for Verifying Fog Systems at Design Time and Generating Deployment Configurations
Authors: Awad Hiba , Alidra Abdelghani , Bruneliere Hugo , Ledoux Thomas , Rivalan Jonathan
Published: October 2024

Fog Computing is a paradigm decentralizing the Cloud by geographically distributing computation, storage, network resources and related services. It provides benefits such as reducing the number of bottlenecks, limiting unwanted data movements, etc. However, managing the size, complexity and heterogeneity of the Fog systems to be engineered is challenging and can quickly become costly. According to best practices in software engineering, verification tasks could be performed on a system design prior to its implementation and deployment. We propose a generic model-based approach for verifying Fog systems at design time, also enabling the automatic generation of corresponding deployment configuration files. Named VeriFog, this approach is notably based on a customizable Fog Modeling Language (FML). We experimented in practice by modeling three use cases, from three different application domains, and by considering three main types of non-functional properties to be verified. From this modeling and verification effort, we show that we are able to automatically generate usable deployment configuration files for different deployment tools. In direct collaboration with our industrial partner Smile, the approach and underlying language presented in this paper are necessary steps towards a more global model-based support for the complete life cycle of Fog systems.
Students Report from ACM Multimedia 2022
Authors: Yamakata Yoko
Published: October 2024

ACM Multimedia 2022 was held in a hybrid format in Lisbon, Portugal from October 10-14, 2022.

This was the first local participation in three years for many participants, as the strict travel restrictions associated with Covid-19 in 2020 and 2021 made it difficult to participate locally by travelling out of the host and neighbouring countries.

In Portugal, the Covid-19 restrictions were almost lifted, and the city was bustling with tourists. Participants were careful to avoid infectious diseases and enjoyed Lisbon's local wine "Vinho Verde" and cod dishes with their colleagues and engaged in lively discussions about multimedia research.

For many students, this was their first time presenting at an international conference, and it was a wonderful experience.

To encourage student authors to participate on-site, SIGMM has sponsored a group of students with Student Travel Grant Awards. Students who wanted to apply for this travel grant needed to submit an online form before the submission deadline. The selected students received either 1,000 or 2,000 USD to cover their airline tickets as well as accommodation costs for this event. Of the recipients, 25 were able to attend the conference. We asked them to share their unique experience attending ACM Multimedia 2022. In this article, we share their reports of the event.
JPEG Column: 97th JPEG Meeting
Authors: Pinheiro Antonio
Published: October 2024

The 97th JPEG meeting was held online from 24 to 28 October 2022. JPEG received responses to the Call for Proposals (CfP) on JPEG Fake Media, the first multimedia international standard designed to facilitate the secure and reliable annotation of media assets creation and modifications. In total six responses were received addressing different requirements in the scope of this standardization initiative. Moreover, relevant advances were made on the standardization of learning-based coding, notably the learning-based coding of images, JPEG AI, and JPEG Pleno point cloud coding. Furthermore, the explorations on quality assessment of images, JPEG AIC, and of JPEG Pleno light field had relevant advances with the definition of their Calls for Contributions and Common Test Conditions.
Koli Calling 2024: Call for Participation
Authors: Leinonen Juho
Published: October 2024

We warmly invite you to attend the 24th Koli Calling International Conference on Computing Education Research (Koli Calling 2024), to be held 14-17 November 2024 in the beautiful Koli National Forest in Eastern Finland. While the submission deadline for full papers and discussion papers has passed, you can still submit posters and demo papers by 20 September 2024.
SIGCSE Technical Symposium 2025: Call for Submissions
Authors: Shoop Libby , Rebelsky Samuel , Prather James
Published: October 2024

The SIGCSE Technical Symposium (SIGCSETS) is a forum for educators and researchers to share new results and insights around developing, implementing, or evaluating computing programs, pedagogy, curricula, and courses. The conference will be held in Pittsburgh, Pennsylvania from February 25 to March 1, 2025, mostly in-person with a few limited online participation opportunities available to accommodate a broader range of attendees. Details are available at the conference website: https://sigcse2025.sigcse.org.
The QIBA Profile for Diffusion-Weighted MRI: Apparent Diffusion Coefficient as a Quantitative Imaging Biomarker
Authors: Boss Michael A. , Malyarenko Dariya , Partridge Savannah , Obuchowski Nancy , Shukla-Dave Amita , Winfield Jessica M. , Fuller Clifton D. , Miller Kevin , Mishra Virendra , Ohliger Michael , Wilmes Lisa J. , Attariwala Raj , Andrews Trevor , deSouza Nandita M. , Margolis Daniel J. , Chenevert Thomas L.
Published: October 2024

The claims and procedures of the Quantitative Imaging Biomarker Alliance Diffusion-Weighted Imaging Biomarker Committee are summarized for apparent diffusion coefficient as a quantitative biomarker to monitor lesions in the brain, liver, prostate, and breast.
Microporous Substrate Effect on SECM Steady State Current- A 3D Modeling Study Critical to Battery Electrode Performance
Authors: Raju Anjana Raj , Krueger Bastian , Schougaard Steen B.
Published: October 2024

Scanning electrochemical microscopy (SECM) enables the study of mass transport in porous substrates with microscale spatial resolution, which is profoundly influenced by the substrate’s architecture. Here, a 3D SECM modeling was used to compare the impact of substrate geometry on transport in three porous structures: a superposition (SP) and two high fidelity (HF-1 and HF-2) models. It was found that the steady-state current decreases with an increase in the geometric complexity from SP to HF-1 to HF-2, indicating the presence of more tortuous paths in HF-2. Despite having the same porosity and thickness values, the disparity between the SP and the two HF substrates shows the effect of microporous geometry. Our findings also demonstrated the deviation of all three substrates from Bruggeman’s predictions, which highlights the significance of modeling to rationalize the transport properties in commercial battery electrodes.
Lithiophilic Protective Dual Layer Enabling Stable Electrodeposition of Lithium at High Current Density
Authors: Choi Hee-Joo , Kim Ji-Wan , Bae Hongyeul , Kim Jinhong , Kim Dong-Won
Published: October 2024

Lithium (Li) is an ideal anode material for rechargeable batteries and thus manufacturing Li metal is crucial for the practical development of Li metal batteries. Electrodeposition is an efficient technique for producing ultrathin and scalable Li metal electrodes. However, the dendritic growth and the side reactions of Li with electrolyte during the electrodeposition are the main obstacles to overcome. In this study, we designed a pre-coated protective dual layer (PDL) composed of a poly(ethylene oxide)-based solid polymer electrolyte (SPE) and a polydopamine-coated cellulose membrane (PD-CM). The adhesive and ion-conductive SPE layer suppressed the growth of Li dendrites and side reactions with liquid electrolyte. The PD-CM layer with high porosity and lithiophilicity promoted a facile and uniform Li-ion flux. By applying the pre-coated PDL, Li was uniformly electrodeposited on the Ag-coated Cu at a high current density of 6 mA cm−2. The Li/LiFePO4 cell composed of an electrodeposited Li anode with PDL and a LiFePO4 cathode was assembled without an additional separator, and its cycling performance was evaluated. The cell initially delivered a high discharge capacity of 154.8 mAh g−1 at 45 °C and exhibited excellent cycling stability with a capacity retention of 97.0% after 200 cycles.
The Influence of Different Terrains on the Wind Pressure Distribution of Glass Curtain Wall in Airport Terminals in Mountainous Areas
Authors: Pei Cheng , Zhang Xiaomin , Cheng Xiaokang , Yang Xiongwei , Ma Cunming
Published: October 2024

Aiming the issue of wind pressure distribution characteristics of airport terminal glass curtain walls in mountainous areas, wind tunnel tests have been conducted to investigate glass curtain walls in airport terminals under different terrains (at mountain heights of 0, 30, 60, 90 m [H1, H2, H3, H4] and under surrounding high mountains of 80, 130, 150 m [H5, H6, H7]). Based on experimental data, a comparative analysis was conducted on the effects of different terrains on the mean and pulsating wind pressures, non‐Gaussian characteristics, peak factor, and extreme wind pressure. The results show that the larger values of the mean and pulsating wind pressures under different terrains appear at the corners of the curtain wall edges. Furthermore, the skewness, kurtosis, and wind pressure probability density function values at the corners of the curtain wall edges significantly deviate from the standard Gaussian distribution, exhibiting significant non‐Gaussian characteristics. The majority values of peak factors range from 3.5 to 5.0, far higher than the recommended value of 2.5 in Chinese specification and code (GB 50009‐2012). Moreover, the values of extreme wind pressure under terrains H1, H2, H3, and H4 were greater than that under terrains H5, H6, and H7. At mountain heights H1, H2, H3, and H4, the increasing mountaintop height has a certain increasing effect on the extreme wind pressure. The maximum increase of 96.5% and 82.8% in mountain height H3 and H4 compared to H1. However, the increase in the height of surrounding mountains has a reducing effect on the extreme wind pressure. Research can provide useful suggestions and references for the design, construction, and site selection of terminals in similar airports.