Autostereoscopic display technology, despite decades of development, has not achieved extensive application, primarily due to the daunting challenge of three-dimensional (3D) content creation for non-specialists. The emergence of Radiance Field as an innovative 3D representation has markedly revolutionized the domains of 3D reconstruction and generation, simplifying 3D content creation for common users and broadening the applicability of Light Field Displays (LFDs). However, the combination of these two technologies remains largely unexplored. The standard paradigm to create optimal content for parallax-based light field displays demands rendering at least 45 slightly shifted views preferably at high resolution per frame, a substantial hurdle for real-time rendering. We introduce DirectL, a novel rendering paradigm for Radiance Fields on autostereoscopic displays with lenticular lens. By thoroughly analyzing the interleaved mapping of spatial rays to screen sub-pixels, we accurately render only the light rays entering the human eye and propose subpixel repurposing to significantly reduce the pixel count required for rendering. Tailored for the two predominant radiance fields---Neural Radiance Fields (NeRFs) and 3D Gaussian Splatting (3DGS), we propose corresponding optimized rendering pipelines that directly render the light field images instead of multi-view images, achieving state-of-the-art rendering speeds on autostereoscopic displays. Extensive experiments across various autostereoscopic displays and user visual perception assessments demonstrate that DirectL accelerates rendering by up to 40 times compared to the standard paradigm without sacrificing visual quality. Its rendering process-only modification allows seamless integration into subsequent radiance field tasks. Finally, we incorporate DirectL into diverse applications, showcasing the stunning visual experiences and the synergy between Light Field Displays and Radiance Fields, which reveals the immense potential for application prospects. DirectL Project Homepage: direct-l.github.io

Weakly-supervised temporal action localization (WTAL) is a practical yet challenging task. Due to large-scale datasets, most existing methods use a network pretrained in other datasets to extract features, which are not suitable enough for WTAL. To address this problem, researchers design several modules for feature enhancement, which improve the performance of the localization module, especially modeling the temporal relationship between snippets. However, all of them omit that ambiguous snippets deliver contradictory information, which would reduce the discriminability of linked snippets. Considering this phenomenon, we propose Discriminability-Driven Graph Network (DDG-Net), which explicitly models ambiguous snippets and discriminative snippets with well-designed connections, preventing the transmission of ambiguous information and enhancing the discriminability of snippet-level representations. Additionally, we propose feature consistency loss to prevent the assimilation of features and drive the graph convolution network to generate more discriminative representations. Extensive experiments on THUMOS14 and ActivityNet1.2 benchmarks demonstrate the effectiveness of DDG-Net, establishing new state-of-the-art results on both datasets. Source code is available at https://github.com/XiaojunTang22/ICCV2023-DDGNet.

Existing document binarization methods can not extract stroke edges finely, mainly due to the fair-treatment nature of vanilla convolutions and the extraction of stroke edges without adequate supervision by boundary-related information. In this paper, we formulate text extraction as the learning of gating values and propose a novel end-to-end gated convolutions-based network (GDB) to solve the problem of imprecise stroke edge extraction. The gated convolutions are applied to selectively extract the features of strokes with different attention. Firstly, a coarse sub-network with an extra edge branch is trained to get more precise feature maps by feeding a priori mask and edge. Secondly, a refinement sub-network is cascaded to refine the output of the first stage by gated convolutions based on the sharp edge. For global information, GDB also contains a multi-scale operation to combine local and global features. Experimental results show that our proposed methods outperform the SOTA methods in terms of all metrics on average over all DIBCO datasets from 2009 to 2019 and achieve top ranking on six benchmark datasets. Available codes: https://github.com/Royalvice/GDB.

Removing degradation from document images not only improves their visual quality and readability, but also enhances the performance of numerous automated document analysis and recognition tasks. However, existing regression-based methods optimized for pixel-level distortion reduction tend to suffer from significant loss of high-frequency information, leading to distorted and blurred text edges. To compensate for this major deficiency, we propose DocDiff, the first diffusion-based framework specifically designed for diverse challenging document enhancement problems, including document deblurring, denoising, and removal of watermarks and seals. DocDiff consists of two modules: the Coarse Predictor (CP), which is responsible for recovering the primary low-frequency content, and the High-Frequency Residual Refinement (HRR) module, which adopts the diffusion models to predict the residual (high-frequency information, including text edges), between the ground-truth and the CP-predicted image. DocDiff is a compact and computationally efficient model that benefits from a well-designed network architecture, an optimized training loss objective, and a deterministic sampling process with short time steps. Extensive experiments demonstrate that DocDiff achieves state-of-the-art (SOTA) performance on multiple benchmark datasets, and can significantly enhance the readability and recognizability of degraded document images. Furthermore, our proposed HRR module in pre-trained DocDiff is plug-and-play and ready-to-use, with only 4.17M parameters. It greatly sharpens the text edges generated by SOTA deblurring methods without additional joint training. Available codes: https://github.com/Royalvice/DocDiff https://github.com/Royalvice/DocDiff.

