Termination proofs for systems code
By Byron Cook, Andreas Podelski, Andrey Rybalchenko. ACM-SIGPLAN Symposium on Programming Language Design and Implementation, 2006
422 citations recorded by the source corpus.
Subfields: Artificial Intelligence, Software, Signal Processing
View Paper: https://www.semanticscholar.org/paper/3d85222ab5290c80b32e995a04b7047d8873f36d
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Sriram K. Rajamani
- Thomas Ball
- Rupak Majumdar
- Ranjit Jhala
- Byron Cook
- Shlomo Zilberstein
- Vladimir Levin
- Siddharth Srivastava
In Software
- Rupak Majumdar
- Ranjit Jhala
- Sriram K. Rajamani
- Thomas Ball
- Sumit Gulwani
- Byron Cook
- Vladimir Levin
- Siddharth Srivastava
In Signal Processing
- Ranjit Jhala
- Rupak Majumdar
- Sumit Gulwani
- Siddharth Srivastava
- Shlomo Zilberstein
- Neil Immerman
- Trishul M. Chilimbi
- Krishna K. Mehra
Citations in the corpus
- SPEED: precise and efficient static estimation of program computational complexity (2009, methodology): “[6, 1] have successfully applied the fundamental result of [27] on disjunctively well-founded relations to prove termination of loops in real systems code.”
- Software model checking (2009, positive): “These observations from the basis of Armc and Terminator, which prove termination for C programs [Cook et al. 2006].”
- Thorough static analysis of device drivers (2006, background): “See [10, 21, 22] for recent work in this area.”
- A new representation and associated algorithms for generalized planning (2011, methodology): “Terminator’s use of linear inequalities for representing changes caused by program statements are also suitable for representing the changes in role counts.”