B & uuml;chi automata have applications in formal verification, e.g., in deciding whether a system satisfies given properties. We provide a definition of B & uuml;chi automata based on first order logics for representing infinite state systems, and investigate rules for proving emptiness and non-emptiness of such automata. We then apply these rules to solve the problem of verifying correctness of concurrent transition systems, leading to a relatively complete approach for proving and disproving LTL (Linear Temporal Logic) specifications. This approach overcomes weaknesses of existing work based on well-founded sets in the sense that the relative completeness does not depend on additional specification for ensuring progress of non-stuttering transitions. On the practical aspect, we provide a set of examples with an experimental verification condition generation tool to demonstrate the potential applicability of the approach for the verification of concurrent systems.

Software bugs often arise from inconsistencies between software requirements documented in natural language and their code implementations. Formal verification is a proven technique for solving this problem by formalizing requirements into specifications. However, specifications are notoriously difficult to write correctly. Consequently, automating the formalization of natural language requirements has attracted growing interest, especially after the advent of large language models (LLMs). This paper investigates the capability and potential of LLMs to formalize task requirements into Dafny specifications. We propose and evaluate three progressively enhanced prompting strategies—Basic Prompting, Syntax-Augmented Prompting, and Semantics-Augmented Prompting—to assess LLMs’ capability of generating Dafny specifications. Additionally, we develop an evaluation method to assess specification correctness, applicable both with and without ground truth. Experiments are carried out across three LLMs (GPT-4, DeepSeek-V3, and DeepSeek-R1) on two datasets derived from MBPP, a benchmark consisting of basic Python programming problems. Results show that Semantics-Augmented Prompting effectively improves both syntactic and semantic correctness of LLM-generated Dafny specifications. To deepen our understanding of LLMs’ formalization potential, we also conduct manual inspections and qualitative analysis, revealing the limitations of generating Dafny specifications with LLMs and bring up suggestions.

Maritime transportation business suffers from trust issues and burdensome paperwork. Blockchain-based smart contracts are a promising solution. Due to the nature of the blockchain, it is important to verify smart contracts before deployment, especially for its functionality and legality. In this paper, we propose a verification framework that automatically verifies the functionality and legality requirements of maritime transportation smart contracts. Smart contracts of an application, based on a set of templates, are modeled in a network of timed automata; domain-specific requirements are collected and formulated as temporal logic formulas; real-time model checking tool UPPAAL is then used to check whether these requirements are satisfied. We carry out experiments on nine real-world smart contracts to show the effectiveness and feasibility of our framework. We also compare our work with existing tools to show its effectiveness and efficiency.

Simplifying programs before verification aims to reduce program complexity thus saving the verification effort. In the paper, we investigate the impacts of applying program slicing before verification. We consider various techniques and verifiers for the workflow and adopt benchmarks from the software verification community to evaluate the strengths and issues in adopting slicing techniques for program simplification. The evaluation considers reachability as the property to be verified and checks the consistency of verification results, the improvement of verification efficiency, and the advantages of different toolchains when verifying reachability. The investigation shows that most programs keep consistent verification results after slicing and verifying programs with much code unrelated to the properties becomes faster when slicing is applied before verification. However, it is surprising that verification time for some programs can be significantly longer after slicing. We have investigated the reasons for such phenomenon concerning the features of these programs, and provide insightful conclusions obtained from using the slicing+verification approach.

Since the inception of Bitcoin in 2008, blockchain technology has had a significant impact on many fields. The lack of effective communication between heterogeneous and isolated blockchains, however, restricts the promotion and ecological development of blockchain industry. In this context, crosschain technology has rapidly developed and become a new research hotspot. Due to the decentralized nature of blockchain and the complexity of crosschain scenarios, crosschain technology faces huge security risks. In this paper, we propose formal analysis of the IBC protocol, one of the most popular crosschain communication protocols, aiming to help developers design and implement crosschain technologies more securely. We formalize three main components of the IBC protocol with TLA+, a temporal logic specification language, and verify some important requirements with model checking tool TLC. The verification results are analyzed comprehensively. Issues found through our formal analysis have been reported to the community, most of which have been acknowledged. We also propose some recommendations for removing potential risks.

