Timing specifications are critical in real-time embedded systems, where even small time deviations may cause system failures. Although designers often model these systems using automata or sequence diagrams, formally verifying their timing properties remains computationally expensive due to the state-space explosion problem. This research proposes an acceleration framework for verifying interrupt-driven real-time systems against explicit clock value timing properties. Using partial order reduction and first-order logic encoding during verification, we abstract certain constructs in the models as parcels to avoid unnecessary state-space exploration. This parcel-based abstraction integrates seamlessly with formal models that support interruption mechanisms. Based on the framework, we implement two acceleration tactics: inclusive and external parcel pruning. Our prototype tool, Parcel, demonstrates the framework's efficacy on both existing models and large-scale models synthesized by LLMs. Experiments show that Parcel significantly improves the verification speed of large-scale, interrupt-driven models, outperforming state-of-the-art tools by thousands of times.

Context sensitivity is a foundational technique in pointer analysis, critical and essential for improving precision but often incurring significant efficiency costs. Recent advances focus on selective context-sensitive analysis, where only a subset of program elements, such as methods or heap objects, are analyzed under context sensitivity while the rest are analyzed under context insensitivity, aiming to balance precision with efficiency. However, despite the proliferation of such approaches, existing methods are typically driven by specific code patterns, therefore lacking a comprehensive theoretical foundation for systematically identifying code scenarios that benefit from context sensitivity. This paper presents a novel and foundational theory that establishes a sound over-approximation of the ground truth, i.e., objects that really improve precision under context sensitivity. The proposed theory reformulates the identification of this upper bound into graph reachability problems over a typical Pointer Flow Graph (PFG), each of which can be efficiently solved under context insensitivity, respectively. Building on this theoretical foundation, we introduce our selective context-sensitive analysis approach, Moon . Moon performs both backward and forward traversal on a Variable Flow Graph (VFG), an optimized variant of PFG designed to facilitate efficient traversal. This traversal systematically identifies all objects that improve precision under context sensitivity. Our theoretical foundation, along with carefully designed trade-offs within our approach, allows Moon to limit the scope of objects to be selected, leading to an effective balance between its analysis precision and efficiency. Extensive experiments with Moon across 30 Java programs demonstrate that Moon achieves 37.2 X and 382.0 X speedups for 2-object-sensitive and 3-object-sensitive analyses, respectively with negligible precision losses of only 0.1% and 0.2%. These results highlight that the balance between efficiency and precision achieved by Moon significantly outperforms all previous approaches.

Specifying channel-based asynchronous circuits in SystemVerilog is a promising alternative design paradigm to combine the advantages of asynchronous circuits and industrial electronic design automation supports. However, communicating through channels can be error-prone, potentially introducing deadlocks that cannot be detected easily through simulation. In contrast, model checking can reliably identify deadlocks, but faces challenges related to scalability and modeling capability. This research proposes a novel model checking approach, named Verilock, to detect deadlocks of channel-based asynchronous circuits specified in SystemVerilog. To address the issue of modeling capability, Verilock extracts intermodule communication behavior from SystemVerilog circuit designs and builds models in communication protocols specifically designed for this purpose. Additionally, Verilock employs a novel hierarchical model checking algorithm that conducts localized verification of well-formed groups of the system from the bottom up, thus reducing the size of the checking problems and presenting the opportunity to parallelize the checking process. Extensive experimental evaluations confirm the efficiency of Verilock in publicly accessible and randomly synthesized large-scale asynchronous circuits. Remarkably, significant benefits of the hierarchical checking approach are demonstrated through an ablative experiment.

Timing analysis of scenario-based specifications (SBS) such as message sequence charts and UML interaction models plays an essential role in the design phase of real-time system development. However, it is time-consuming and labor-intensive to conduct analysis on the satisfiability of the timing constraints. In this article, we propose a novel SAT and linear programming (LP) collaborative timing analysis approach named TASSAT for SBS. Instead of using depth-first traversal algorithms, TASSAT encodes the structures of the SBS into propositional formulas and use the SAT solver to find candidate paths. The timing analysis of candidate paths is then reduced to LP problems, where irreducible infeasible set of the infeasible path can be used to prune unnecessary search space of the SAT solver. The experimental results show that TASSAT is effective and offers better performance than existing tools in terms of both time consumption and memory footprint.