- 【Updated on May 12, 2025】 Integration of CiNii Dissertations and CiNii Books into CiNii Research
- Trial version of CiNii Research Knowledge Graph Search feature is available on CiNii Labs
- 【Updated on June 30, 2025】Suspension and deletion of data provided by Nikkei BP
- Regarding the recording of “Research Data” and “Evidence Data”
Termination proofs for systems code
-
- Byron Cook
- Microsoft Research
-
- Andreas Podelski
- Max-Planck-Institut für Informatik
-
- Andrey Rybalchenko
- Max-Planck-Institut für Informatik and EPFL
Search this article
Description
<jats:p>Program termination is central to the process of ensuring that systems code can always react. We describe a new program termination prover that performs a path-sensitive and context-sensitive program analysis and provides capacity for large program fragments (i.e. more than 20,000 lines of code) together with support for programming language features such as arbitrarily nested loops, pointers, function-pointers, side-effects, etc.We also present experimental results on device driver dispatch routines from theWindows operating system. The most distinguishing aspect of our tool is how it shifts the balance between the two tasks of constructing and respectively checking the termination argument. Checking becomes the hard step. In this paper we show how we solve the corresponding challenge of checking with binary reachability analysis.</jats:p>
Journal
-
- ACM SIGPLAN Notices
-
ACM SIGPLAN Notices 41 (6), 415-426, 2006-06-11
Association for Computing Machinery (ACM)
- Tweet
Details 詳細情報について
-
- CRID
- 1363670319006609792
-
- ISSN
- 15581160
- 03621340
-
- Data Source
-
- Crossref