Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics

DOI10.1007/S10703-011-0134-0MaRDI QIDQ453526zbMATHOpenAlexFDO

Authors Satrajit Chatterjee, Michael Kishinevsky

Publication date 27 September 2012

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-011-0134-0

zbMATH Keywords

model checkinginductionnetwork-on-chipsafety verificationformal verificationproofcommunication fabricshigh-level modelsinvariant synthesismicroarchitecturesynchronous model

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Network design and communication in computer systems (68M10)

Recommendations

• Verifying deadlock-freedom of communication fabrics
• scientific article; zbMATH DE number 1796150
• Formal modeling and verification of microprocessors
• scientific article; zbMATH DE number 2102696
• scientific article; zbMATH DE number 1701763

Cites work

• scientific article; zbMATH DE number 1796150 (Why is no real title available?)
• An axiomatic basis for computer programming
• Automatic generation of invariants and intermediate assertions
• SAT-Based Model Checking without Unrolling
• Verifying deadlock-freedom of communication fabrics

Cited in

(2)

• Verifying deadlock-freedom of communication fabrics
• A formalisation of \textsc{xMAS}

This page was built for publication: Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics

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