A smart contract is a computerized protocol running on the blockchain, which provides a reliable environment for transactions among trustless participants. The business of maritime transportation is usually with multifarious participants and burdensome paperwork. Blockchain-based smart contract systems are promising to improve the efficiency and transparency of the transactions. However, due to the gap between domain experts and programmers, and the diversity of maritime business scenarios, it is challenging to efficiently develop reliable smart contracts for this domain. In this paper, we propose MariSmart, a novel development framework for maritime transportation smart contracts, which consists of a business logic model and a set of Solidity templates. The templates are designed based on the business logic model extracted from the domain knowledge. We carry out case studies on three real-world maritime transportation systems to show the feasibility and effectiveness of the framework.

One of the main concerns of automated verification and error detection of software designs is the efficiency. Although bounded model checking (BMC) has been proven to be effective for error detection, further improvement of the efficiency is of great importance to the practical application of such methods. The development of BMC approaches is based on bounded semantics of temporal logics. Therefore the design of bounded semantics is essential for the subsequent BMC approaches. In this work, we propose a non-monotone bounded semantics for the linear temporal logic (LTL), and consequently a non-monotone BMC approach for improving the efficiency of bounded model checking. To this end, the information that a formula is unsatisfiable in an early step of checking is partly taken into consideration in a later one (in the sequence) in order to provide possibility for dismissing some of the irrelevant paths quickly in checking the later more complicated bounded model. The experimental results have shown that this approach has clear advantage over the traditional one on the test cases with respect to the efficiency. A comparison of such a non-monotone BMC approach with the traditional one implemented in the well-known model checking tools NuSMV and nuXmv is also reported.

Combined with smart contracts, the application of blockchain techniques has grown faster and broader. However, it is very difficult to write secure and functionally correct smart contracts because of the openness of blockchain platforms. Formal verification, such as model checking, has been proven to be an effective way of guaranteeing security and correctness of systems. In this paper, we propose a novel model checking based framework, called mcVer, to support the verification of smart contracts written in Solidity. Built on model checking tool VERDS, the mcVer framework is able to verify not only safety properties but also liveness properties of smart contracts. For the properties that are not satisfied, mcVer produces a counter example by showing a sequence of statements in the original Solidity program as a hint for fault localization. We implemented the automatic transformation from a subset of the Solidity language to the modeling language of VERDS, that therefore provides automatic verification for smart contracts. Experiments are carried out on various cases, including checking contracts for finding typical security vulnerabilities and verifying properties of an access control smart contract. The experimental results demonstrate the flexibility and efficiency of mcVer.

The relation between automata and temporal logics has been widely studied, and as a consequence, automata theoretical approaches have been successfully applied to the checking of satisfiability of temporal logic formulas and the verification of temporal properties in various settings. Epistemic logics are natural formalisms for reasoning of knowledge in multi-agent systems (MAS) and are often combined with temporal logics for the reasoning of a combination of knowledge and temporal behaviors of MAS. However, the relation between automata and the logics combined with epistemic logic has not been sufficiently explored. In this paper, we explore the relation between them by developing a mechanism for handling epistemic operators. In particular, we present a definition of multi-agent automata, the construction of such automata from formulas of the linear dynamic epistemic logic (LDLK), which is an extension of epistemic logic and has high expressivity, and an approach for solving the satisfiability problem of LDLK. Experimental results on the translation of LDLK formulas to multi-agent automata are reported.

蓝牙、WiFi等网络技术的进步推动物联网(IoT)的发展,然而IoT在方便了人们生活的同时也存在严重的安全隐患.若无安全的访问控制,非法接入IoT的访问可能给用户带来各方面的损失.传统的访问控制方法需要一个可信任的中心节点,不适合节点分散的IoT环境.区块链及智能合约的出现为IoT应用的访问控制提供了更有效的解决方案,但用一般测试方法难以保证实现IoT应用的访问控制智能合约的正确性.针对这个问题,提出一种利用模型检测工具Verds对访问控制智能合约进行形式化验证从而保障合约正确性的方法.该方法利用状态迁移系统定义Solidity智能合约的语义,应用计算树逻辑(CTL)公式描述所要验证的性质,并对智能合约交互及用户行为进行建模,从而形成Verds的输入模型及所要验证性质,然后利用Verds验证待测性质的正确性.方法核心是Solidity合约子集到Verds输入模型的转换.对两个IoT资源访问控制智能合约的实验结果表明,该方法可以对访问控制合约的典型场景及期望性质进行验证,提升了智能合约的可靠性.

Model checking is considered one of the most practical applications of theoretical computer science in the verification of concurrent systems, and model checking tools are very important for such applications. This paper presents the model checking tool VERDS with the theoretical background, basic functionalities and modeling techniques with various examples. In particular, the tool includes an implementation of a bounded correctness checking approach which can be seen as an extension of bounded model checking and complementary to the traditional symbolic model checking. VERDS is also flexible for extension. We show how it is extended to handle discrete time models. We carry out case-studies of a kind of task scheduling problems, in which time specification is essential. The experimental results show that VERDS is not only feasible for solving practical problems but also with good performance in solving such problems.

