• 在智能家居中实现协作式异常检测：收集用户需求与安全场景分析

  摘要智能家居技术正变得越来越普及，它们自动化了照明、供暖、安全以及其他重要的家庭功能，从而提高了居住者的舒适度、效率和生活便利性。然而，这些系统日益增加的复杂性和互联性使它们面临高级网络威胁，从而危及居民的隐私和安全。在这项研究中，我们探讨了未来智能家居环境的设计，以支持协作式异常检测，使居住者和设备能够共同识别和应对新兴威胁。我们采用了混合方法（首先进行问卷调查，参与者40人，随后进行互动焦点小组讨论，参与者36人），深入了解了智能家居设备的配置、用户工作流程以及潜在的安全漏洞。我们的研究结果包括：(i) 现实安全威胁的分类；(ii) 通过具体布局和场景展示了异常如何在日常家庭活动中出现；(

  来源：Proceedings of the ACM on Interactive, Mobile, Wearable and Ubiquitous Technologies

  时间：2025-11-07

• 关于音乐生成模型评估的调研

  近年来，随着机器学习系统架构和训练方法的不断进步，生成系统在音乐领域的应用也取得了显著进展。尽管这些系统在自然语言处理和图像生成领域广受关注，音乐生成系统却往往较少受到媒体聚焦。然而，音乐生成系统的研究和开发仍展现出强劲的发展势头。音乐作为一种复杂且高度抽象的艺术形式，其评估方式与传统领域有所不同，不仅涉及对系统输出的评估，还包括对用户交互体验的考察。本文旨在对音乐生成系统的评估目标、方法和指标进行跨学科的全面回顾，同时探讨当前评估方法的局限性以及未来可能的发展方向。音乐生成系统的评估通常涉及两个主要方面：系统输出的质量评估和用户在使用过程中的体验。对于系统输出的评估，其目标可能包括音乐的审美

  来源：ACM Computing Surveys

  时间：2025-11-07

• 关于持久线性化的规范自动机——勘误表

  在当今计算机系统中，非易失性存储器（NVM）正逐渐成为一种关键的存储技术。NVM不仅具有与传统动态随机存取存储器（DRAM）相当的访问速度，还能够在系统崩溃后保留其存储的内容。这种特性使得NVM在构建并发程序时提供了额外的优势，同时也带来了新的挑战。并发程序需要满足一系列额外的属性，如故障原子性与可恢复性，以确保在系统出现故障时数据的一致性与正确性。特别是对于并发数据结构的设计，如栈、集合、队列等，这些挑战尤为明显，因为它们需要在有限的同步机制下支持并发操作。为了确保在NVM环境下并发数据结构的正确性，研究人员已经对传统的线性化（linearizability）概念进行了扩展，提出了“持久线性

  来源：Formal Aspects of Computing

  时间：2025-11-07

• 关于深度学习在蒙特卡洛路径追踪中的应用的调研

  摘要近期在硬件加速光线追踪方面取得的进展，使得那些原本仅适用于离线渲染的算法（如蒙特卡洛路径追踪）得以实现实时交互。虽然路径追踪在电影行业的场景动画制作中已被证明非常实用，但要获得无视觉噪声的图像通常需要每像素采集数千个样本，并耗费大量计算时间。遗憾的是，这对需要高帧率和分辨率的视频游戏及虚拟现实应用来说是一个挑战，因为这些应用限制了路径追踪的计算开销。目前有两种主要方法可以应对这一难题：过程中采样和后处理重建技术（如去噪和上采样）。深度学习技术的飞速发展为路径追踪处理带来了重大变革。我们基于深度学习对蒙特卡洛路径追踪技术进行了探索与改进，并分析了各种设计方案与技术的优缺点，提出了潜在的未来发

  来源：ACM Computing Surveys

  时间：2025-11-07

• 迈向TPM软件栈的形式化验证：取得的成果与机遇

  在现代计算机系统中，安全性和完整性是至关重要的特性。为了实现这些目标，Trusted Platform Module（TPM）作为一种安全硬件组件被广泛采用。TPM是一种加密处理器，用于保护计算机架构的完整性，并确保存储在其中的加密密钥的安全性。操作系统和应用程序通过一套称为TPM Software Stack（TSS）的API接口与TPM进行交互。在众多TSS的实现中，开源库tpm2-tss因其在安全领域的重要性而受到关注。然而，由于其代码的复杂性，包括大量使用链表和动态内存分配等特性，使得对其的正式验证变得极具挑战性。本文通过一个案例研究，探讨了使用Frama-C验证平台对tpm2-tss

  来源：Formal Aspects of Computing

  时间：2025-11-07

• 人形机器人与人形人工智能：综述、展望与发展方向

  在过去的近一个世纪中，机器人技术经历了飞速发展，而人形机器人作为这一领域的重要分支，早在六十年前便已出现。这些机器人以类人形态为特点，不仅外观类似人类，还具备某些人类的结构特征。然而，尽管当前的人形机器人在外观上越来越接近人类，它们仍然未能真正体现出人类的情感与智能，距离实现与人类相似甚至达到人类水平的智能还有很大差距。随着近年来生成式人工智能（GenAI）和大型语言模型（LLMs）的快速发展，人们对人形机器人的研究兴趣进一步提升，推动了其向实时、互动和多模态方向的演进。这一趋势为人类社会的多个领域带来了巨大的潜力，包括人形工、顾问、教育者、医护人员、护理人员和接待员等。这些应用场景揭示了人形

  来源：ACM Computing Surveys

  时间：2025-11-07

• 在医疗健康领域的机器学习应用设计中面临的公平性挑战

  在当今的医疗领域，人工智能（AI）和机器学习（ML）的应用正在迅速扩展，为决策支持提供了前所未有的机会。然而，这种技术的引入也伴随着一系列复杂的挑战，特别是在确保公平性方面。本文通过分析16位具备医疗科技领域专业知识的工程师和设计师的访谈内容，探讨了在三种医疗场景下如何优先考虑公平性。研究结果表明，医疗科技的公平性不仅涉及技术层面的考量，还与医疗环境、用户视角及利益相关者的互动密切相关。首先，医疗科技的公平性是一个多维度的概念。它不仅关乎模型本身是否在不同群体间表现出一致的性能，还涉及医疗决策过程中的伦理考量。例如，医疗系统中长期存在的偏见可能导致某些群体的健康状况被忽视或误诊，这些偏见可能已

  来源：ACM Transactions on Computing for Healthcare

  时间：2025-11-07

• 面向特征的建模与自适应机器人系统的分析

  在当今高度依赖技术的工业环境中，自主机器人系统（如水下机器人）的可靠性和适应性成为推动创新的关键因素。这些机器人常常被部署在充满不确定性的危险环境，如深海区域，其任务包括水下管道检查、生态监测等。然而，如何在这些复杂环境中确保自主系统的安全性和稳定性，同时提高其适应能力，是一个具有挑战性的问题。本文探讨了使用特征导向方法对自主水下机器人（AUV）进行形式化建模与分析的可能性，以确保其在不确定环境中的行为符合预期，并且能够在不同环境条件下实现可靠的操作。自主机器人系统通常被设计为一个两层架构：管理子系统负责执行具体任务，如导航或管道检查；而管理子系统则负责适应性逻辑，根据环境和内部状态的变化调整

  来源：Formal Aspects of Computing

  时间：2025-11-07

• 多维空间中学习索引的综述

  近年来，随着机器学习（ML）技术的迅速发展，数据库索引结构的构建方式正经历一场深刻的变革。传统的索引结构，如B树和R树，长期以来是数据库查询优化的核心工具，它们通过预定义的算法和数据组织方式确保了查询的准确性和效率。然而，随着数据规模的不断扩大以及查询模式的复杂化，传统索引结构在某些场景下暴露出性能瓶颈和空间占用较大的问题。因此，一种新的研究趋势逐渐兴起，即“学习型索引”（Learned Indexes）。这类索引将数据库索引结构视为机器学习模型，通过训练模型来学习数据的分布规律，从而在查询过程中利用这些模型进行快速定位，显著提升了索引效率，同时降低了存储需求。在这一领域，学习型索引的研究主要

  来源：ACM Computing Surveys

  时间：2025-11-07

• 罗德·伯斯塔尔：悼念

  Rodney Martineau Burstall，一位在计算机科学领域有着深远影响的学者，以其广泛的学术贡献、开放的人格和对科研社区的持续投入而闻名。他的职业生涯跨越了几十年，从早期的运筹学研究到后来在人工智能、编程语言理论和形式化方法等领域的探索，展现了他作为科学家的多面性和前瞻性。Rod不仅在学术上取得了卓越的成就，更在个人风格和研究态度上留下了深刻的印记。他始终相信，科研不仅是一项严谨的学术活动，更是一种充满乐趣和创造力的人类行为。这种信念贯穿于他的研究生涯，也影响了他所指导的众多学生和研究团队。Rod出生于1934年，成长于利物浦的一个普通家庭。他的父亲是一位绘图员，母亲则是一位家庭

  来源：Formal Aspects of Computing

  时间：2025-11-07

• 关于基于机器学习/深度学习的软件工程的可解释性的系统文献综述

  摘要人工智能（AI）算法，特别是在机器学习（ML）和深度学习（DL）领域的显著成就，推动了它们在多个领域的广泛应用，包括软件工程（SE）。然而，由于这些AI驱动的SE模型具有“黑箱”特性，它们在实践中的部署仍然面临诸多挑战。这种不可解释性为它们在关键任务中的应用带来了风险，例如漏洞检测，而在这些任务中，决策的透明度至关重要。本文旨在通过系统地回顾旨在提高SE领域中AI模型可解释性的方法来阐明这一跨学科领域。该回顾涵盖了在最重要的SE和AI会议及期刊上发表的论文，涉及23个不同SE任务的108篇文章。基于三个关键研究问题（RQs），我们的目标是：（1）总结迄今为止XAI技术在SE任务中取得成功的

  来源：ACM Computing Surveys

  时间：2025-11-07

• 基于代理的建模与仿真在车辆路径问题中的应用调查

  摘要近年来，基于代理的建模与仿真（Agent-Based Modeling and Simulation，ABMS）在车辆路径问题（Vehicle Routing Problem，VRP）中的应用受到了越来越多的关注。本文回顾了过去十年中45篇将基于代理的模型（Agent-Based Models，ABMs）应用于VRP的研究论文，总结了推动ABMS在VRP中应用的五个主要目标，并根据连接ABM仿真器与VRP求解器的实现架构将相关模型分为三类。研究表明，ABMS主要因其能够有效表征和模拟VRP的时空特性而被广泛使用。然而，ABMS的其他一些优势在车辆路径计算中尚未得到充分利用。

  来源：ACM Computing Surveys

  时间：2025-11-07

• 使用ATHENA验证CHC可满足性

  在现代软件验证领域，逻辑求解器已成为不可或缺的工具。这些求解器能够自动推理复杂逻辑公式，帮助开发者识别程序中的错误，确保其行为符合预期。然而，随着逻辑求解器功能的增强，其代码库的复杂性也随之增加，导致错误出现的频率显著上升。为了提高验证工具的可靠性，确保其输出结果的正确性，研究者们开始探索更加严谨的验证方法，以增强对求解器结果的信心。本文提出了一种针对受限的Horn子句（CHC）求解器输出结果的两层验证方法。该方法通过结合SMT（可满足性模理论）求解器生成的证明来验证CHC模型的正确性。这种两层验证策略不仅提高了模型验证的准确性，还为验证工具提供了额外的保障。此外，研究者还开发了一个名为ATH

  来源：Formal Aspects of Computing

  时间：2025-11-07

• 利用ByteBack在Java字节码层面对异常行为进行推理

  本文介绍了ByteBack验证工具的新进展，该工具专注于Java程序的异常行为验证，并且能够支持其他JVM语言如Scala和Kotlin。随着现代编程语言中异常机制的广泛应用，对程序的异常行为进行形式化验证成为保障程序正确性的关键步骤。然而，传统上大多数形式化验证工具是基于源代码的，这限制了它们在面对语言更新和新增特性时的适应性。而ByteBack通过分析字节码来处理异常行为，提供了更高的灵活性和稳定性，使其能够适用于不同版本的Java，以及支持其他兼容字节码的JVM语言。在Java中，异常处理是语言设计的一个重要组成部分，它允许程序在遇到不寻常的运行时条件时进行错误处理。然而，由于异常引入了

  来源：Formal Aspects of Computing

  时间：2025-11-07

• iFM 2023 特别系列介绍

  摘要这个特刊源于2023年11月13日至15日在荷兰莱顿举行的第18届国际集成形式方法会议（iFM 2023）。这个特刊源自2023年11月13日至15日在荷兰莱顿举行的第18届国际集成形式方法会议。该会议（集成形式方法，简称）是一项年度活动，旨在探讨结合不同建模和分析方法的形式化研究。在过去的几十年里，我们见证了多种集成建模、验证和仿真技术的方法的蓬勃发展，这些方法使得对软件密集型系统的分析更加多样化和高效。这些方法为分析系统的不同功能和非功能属性、不同性质组件之间的复杂交互以及系统行为的各个方面提供了强大的支持。iFM会议系列是一个讨论集成形式化建模和分析方法最新研究成果的论坛。会议涵盖了

  来源：Formal Aspects of Computing

  时间：2025-11-07

• 中间环节的类加载器：让Android静态分析工具感到困惑

  在移动应用开发和安全分析领域，Android系统中的类加载机制是一个复杂且关键的环节。开发者和系统提供的类在运行时被加载，而这种动态过程为潜在的安全威胁提供了可能的切入点。本文深入探讨了Android类加载过程中可能发生的“阴影攻击”（shadow attacks），并分析了这些攻击对静态分析工具的影响，以及它们在实际应用中的使用情况。Android的类加载系统由Android运行时（ART）负责，它在应用运行时动态地加载所需的类。在开发阶段，Android Studio会将应用代码与Android SDK类进行链接，这些SDK类通常被包含在`android.jar`中，而在运行时，它们会从其

  来源：Digital Threats: Research and Practice

  时间：2025-11-07

• 混合现实游戏的自适应交互范式

  摘要本文介绍了一种适用于混合现实（MR）游戏的自适应交互范式，旨在提升大规模MR环境中的可访问性、可扩展性和响应性。通过利用深度感应技术和实时3D骨骼追踪技术，该范式使虚拟元素能够动态响应用户动作，从而实现个性化且包容性的交互体验。与传统固定交互模型不同，这种方法根据每个用户的实际情况调整交互区域和手势识别阈值，解决了现有MR设计在应对不同身体能力用户时的局限性。所提出的方法采用以用户为中心的规则驱动框架，在保证低延迟和实时性能的同时，还保持了系统的透明度和适应性。隐私保护原则是该方法的核心组成部分，通过本地计算和数据匿名化来保护用户隐私。通过超过5000次游戏体验的案例验证了这种自适应范式的

  来源：Games: Research and Practice

  时间：2025-11-07

• 家庭生活与数字游戏之间的相互作用

  ### 家庭与数字游戏的互动：深入探讨与未来发展在现代社会，数字游戏已经成为许多家庭生活中不可或缺的一部分。它们不仅作为一种娱乐方式存在，更在家庭成员之间的互动、沟通和情感连接中扮演着重要角色。随着技术的进步和游戏种类的多样化，家庭成员之间的游戏体验也在不断变化。然而，尽管数字游戏在促进家庭关系方面展现出巨大的潜力，但其在家庭环境中的应用仍然面临诸多挑战。这些挑战不仅来自于游戏本身的特性，也源于家庭内部的动态关系，例如父母对孩子的游戏行为进行干预，或者不同世代之间的兴趣差异。本文通过分析Reddit上的139篇帖子及其评论，探讨了数字游戏如何影响家庭互动以及家庭成员如何通过游戏建立联系。研究采

  来源：Games: Research and Practice

  时间：2025-11-07

• 增量数据流分析中的共同主题：一项全面调查

  摘要增量数据流分析采用了一种技术，该技术仅根据代码中修改的部分来更新数据流信息，从而重用了大量之前计算过的信息。由于大多数现实世界的软件系统都会随时间演变，增量分析技术提供了一种高效的方法，而且通常是从头开始进行完整（重新）分析的唯一可行替代方案。我们描述了现有的增量分析技术如何遵循一个共同的“重置并重新计算”范式。这种方法具有双重好处：首先，它使我们能够根据各种增量技术如何适应这一范式来对其进行研究；其次，它有助于我们识别增量数据流分析领域中的空白和待解决的问题，为未来的研究提供方向。

  来源：ACM Computing Surveys

  时间：2025-11-07

• 关于判别聚类和互信息的教程

  ### 深度判别聚类方法的演进与互信息的基石作用聚类是将数据样本划分成若干个组的无监督学习任务，每个组称为“簇”，其核心目标是发现数据中隐藏的结构。在众多聚类方法中，判别聚类方法因其独特的优势而备受关注，尤其是在处理高维数据时，它们通过神经网络构建模型，能够在判别边界上进行优化，从而更有效地发现数据的潜在结构。本文旨在回顾判别聚类方法的历史演进，特别是互信息（Mutual Information, MI）在其中所扮演的重要角色，并探讨判别聚类模型在选择簇数时面临的挑战。我们还将通过一个实际的示例，展示如何使用我们开发的Python包GemClus来实现这些方法。#### 判别聚类方法的演进在聚

  来源：ACM Computing Surveys

  时间：2025-11-07

知名企业招聘：