welcome: please sign in

Upload page content

You can upload content for the page named below. If you change the page name, you can also upload content for another page. If the page name is empty, we derive the page name from the file name.

File to load page content from
Page name
Comment

location: AbstractChinWeiNgan

Program Verification and Specification Inference

Wei-Ngan Chin

Traditionally, the focus of specification mechanism has been on improving its ability to cover a wider range of problems more accurately, while the effectiveness of verification is left to the underlying theorem provers. Our work attempts a novel approach, where the focus is on designing good specification mechanisms which can achieve both better expressiveness and better verifiability. Moreover, we shall also highlight a unified specification mechanism that can be used for both verification and inference. Our framework allows preconditions and postconditions to be selectively inferred via a set of uninterpreted relations which are computed using bi-abduction, and modularly synthesized to support concise specification for program code.