TLC flash has three types of pages to accommodate the three bits in each TLC physical cell exhibiting very different program latencies. This paper proposes PA-SSD to effectively improve the overall performance by exploiting the dissimilarity of TLC pages on program latency throughout the write request handling workflow. The main idea behind PA-SSD is to coordinately allocate the same type of pages for sub-requests of any given user write request, to mitigate the potential program latency imbalance among the sub-requests, and to schedule sub-requests according to their page-types. We achieve the PA-SSD design goal by answering three key research questions: (1) how to properly determine page-type for each user write request? (2) how to actually allocate a physical page for each sub-request with an assigned page-type from (1)? (3) how to effectively schedule the sub-requests in the chips queues when their page-types are judiciously allocated from (2)? To answer the first question, we propose seven page-type specifying schemes to investigate their effects under different workloads. We answer the second question by redesigning the page allocation strategy in TLC SSD to uniformly and sequentially determine physical pages for allocation following the internal programming process of TLC flash. Lastly, a page-type aware scheduling policy is presented to reorder the sub-requests within chips’ queues. Our experiments show that PA-SSD can accelerate both the write and read performance. Particularly, our proposed queue-depth based page-type specifying scheme improves write performance by 2.6 times and read performance by 1.5 times over the conventional TLC SSD.

Summary form only given, as follows. The complete presentation was not made available for publication as part of the conference proceedings. Correctness is an important issue in computer science and software engineering. For concurrent systems, the definition of correctness is usually based on properties of infinite execution paths. Bounded correctness is a kind of correctness defined on finite paths, and provides a different view on the issue of correctness. This talk focuses on the concept of bounded correctness and the relation between correctness and bounded correctness. For the purpose of verification, the definition of correctness based on infinite paths is not directly applicable as a means for verification, and the approaches for such a purpose include those based on the analysis of strongly connected components and on the computation of fixed points. On the other hand, correctness may be verified in terms of bounded correctness by an approach derived from the definition of bounded correctness. The complementariness of these verification approaches is explained.

Squeezed state light is a fundamental resource for many quantum optics experiments. Important applications like quantum-enhanced magnetometer and quantum key distribution, require the squeezing level as high as possible. In balanced homodyne detection, the detector output is directly proportional to the noise of the squeezed beam. The detected quadrature is dependent on the relative phase between the squeezed beam and local oscillator. Here, we present a balanced homodyne detector (BHD) with independent phase control and noise detection branches. The independence between the phase control and noise detection branches is experimentally verified, the two branches are independently optimized according to the practical requirements. With the BHD, a bright squeezed light at 1550 nm with quantum noise reduction of 10.3 dB is directly detected. After stabilizing the relative phase between the squeezed states and local oscillator by the phase locking branch of the BHD, the fluctuation of the noise suppression is ±0.2 dB by 1-h testing time.

To address the write performance problem suffered by MLC/TLC flash, researchers have proposed hybrid SSD that aims to combine the strengths of SLC flash, used as the write-buffer zone for its superior write performance, and MLC/TLC flash, as the capacity zone for its high storage density. While leveraging SLC as a physical write-buffer zone is proven effective in traditional 2D hybrid SSDs, how to effectively incorporate SLC into a 3D-stacked TLC to form a hybrid SSD has not been studied to the best of our knowledge. Yet this is a timely and important performance issue for 3D-stacked TLC given its one-shot programming scheme that results in much worse write performance than the programming scheme in 2D TLC where pages are associated with different bits of a cell and programmed in sequence separately. We believe that naively adopting the two-physical-zone approach to 3D hybrid SSD will miss a great opportunity for performance optimization because it ignores the inherent four-level parallelism (channel/chip/die/plane) of the flash chip array. To this end, we propose in this paper an SLC and Parallelism Aware hybrid SSD (SPA-SSD) to take full advantages of SLC's superior write performance, the internal multi-level parallelism of SSD, and the high storage density of 3D-stacked TLC flash. Two novel techniques enable SPA-SSD to be highly effective: (1) Type-Parallelism Joint Page Allocation (TPJ-PA), which allocates pages for write transactions according to not only available SLC pages but also parallelism to maximize resource utilization within the hybrid SSD, and (2) Queue-length and Parallelism Constrained Data Migration (QPC-DM), which triggers data migration without degrading user write performance by analyzing the device queue length and available flash resources. To evaluate performance of SPA-SSD, a hybrid SSD simulator, called HybridSim, is developed based on MQSim. Experimental results on HybridSim show that TPJ-PA improves write throughput by 60%, while QPC-DM improves write throughput by up to 10 times. Besides, trace-driven experiments on HybridSSD demonstrate that SPA-SSD improves the write latency to the flash by up to two orders of magnitude over the state-of-the-art designs.

