4 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…
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…