1 citations · 1 across the 5 of their papers we have counts for
5 papers
Automatic Detection, Validation and Repair of Race Conditions in Interrupt-Driven Embedded Software
Yu Wang, Fengjuan Gao, Linzhang Wang +4
Interrupt-driven programs are widely deployed in safety-critical embedded systems to perform hardware and resource dependent data operation tasks. The frequent use of interrupts in…
Formal Verification of `Programming to Interfaces' Programs
Jianhua Zhao, Xuandong LI
This paper presents a formal approach to specify and verify object-oriented programs written in the `programming to interfaces' paradigm. Besides the methods to be invoked by its c…
Online Verification of Control Parameter Calculations in Communication Based Train Control System
Lei Bu, Xin Chen, Linzhang Wang +1
Communication Based Train Control (CBTC) system is the state-of-the-art train control system. In a CBTC system, to guarantee the safety of train operation, trains communicate with…
Scope Logic with Local Reasoning and Pre/Post-State Properties
Jianhua Zhao, Xuandong Li
This paper presents an extension to Hoare logic for pointer program verification. Logic formulas with user-defined recursive functions are used to specify properties on the program…
Scope Logic: Extending Hoare Logic for Pointer Program Verification
Jianhua Zhao, Xuandong Li
This paper presents an extension to Hoare logic for pointer program verification. First, the Logic for Partial Function (LPF) used by VDM is extended to specify memory access using…