Why Us? >>

  • - Open Access
  • - Peer-reviewed
  • - Rapid publication
  • - Lifetime hosting
  • - Free indexing service
  • - Free promotion service
  • - More citations
  • - Search engine friendly

Free SCIRP Newsletters>>

Add your e-mail address to receive free newsletters from SCIRP.


Contact Us >>

WhatsApp  +86 18163351462(WhatsApp)
Paper Publishing WeChat
Book Publishing WeChat
(or Email:book@scirp.org)

Article citations


O. Hasan and S. Tahar, “Verification of Probabilistic Properties in the HOL Theorem Prover,” Integrated Formal Methods, Springer, Berlin, 2007, pp. 333-352.

has been cited by the following article:

  • TITLE: LR(K) Parser Construction Using Bottom-up Formal Analysis

    AUTHORS: Nazir Ahmad Zafar

    KEYWORDS: Compiler Construction; LR(K) Parser; Context-Free Grammar; Z Specification; Correctness; Verification

    JOURNAL NAME: Journal of Software Engineering and Applications, Vol.5 No.1, December 31, 2011

    ABSTRACT: Design and construction of an error-free compiler is a difficult and challenging process. The main functionality of a compiler is to translate a source code to an executable machine code correctly and efficiently. In formal verification of software, semantics of a language has more meanings than the syntax. It means source program verification does not give guarantee the generated code is correct. This is because the compiler may lead to an incorrect target program due to bugs in itself. It means verification of a compiler is much more important than verification of a source program. In this paper, we present a new approach by linking context-free grammar and Z notation to construct LR(K) parser. This has several advantages because correctness of the compiler depends on describing rules that must be written in formal languages. First, we have defined grammar then language derivation procedure is given using right-most derivations. Verification of a given language is done by recursive procedures based on the words. Ambiguity of a language is checked and verified. The specification is analyzed and validated using Z/Eves tool. Formal proofs are presented using powerful techniques of reduction and rewriting available in Z/Eves.