4 ms·
Abstract copied from the PDF: We present Nagini, an automated, modular verifier for statically-typed, concurrent Python 3 programs, built on the Viper verificat
by Klasiaster 8y ago
Abstract copied from the PDF:
We present Nagini, an automated, modular verifier for statically-typed, concurrent Python 3 programs, built on the Viper verification infrastructure. Combining established concepts with new ideas, Nagini can verify memory safety, functional properties, termination, deadlock freedom, and input/output behavior. Our experiments show that Nagini is able to verify non-trivial properties of real-world Python code.
- rcthompson 8y agoWhat exactly does verifying memory safety mean in Python? What memory-unsafe operations does Python allow?
- UncleEntity 8y agoI think (maybe) they mean something like: x = Foo() thread1.do_something_to_foo(x) thread2.do_something_to_foo(x) wait_on_threads(thread1, thread2) # however that works in python? do_something_to_modified_foo(x)
- rcthompson 8y agoWouldn't that be thread safety? I thought memory safety was things like preventing access to uninitialized or freed memory. As far as I know there's no way to do such things in pure Python.
- marcoeilers 8y agoWe use the term "memory safety" very broadly; what we meant was the absence of runtime errors (e.g., out-of-bounds list accesses), uncaught exceptions, concurrent modification, basically anything that would lead the program to crash. Those aren't memory unsafe in the original sense of the word in Python, but they still crash the program. Additionally, we prove the absence of data races between threads.