Loading...
Please wait, while we are loading the content...
Similar Documents
Validating low-level instructions for fixnums using BDDs
| Content Provider | ACM Digital Library |
|---|---|
| Author | Yasugi, Masahiro Yuasa, Shingo |
| Abstract | A fixnum is a data object used in Lisp and other programming languages for representing an integer within some fixed range; fixnum consisting of tag bits and an integer value is represented in a single machine word. Programming language systems must use or generate instruction sequences such as "check if two objects are both fixnums" and "check if the sum of two fixnums does not overflow." To obtain efficient code, tricky bit operations with low-level instructions are used. To the best of our knowledge, mechanical verification frameworks for verifying these instruction sequences have not been investigated thus far. We implemented a library for validating low-level instructions against their intended meaning in Common Lisp. We consider each bit in a machine word as a Boolean value and verify the constraints that correspond to the intended meaning using binary decision diagrams. |
| Starting Page | 11 |
| Ending Page | 20 |
| Page Count | 10 |
| File Format | |
| ISBN | 9781450304702 |
| DOI | 10.1145/1869643.1869646 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2010-10-19 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Fixnum Bdd Mechanical verification |
| Content Type | Text |
| Resource Type | Article |
