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

DOI10.1007/S10703-011-0134-0zbMATH Open1247.68162OpenAlexW2034592364MaRDI QIDQ453526FDOQ453526

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

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

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)

Cites Work

• Automatic generation of invariants and intermediate assertions
• An axiomatic basis for computer programming
• SAT-Based Model Checking without Unrolling
• Verifying deadlock-freedom of communication fabrics
• Title not available (Why is that?)

Cited In (2)

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

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)