The technical complexity of research papers often limits their reach, necessitating more accessible formats like scientific videos to disseminate key insights through engaging narration. However, existing automated methods primarily focus on static posters or slide presentations that remain template-bound and linear. Shifting to audience-adaptive video synthesis requires addressing non-linear narrative orchestration and the joint synchronization of disparate multimodal assets. We introduce VideoAgent, a modular framework that redefines scientific video synthesis as an intent-driven planning problem. By decoupling content understanding from multimodal synthesis, VideoAgent adaptively interleaves static slides with dynamic animations to match the semantic density of the narration. We further propose SciVidEval, a benchmark evaluating multimodal quality and pedagogical utility through automated metrics and human knowledge transfer studies. Extensive experiments demonstrate that VideoAgent effectively conveys complex technical logic with high narrative fidelity and communicative impact.

In recent years, sketching has emerged as a pivotal technique for identifying heavy hitters (items with high frequency) in large-scale data streams. Despite this progress, the majority of existing sketch algorithms are tailored primarily for detecting local heavy hitters within a single data stream, with only a few capable of extending their application to global heavy hitters across distributed data streams. A common challenge encountered by these algorithms is balancing performance with accuracy. To address this challenge, we introduce HeavyLocker, a novel sketch algorithm that takes advantage of a distinct feature of real data streams: the separability of heavy hitters. By leveraging this attribute, HeavyLocker precisely locks and protects potential heavy hitters during the data stream processing, ensuring accuracy in local heavy hitter detection without compromising on speed. This unique capability also facilitates its application to global detection tasks. Through theoretical analysis, we validate the efficacy of HeavyLocker's locking mechanism. Our extensive experiments show that HeavyLocker outperforms five benchmarked algorithms in accuracy and maintains fast speed for both local and global heavy hitter detection, significantly reducing errors by up to an order of magnitude compared to the renowned Double-Anonymous Sketch.

Sketch algorithms are crucial for identifying top-k items in large-scale data streams. Existing methods often compromise between performance and accuracy, unable to efficiently handle increasing data volumes with limited memory. We present Bubble Sketch, a compact algorithm that excels in both performance and accuracy. Bubble Sketch achieves this by (1) Recording only full keys of hot items, significantly reducing memory usage, and (2) Using threshold relocation to resolve conflicts, enhancing detection accuracy. Unlike traditional methods, Bubble Sketch eliminates the need for a Min-Heap, ensuring fast processing speeds. Experiments show Bubble Sketch outperforms the other seven algorithms compared, with the highest throughput and precision, and surpasses HeavyKeeper in accuracy by up to two orders of magnitude.

Requirements-based testing is one of the most commonly used ways to ensure the correctness of software, especially for embedded control software in safety-critical domains such as spacecraft and railway systems. Many industrial standards such as the DO-333 and EN50128 also request rigorous requirements-based software testing. To test embedded control software effectively and efficiently, generating high-quality test cases automatically is extremely important. However, existing methods for generating test cases from requirements require intensive manual efforts and expertise. To address this problem, we proposed an automatic requirements-based software testing method for embedded control software. To obtain automatic test case generation and precise test oracles derivation, requirements specification should be precise and readable for the industrial practitioners. Therefore, we use the light-weight domain-specific formal description language, CASDL (Casco Accurate Specification Description Language) for the industrial practitioners to define software requirements into formal specifications at the first step. Based on the formal specification, we propose an algorithm to automatically generate test inputs that satisfy the MC/DC criteria suggested by typical industrial standards and precise test oracles can be derived by “running” the specification with such test inputs. To this end, we proposed an algorithm for simulating the formal specification to generate the test oracles, i.e., the expected outputs corresponding to the test inputs. To facilitate the application of this method in the industry, we have built a tool that can automatically perform the overall testing process. To validate and evaluate its effectiveness in real industrial projects, we have applied it in testing a real Automatic Train Protection (ATP) system provided by our industrial partner, the Casco Signal Co., Ltd (one of the largest railway control system companies in China). In the case study on ATP requirements, our approach generated test cases for 129 requirement items following MC/DC criteria and caught 40 inconsistencies between Casco’s requirements and implementation.

Formal methods are promising for modeling and analyzing system requirements. However, applying formal methods to large-scale industrial projects is a remaining challenge. The industrial engineers are suffering from the lack of automated engineering methodologies to effectively conduct precise requirement models, and rigorously validate and verify (V&V) the generated models. To tackle this challenge, in this paper, we present a systematic engineering approach, named Formal Requirement Engineering Platform in Aircraft (FREPA), for formal requirement modeling and V&V in the aerospace and aviation control domains. FREPA is an outcome of the seamless collaboration between the academy and industry over the last eight years. The main contributions of this paper include 1) an automated and systematic engineering approach FREPA to construct requirement models, validate and verify systems in the aerospace and aviation control domain, 2) a domain-specific modeling language AASRDL to describe the formal specification, and 3) a practical FREPA-based tool AeroReq which has been used by our industry partners. We have successfully adopted FREPA to seven real aerospace gesture control and two aviation engine control systems. The experimental results show that FREPA and the corresponding tool AeroReq significantly facilitate formal modeling and V&V in the industry. Moreover, we also discuss the experiences and lessons gained from using FREPA in aerospace and aviation projects.

Formal method is a promising solution for precise software requirements modeling and V&V (Validation and Verification). However, domain experts are suffering from using complex mathematics formal notations to precisely describe their domain specific software requirements. Meanwhile, the lack of systematic engineering methodologies that can effectively encompass precise requirements modeling and rigorous requirements V&V makes the application of formal methods in industry still a big challenge. To tackle this challenge, in this paper, we present a domain experts centric approach to the formal requirements modeling and V&V in the domain of embedded control software. The major advancements of the approach are: 1) a domain-specific and systematic engineering approach to the formal requirements specification construction and 2) scenario-based requirements validation and verification requirements technique. Specifically, the approach offers a domain-specific template for formal specification construction through a three-step specification evolution process. For formal requirements V&V, diagrams are derived from formal specification and domain experts' concerned scenarios can be checked based on the diagrams. These modeling and V&V technologies are coherently incorporated in the approach and fully automated by a supporting tool. We have applied the approach real software projects of our industrial partners. The experimental results show that it significantly facilitates the formal modeling and V&V in industry.

We present Prema, a tool for Precise Requirement Editing, Modeling and Analysis. It can be used in various fields for describing precise requirements using formal notations and performing rigorous analysis. By parsing the requirements written in formal modeling language, Prema is able to get a model which aptly depicts the requirements. It also provides different rigorous verification and validation techniques to check whether the requirements meet users' expectation and find potential errors. We show that our tool can provide a unified environment for writing and verifying requirements without using tools that are not well inter-related. For experimental demonstration, we use the requirements of the automatic train protection (ATP) system of CASCO signal co. LTD., the largest railway signal control system manufacturer of China. The code of the tool cannot be released here because the project is commercially confidential. However, a demonstration video of the tool is available at https://youtu.be/BX0yv8pRMWs.