Formal verification of the VAMP floating point unit (Q816201): Difference between revisions

@@ Property / describes a project that uses @@
+ACL2
@@ Property / describes a project that uses: ACL2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10703-005-1613-y
+Normal rank
@@ Property / OpenAlex ID @@
+W2157753532
@@ Property / OpenAlex ID: W2157753532 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754053
@@ Property / cites work: Q2754053 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4787242
@@ Property / cites work: Q4787242 / rank @@
+Normal rank
@@ Property / cites work @@
+Correct Hardware Design and Verification Methods
@@ Property / cites work: Correct Hardware Design and Verification Methods / rank @@
+Normal rank
@@ Property / cites work @@
+Q4790659
@@ Property / cites work: Q4790659 / rank @@
+Normal rank
@@ Property / cites work @@
+On the design of IEEE compliant floating point units
+Normal rank
@@ Property / cites work @@
+Q4860810
@@ Property / cites work: Q4860810 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4804904
@@ Property / cites work: Q4804904 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4787230
@@ Property / cites work: Q4787230 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4494691
@@ Property / cites work: Q4494691 / rank @@
+Normal rank
@@ Property / cites work @@
+A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7<sup>™</sup> Processor
+Normal rank
@@ Property / cites work @@
+A proof of the nonrestoring division algorithm and its implementation on an ALU
+Normal rank