Music generation, as a creativity problem, attracts growing attention from artificial intelligence researchers. Among the challenging tasks, lyrics-conditional melody generation aims to leverage natural language processing (NLP) techniques to generate music from texts, for which Generative Adversarial Networks (GAN) has become a promising unsupervised solution. The adversarial training of two agents, i.e., generator and discriminator, allows GAN to achieve a better generation performance and has been proven effective in conditional generation tasks. In this paper, we propose the multi-criteria relational GAN (MRGAN), which includes a relation memory-based generator and two discriminators with a unique discrimination criterion each. The relational memory in the generator is adopted for long-time dependency modeling. Meanwhile, the two discriminators can judge both musical quality and conditional correspondence. Based on the bilingual evaluation understudy (BLEU) score, a new metric, named Music-BLEU, has also be designed to evaluate the lyrics-conditional melody generation. Experimental results verify that MRGAN outperforms existing approaches in related key metrics.

Abstract The hardware description language Verilog has been standardized and widely used in industry. Multithreaded Discrete Event Simulation Language (MDESL) is a Verilog-like language and it contains a rich variety of interesting features such as the event-driven computation and shared-variable concurrency as well as the realtime feature. In this paper, we present the denotational semantics for MDESL based on UTP. First a discrete time semantic model is proposed to describe the observation-oriented semantics for MDESL. The observations record the change of variables of atomic actions over time. Then the healthy formulae are defined to denote all different behaviors of programs and the semantics of programs is expressed in terms of healthy formulae. In addition, we demonstrate some interesting properties about the MDESL programs expressing as algebraic laws and their proofs are supported by our formalized denotational semantics. Our theoretical approach is complemented by a practical one, we use the theorem proof assistant Coq to formalize the UTP-based semantics for MDESL. The correctness of the algebraic laws is also verified via the mechanical approach in Coq. Our work provides a novel way to verify the correctness of UTP-based semantics forMDESL both in a theoretical approach and in a practical approach. It is also a new attempt for the application of Coq in the mechanized semantics.

Model Driven Engineering (MDE) uses models to represent the core part of the software systems. The Unified Model Language (UML) is a widely accepted standard for modeling software systems. Although UML provides numbers of concepts and diagrams to describe the system, there is still an unsolved problem that the semantics and refinement relations of models are not formally defined. In this paper, we apply the constructive type theory to formalize the class diagrams and object diagrams. A suitable subset of UML static models is identified and formally defined. The theorem assistant Coq is applied to encode the semantics of class diagrams. Moreover the refinement relations are also formalized in Coq. The whole approach is supported by tools that do not constrain the semantic definition's expressiveness and flexibility while making it machine-checkable. Our approach offers a novel way for giving a precise foundation in UML and contributes to the goal of improving the overall trustworthy software systems by combining theoretical and practical techniques.

The Unified Modeling Language (UML) provides a number of diagrams to describe the modeling system from different perspectives, which contain overlapping information about the systems.However, it does not provide any means of meticulously checking consistencies among the overlapping elements.In this study, we propose an approach for consistency checking of UML class diagrams and object diagrams using Prolog.First we formalize the model elements based on metamodel and convert the models into Prolog facts.Then we define some consistency rules that are encoded into Prolog.The Prolog's reasoning engine automatically checks the consistencies of models.In addition, we provide interfaces to query models for properties, elements and submodels.The design errors can be effectively avoided and the correctness of code-generalization can be guaranteed according to our approach.

