Comments

• 

  almost 2 years ago by shunghsiyu | Reply

  I've uploaded the jupyter notebook on GitHub that contains a minimal model of tnum along with tnum_add(), as well as the prove that it works.

×
Edit Comment 6455
# A First Level Header
## A Second Level Header

Use one asterisk to *emphasize*

Use two asterisks for **strong emphasis**

* Use asterisks
* for lists

This is an [example link](http://example.com/)

This is an ![example image](http://paste.opensuse.org/view/raw/68957446)

This is a user link @hans

This is a project link hw#some-cool-title
More Complex Markdown Help
Formatting Help
• Edit
• Preview
I've uploaded the [jupyter notebook on GitHub](https://gist.github.com/shunghsiyu/a63e08e6231553d1abdece4aef29f70e) that contains a minimal model of tnum along with tnum_add(), as well as the prove that it works.
 
×
Reply to shunghsiyu
I've uploaded the jupyter notebook on GitHub that contains a minimal model of tnum along with tnum_add(), as well as the prove that it works.
---
# A First Level Header
## A Second Level Header

Use one asterisk to *emphasize*

Use two asterisks for **strong emphasis**

* Use asterisks
* for lists

This is an [example link](http://example.com/)

This is an ![example image](http://paste.opensuse.org/view/raw/68957446)

This is a user link @hans

This is a project link hw#some-cool-title
More Complex Markdown Help
Formatting Help
• Edit
• Preview
 
• 

  almost 2 years ago by shunghsiyu | Reply

  The slides used for lightning talk can be found here

  While I'd like to achieve much more, I think what I've done during hack week is suffice to be called a complete project, so I'm marking this as complete

×
Edit Comment 6524
# A First Level Header
## A Second Level Header

Use one asterisk to *emphasize*

Use two asterisks for **strong emphasis**

* Use asterisks
* for lists

This is an [example link](http://example.com/)

This is an ![example image](http://paste.opensuse.org/view/raw/68957446)

This is a user link @hans

This is a project link hw#some-cool-title
More Complex Markdown Help
Formatting Help
• Edit
• Preview
The [slides used for lightning talk can be found here](https://mysuse-my.sharepoint.com/:p:/g/personal/shung-hsi_yu_suse_com/Ear265Ka3QJLgX9yFNOYpCMBaCZI021YS5_JaERmixsC-g) While I'd like to achieve much more, I think what I've done during hack week is suffice to be called a complete project, so I'm marking this as complete
 
×
Reply to shunghsiyu
The slides used for lightning talk can be found here
While I'd like to achieve much more, I think what I've done during hack week is suffice to be called a complete project, so I'm marking this as complete
---
# A First Level Header
## A Second Level Header

Use one asterisk to *emphasize*

Use two asterisks for **strong emphasis**

* Use asterisks
* for lists

This is an [example link](http://example.com/)

This is an ![example image](http://paste.opensuse.org/view/raw/68957446)

This is a user link @hans

This is a project link hw#some-cool-title
More Complex Markdown Help
Formatting Help
• Edit
• Preview
 
• 

  6 months ago by shunghsiyu | Reply

  I'm restarting this project to model check the range tracking (minimal and maximal value possible in s32/u32/u64/s64 range) done in BPF verifier.

  In addition to that I hope to unify signed and unsigned range tracking based on previously posted idea and the "Interval Analysis and Machine Arithmetic: Why Signedness Ignorance Is Bliss" paper for simpler range tracking code.

×
Edit Comment 7361
# A First Level Header
## A Second Level Header

Use one asterisk to *emphasize*

Use two asterisks for **strong emphasis**

* Use asterisks
* for lists

This is an [example link](http://example.com/)

This is an ![example image](http://paste.opensuse.org/view/raw/68957446)

This is a user link @hans

This is a project link hw#some-cool-title
More Complex Markdown Help
Formatting Help
• Edit
• Preview
I'm restarting this project to model check the range tracking (minimal and maximal value possible in s32/u32/u64/s64 range) done in BPF verifier. In addition to that I hope to unify signed and unsigned range tracking based on [previously posted idea](https://lore.kernel.org/bpf/ZTZxoDJJbX9mrQ9w@u94a/) and the ["Interval Analysis and Machine Arithmetic: Why Signedness Ignorance Is Bliss"](https://dl.acm.org/doi/abs/10.1145/2651360) paper for simpler range tracking code.
 
×
Reply to shunghsiyu
I'm restarting this project to model check the range tracking (minimal and maximal value possible in s32/u32/u64/s64 range) done in BPF verifier.
In addition to that I hope to unify signed and unsigned range tracking based on previously posted idea and the "Interval Analysis and Machine Arithmetic: Why Signedness Ignorance Is Bliss" paper for simpler range tracking code.
---
# A First Level Header
## A Second Level Header

Use one asterisk to *emphasize*

Use two asterisks for **strong emphasis**

* Use asterisks
* for lists

This is an [example link](http://example.com/)

This is an ![example image](http://paste.opensuse.org/view/raw/68957446)

This is a user link @hans

This is a project link hw#some-cool-title
More Complex Markdown Help
Formatting Help
• Edit
• Preview