English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 Local TagsRelease HistoryDetailsSummary
  Termination Proofs for Systems Code

Cook, B., Podelski, A., & Rybalchenko, A. (2006). Termination Proofs for Systems Code. In PLDI 2006 : Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation (pp. 415-426). New York, USA: ACM.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2416-9 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2417-7
Genre: Conference Paper

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Cook, Byron, Author
Podelski, Andreas1, Author           
Rybalchenko, Andrey1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: 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.

Details

show
hide
Language(s): eng - English
 Dates: 2007-04-272006
 Publication Status: Issued
 Pages: -
 Publishing info: New York, USA : ACM
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 314429
Other: Local-ID: C1256104005ECAFC-88C906F53622F174C125729D00531880-PodelskiRybalchenkoCook2006
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: Ottawa, Ontario, Canada
Start-/End Date: 2006-06-10

Legal Case

show

Project information

show

Source 1

show
hide
Title: PLDI 2006 : Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation
Source Genre: Proceedings
 Creator(s):
Affiliations:
Publ. Info: New York, USA : ACM
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 415 - 426 Identifier: ISBN: 1-59593-320-4

Source 2

show
hide
Title: ACM SIGPLAN Notices
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: - Identifier: -