Validating the PSL/Sugar semantics using automated reasoning

DOI10.1007/S00165-003-0014-5MaRDI QIDQ706502zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(5)

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

Describes a project that uses

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)