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.
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.