search

HalosGhost / enlighten

An expressive, sysfs-based backlight brightness manager
GNU General Public License v3.0
18 stars 2 forks source link

Formal Methods? #20

Closed HalosGhost closed 5 years ago

HalosGhost commented 5 years ago

Many parts of enlighten (most of it, if not all of it, actually), could resonably be specified and verified using frama-c. Aside from being a fun opportunity to get more familiar with practical formal methods, it would be fun to be one of the only backlight utilities out there (the only?) to be formally verified.

The obvious negatives are the added dependency for the test-suite (which would run the current system tests as well as the acsl verification), higher bar for entry for contributions, along with the extra work of the verification itself, and any refactoring the verification necessitates.

This is not a cut-and-dry choice as the cons are non-trivial. I shall continue to think on this. Thoughts are welcome.

HalosGhost commented 5 years ago

Nope. I'm going to try to do this as much as possible.