Verilog is a hardware description language (HDL) that has been standardized and widely used in industry. Multithreaded discrete event simulation language (MDESL) is a Verilog-like language. It contains interesting features such as event-driven computation and shared-variable concurrency. This article considers how the algebraic semantics links with the operational semantics for MDESL. Our approach is from both the theoretical and practical aspects. The link is proceeded by deriving the operational semantics from the algebraic semantics. First, we present the algebraic semantics for MDESL. We introduce the concept of head normal form. Second, we present the strategy of deriving operational semantics from algebraic semantics. We also investigate the soundness and completeness of the derived operational semantics with respect to the derivation strategy. Our theoretical approach is complemented by a practical one, and we use the theorem proof assistant Coq to formalize the algebraic laws and the derived operational semantics. Meanwhile, the soundness and completeness of the derived operational semantics is also verified via the mechanical approach in Coq. Our approach is a novel way to formalize and verify the correctness and equivalence of different semantics for MDESL in both a theoretical approach and a practical approach.

The Unified Modeling Language (UML) is an industry standard for modeling analysis and design. However, the semantics of UML is not precisely defined and the correctness of refinement relations cannot be verified. In this study, we use the theorem proof assistant Coq to formalize and mechanize the semantics of UML-Statecharts and the refinement relations between models. Based on the mechanized semantics, the desired properties of both the semantics and the refinement relations can be described and proven as predicates and lemmas. This approach provides a promising way to obtain certified fault-free modeling and refinement.

Model-based engineering has emerged as a key set of technologies to engineer software systems. While system source code is expected to match with the designed model, legacy systems and workarounds during deployment would undoubtedly change the source code, making the actual running implementation mismatch with its model. Such mismatch poses a challenge of maintaining the conformance between the model and the corresponding implementation. Prior techniques, such as model checking and model-based testing, simply assumed the sole correctness of the model or the implementation, which is naive since they both could contain correct information (e.g. representing either the software requirements or the actual running environment).In this paper, we aim to address this problem through model-based continuous verification (ConV), an iterative verification process that links the traditional model checking phase with the software testing phase to a feedback loop, ensuring the conformance between the system model and its implementation. It allows to execute the abstract test cases over the implementation through a semi-automatic binding mechanism to guide the update of the code, and augments system properties from the actually running system to guide the update of the model through model checking. Based on these techniques, we implemented Eunomia, a conformance verification system, to support the continuous verification process. Experiments show that Eunomia can effectively detect and locate inconsistencies both in the model and the source code.

The formal specification of design patterns is central to pattern research and is the foundation of solving various pattern-related problems. In this paper, we propose a metamodeling approach for pattern specification, in which a pattern is modeled as a meta-level class and its participants are meta-level references. Instead of defining a new metamodel, we reuse the Unified Modeling Language (UML) metamodel and incorporate the concepts of Variable and Set into our approach, which are unavailable in the UML but essential for pattern specification. Our approach provides straightforward solutions for pattern-related problems, such as pattern instantiation, evolution, and implementation. By integrating the solutions into a single framework, we can construct a pattern management system, in which patterns can be instantiated, evolved, and implemented in a correct and manageable way.

Approaches to enforcing communication integrity in the implementation, exemplified by ArchJava, consider only architectural constraints, without taking into account the late integration of prebuilt components into the architecture. This may hinder the practice of architecture in the common component building. In this paper, we present an approach to supporting the integration of prebuilt components in the context of the architectural constraints. This approach is described in terms of a novel design pattern, an architectural description language (ADL) JCMPL and a toolset JCMP. The language and toolset are designed based on the pattern to dynamically link the architectural constraints with the component building. To achieve this goal, an important step is to automatically translate the connector specification defined in the architecture into the connector implementation, which can serve as glue codes to connect two prebuilt components together by transferring the methods invocation between two components.

Unit testing is a methodology for testing small parts of an application independently of whatever application uses them. It is time consuming and tedious to write unit tests, and it is especially difficult to write unit tests that model the pattern of usage of the application. Aspect-oriented programming (AOP) addresses the problem of separation of concerns in programs which is well suited to unit test problems. What's more, unit tests should be made from different concerns in the application instead of just from functional assertions of correctness or error. In this paper, we firstly present a new concept, application-specific Aspects, which mean top-level aspects picked up from generic low-level aspects in AOP for specific use. It can be viewed as the separation of concerns on applications of generic low-level aspects. Second, this paper describes an aspect-oriented test description language (AOTDL) and techniques to build top-level aspects for testing on generic aspects. Third, we generate JUnit unit testing framework and test oracles from AspectJ programs by integrating our tool with AspectJ and JUnit. We use runtime exceptions thrown by testing aspects to decide whether methods work well. Finally, we present a double-phase testing way to filter out meaningless test cases in our framework.