• DocumentCode
    1554839
  • Title

    Mechanizing CSP trace theory in higher order logic

  • Author

    Camilleri, Albert John

  • Author_Institution
    Hewlett-Packard Lab., Stoke Gifford, UK
  • Volume
    16
  • Issue
    9
  • fYear
    1990
  • fDate
    9/1/1990 12:00:00 AM
  • Firstpage
    993
  • Lastpage
    1004
  • Abstract
    How a mechanized tool for reasoning about CSP (communicating sequential processes) can be developed by customizing an existing general-purpose theorem prover based on higher-order logic is described. How the trace semantics of CSP operators can be mechanized in higher-order logic is investigated, and how the laws associated with these operators can be proved from their semantic definitions is shown. The resulting system is one in which natural-deduction style proofs can be conducted using the standard CSP laws
  • Keywords
    formal logic; formal specification; theorem proving; communicating sequential processes; general-purpose theorem prover; higher order logic; mechanising CSP trace theory; Algebra; Concurrent computing; Formal verification; Helium; Humans; Information systems; Logic functions; System recovery;
  • fLanguage
    English
  • Journal_Title
    Software Engineering, IEEE Transactions on
  • Publisher
    ieee
  • ISSN
    0098-5589
  • Type

    jour

  • DOI
    10.1109/32.58786
  • Filename
    58786
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1554839