Validating the PSL/Sugar semantics using automated reasoning

DOI10.1007/S00165-003-0014-5zbMATH Open1093.68603OpenAlexW2081042767MaRDI QIDQ706502FDOQ706502

Authors: Michael J. C. Gordon 

Publication date: 8 February 2005

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-003-0014-5

Recommendations

• Executing the formal semantics of the Accellera property specification language by mechanised theorem proving
• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 1796144
• From Church and Prior to PSL
• From Monadic Logic to PSL

zbMATH Keywords

HOLModel checkingSemanticsTheorem provingAccelleraFormal verificationHigher-order logicProperty languagePSLSugar

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Cited In (5)

• From Church and Prior to PSL
• Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
• Theorem Proving in Higher Order Logics
• Functional specification of hardware via temporal logic
• Executing the formal semantics of the Accellera property specification language by mechanised theorem proving

Uses Software

• FoCs
• HOL

This page was built for publication: Validating the PSL/Sugar semantics using automated reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q706502)