Constructing Property-Oriented Models for Verification

Jifeng He, Shengchao Qin, Adnan Sherif

Research output: Chapter in Book/Report/Conference proceedingConference contribution

121 Downloads (Pure)


This paper advocates a general approach to formal verification by constructing property-oriented models. We instantiate the approach using timing properties, and construct a heterogeneous untimed model in which time is abstracted away, so that we can verify timing properties in an untimed framework. The correctness of property-oriented model construction is ensured by the conformance of semantic and syntactic mappings.
Original languageEnglish
Title of host publicationUnifying theories of programming
Publication statusPublished - 2006
Event1st International Symposium on Unifying Theories of Programming - Walworth Castle, United Kingdom
Duration: 5 Feb 20067 Feb 2006
Conference number: 1

Publication series

NameUnifying Theories of Programming
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference1st International Symposium on Unifying Theories of Programming
Country/TerritoryUnited Kingdom

Bibliographical note

Author can archive post-print (ie final draft post-refereeing).

Cite this