I phrased my question about time and space badly. I was interested in proving the time and space behavior of the software “under scrutiny”, not in the resource consumption of the verification systems themsvelves.
It would be nice to be able to prove things like “this program will never allocate more than X memory”, or “this service will always respond to any given request within Y time”.
I phrased my question about time and space badly. I was interested in proving the time and space behavior of the software “under scrutiny”, not in the resource consumption of the verification systems themsvelves.
LOL!
I know a few people who have worked in this area. Jan Hoffman and Peng Gong have worked on automatically inferring complexity. Tristan Knoth has gone the other way, including resource bounds in specs for program synthesis. There’s a guy who did an MIT Ph. D. on building an operating system in Go, and as part of it needed an analyzer that can upper-bound the memory consumption of a system call. I met someone at CU Boulder working under Bor-Yuh Evan Chang who was also doing static analysis of memory usage, but I forget whom.
So, those are some things that were going on. About all of these are 5+ years old, and I have no more recent updates. I’ve gone to one of Peng’s talks and read none of these papers.
I phrased my question about time and space badly. I was interested in proving the time and space behavior of the software “under scrutiny”, not in the resource consumption of the verification systems themsvelves.
It would be nice to be able to prove things like “this program will never allocate more than X memory”, or “this service will always respond to any given request within Y time”.
LOL!
I know a few people who have worked in this area. Jan Hoffman and Peng Gong have worked on automatically inferring complexity. Tristan Knoth has gone the other way, including resource bounds in specs for program synthesis. There’s a guy who did an MIT Ph. D. on building an operating system in Go, and as part of it needed an analyzer that can upper-bound the memory consumption of a system call. I met someone at CU Boulder working under Bor-Yuh Evan Chang who was also doing static analysis of memory usage, but I forget whom.
So, those are some things that were going on. About all of these are 5+ years old, and I have no more recent updates. I’ve gone to one of Peng’s talks and read none of these papers.