English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software, invited chapter

Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., et al. (2002). Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software, invited chapter. In T. Mogensen, D. A. Schmidt, & I. H. Sudborough (Eds.), The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones (pp. 85-108). Berlin, Germany: Springer.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-30F0-5 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-30F1-3
Genre: Book Chapter

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Blanchet, Bruno1, Author           
Cousot, Patrick, Author
Cousot, Radhia, Author
Feret, Jérôme, Author
Mauborgne, Laurent2, Author           
Miné, Antoine, Author
Monniaux, David, Author
Rival, Xavier, Author
Affiliations:
1Static Analysis, MPI for Informatics, Max Planck Society, ou_1116553              
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: We report on a successful preliminary experience in the design and implementation of a special-purpose Abstract Interpretation based static program analyzer for the verification of safety critical embedded real-time software. The analyzer is both precise (zero false alarm in the considered experiment) and efficient (less than one minute of analysis for 10,000 lines of code). Even if it is based on a simple interval analysis, many features have been added to obtain the desired precision: expansion of small arrays, widening with several thresholds, loop unrolling, trace partitioning, relations between loop counters and other variables. The efficiency of the tool mainly comes from a clever representation of abstract environments based on balanced binary search trees.

Details

show
hide
Language(s): eng - English
 Dates: 2004-12-082002
 Publication Status: Issued
 Pages: -
 Publishing info: Berlin, Germany : Springer
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 520652
Other: Local-ID: C1256BDD001D715B-A7D599601D7ED3E8C1256C8E0046DD25-BlanchetCousotetal2002
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones
Source Genre: Book
 Creator(s):
Mogensen, Torben, Editor
Schmidt, David A., Editor
Sudborough, Ivan Hal, Editor
Affiliations:
-
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 85 - 108 Identifier: ISBN: 3-540-00326-6

Source 2

show
hide
Title: Lecture Notes in Computer Science
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 2566 Sequence Number: - Start / End Page: - Identifier: -