NDLI: Why does Astrée scale up?

Content Provider	Springer Nature Link
Author	Cousot, Patrick Cousot, Radhia Feret, Jérôme Mauborgne, Laurent Miné, Antoine Rival, Xavier
Copyright Year	2009
Abstract	Astrée was the first static analyzer able to prove automatically the total absence of runtime errors of actual industrial programs of hundreds of thousand lines. What makes Astrée such an innovative tool is its scalability, while retaining the required precision, when it is used to analyze a specific class of programs: that of reactive control-command software. In this paper, we discuss the important choice of algorithms and data-structures we made to achieve this goal. However, what really made this task possible was the ability to also take semantic decisions, without compromising soundness, thanks to the abstract interpretation framework. We discuss the way the precision of the semantics was tuned in Astrée in order to scale up, the differences with some more academic approaches and some of the dead-ends we explored. In particular, we show a development process which was not specific to the particular usage Astrée was built for, hoping that it might prove helpful in building other scalable static analyzers.
Starting Page	229
Ending Page	264
Page Count	36
File Format	PDF
ISSN	09259856
Journal	Formal Methods in System Design
Volume Number	35
Issue Number	3
e-ISSN	15728102
Language	English
Publisher	Springer US
Publisher Date	2009-11-11
Publisher Place	Boston
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Software Engineering/Programming and Operating Systems Computer-Aided Engineering (CAD, CAE) and Design Electrical Engineering Circuits and Systems
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Software Hardware and Architecture

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

The CAV award

The 2008 CAV Award citation

2009 CAV award announcement

Foreword: Special issue on numerical software verification

Reactive Modules

Hazard Algebras

Before and after vacuity

Special issue: 2nd World Congress on Formal Methods

From liveness to promptness

Why does Astrée scale up?

Similar Documents

The CAV award

The 2008 CAV Award citation

2009 CAV award announcement

Foreword: Special issue on numerical software verification

Reactive Modules

Hazard Algebras

Before and after vacuity

Special issue: 2nd World Congress on Formal Methods

From liveness to promptness

Why does Astrée scale up?