Modal logic S5 has found various applications in artificial intelligence. With the advances in modern SAT solvers, SAT-based approach has shown great potential in solving the satisfiability problem of S5. The scale of the SAT encoding for S5 is strongly influenced by the upper bound on the number of possible worlds. In this paper, we present a novel SAT-based approach for S5 satisfiability problem. We show a normal form for S5 formulas. Based on this normal form, a conflict graph can be derived whose chromatic number provides an upper bound of the possible worlds and a lot of unnecessary search spaces can be eliminated in this process. A heuristic graph coloring algorithm is adopted to balance the efficiency and optimality. The number of possible worlds can be significantly reduced for many practical instances. Extensive experiments demonstrate that our approach outperforms state-of-the-art S5-SAT solvers.

This work is on methodologies for checking multi-agent systems against temporal-epistemic specifications. Since behaviors that comply with temporal-epistemic specifications in general (or theoretically) involve infinite sequences of actions of the involved agents, we must avoid checking such specifications based on such infinite sequences. This work at the theoretical side provides a bounded semantics for the temporal-epistemic specification formalism CTLK such that checking an infinite number of steps can be reduced to checking a finite number of steps, and at the practical side develops an approach based on the semantics and QBF-solving techniques for the verification purpose. The approach has been implemented and experimental data show that there exist verification problems that can be verified by this approach more efficiently than BDD based symbolic model checking.

The Belief-Desire-Intention (BDI) architecture is a framework for studying computational agents capable of rational behaviors. The behaviors of such agents may be modeled by possible world structures, for the specification of the behaviors, CTLBDI may be used. As multi-agent systems are increasingly complex, the problem of their verification is acquiring importance. This work develops a symbolic model checking approach for the verification of CTLBDI properties within the BDI-architecture. In addition, we develop a symbolic approach for checking whether a model satisfies the weak and strong realism constraints. The approaches for model checking and realism checking have been implemented, and the experimental data show that the approaches are able to handle models with a fairly large number of possible worlds.

Multilevel cell (MLC) states with lower threshold voltage endure less cell damage, lower retention error, and less current consumption. Based on these characteristics, it is opportunistic to strengthen MLC flash by introducing bit-flipping that reshapes state proportions on MLC pages. In this paper, we present a holistic study of bit-flipping schemes upon MLC flash in theory and practice. Specifically, we systematically investigate effective bit-flipping schemes and propose four new schemes on manipulating MLC states. We further design a generic implementation framework, named MLC bit-flipping framework, to implement bit-flipping schemes within solid state drives controllers, nicely integrating with existing system-level optimizations to further improve overall performance. The experimental results demonstrate that our proposed bit-flipping schemes standalone can reduce up to 28% cell damages and 53% retention errors. Our circuit-level simulation manifests that the bit-flipping latency on a page is less than 4 $\mu \text{s}$ when using 8K logic gates.

The study of modal logics and various bisimulation equivalences so far shows the following progression: 1. weak bisimilarity is characterized by Hennessy-Milner logic (HML), a simple propositional modal logic with a weak possibility modality, and 2. extending HML by refining the weak possibility modality one obtains a logic which characterizes branching bisimilarity, a refinement of weak bisimilarity, and 3. further extending the logic with a divergence modality one obtains a logic which characterizes branching bisimilarity with explicit divergence, a refinement of branching bisimilarity. In this paper, we explore the development by exchanging the above 2 and 3, i.e. by first extending HML with a divergence modality and then refining the weak possibility modality in the extended logic. We have the following findings: A. extending HML with a new divergence modality one obtains a new logic which characterizes complete weak bisimilarity, an equivalence relation with distinguishing power in between weak bisimilarity and branching bisimilarity with explicit divergence; B. further extending the obtained logic by refining the weak possibility modality in it one obtains another logic which characterizes branching bisimilarity with explicit divergence. As main results of the paper, the logic in A. provides a modal characterization for complete weak bisimilarity, and moreover the two new logics in A. and B. are both sub-logics of the known logic obtained in above 3.