scientific article; zbMATH DE number 1796150

zbMath0991.68639MaRDI QIDQ4551174

K. L. McMillan, Ranjit Jhala

Publication date: 4 September 2002

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2102/21020396

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Computing methodologies and applications (68U99) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07)

Related Items

Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics, Algebraic models of correctness for abstract pipelines., Efficient Information-Flow Verification Under Speculative Execution, Local proofs for global safety properties

Uses Software

• ACL2
• PVS