Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Effect Analysis for Programs with Callbacks
 
Loading...
Thumbnail Image
conference paper

Effect Analysis for Programs with Callbacks

Kneuss, Etienne  
•
Kuncak, Viktor  
•
Suter, Philippe  
2013
5th International Conference, VSTTE 2013
Verified Software: Theories, Tools, Experiments

We introduce a precise interprocedural effect analysis for programs with mutable state, dynamic object allocation, and dynamic dispatch. Our analysis is precise even in the presence of dynamic dispatch where the context-insensitive estimate on the number of targets is very large. This feature makes our analysis appropriate for programs that manipulate first-class functions (callbacks). We present a framework in which programs are enriched with special effect statements, and define the semantics of both program and effect statements as relations on states. Our framework defines a program composition operator that is sound with respect to relation composition. Computing the summary of a procedure then consists of composing all its program statements to produce a single effect statement. We propose a strategy for applying the composition operator in a way that balances precision and efficiency. We instantiate this framework with a domain for tracking read and write effects, where relations on program states are abstracted as graphs. We implemented the analysis as a plugin for the Scala compiler. We analyzed the Scala standard library containing 58000 methods and classified them into several categories according to their effects. Our analysis proves that over one half of all methods are pure, identifies a number of conditionally pure methods, and computes summary graphs and regular expressions describing the side effects of non-pure methods.

  • Details
  • Metrics
Type
conference paper
DOI
10.1007/978-3-642-54108-7_3
Author(s)
Kneuss, Etienne  
•
Kuncak, Viktor  
•
Suter, Philippe  
Date Issued

2013

Publisher

Springer Berlin Heidelberg

Published in
5th International Conference, VSTTE 2013
ISBN of the book

978-3-642-54108-7

Series title/Series vol.

Lecture Notes in Computer Science; 8164

Start page

48

End page

67

Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LARA  
Event nameEvent placeEvent date
Verified Software: Theories, Tools, Experiments

Menlo Park, CA, USA

2013

Available on Infoscience
April 25, 2014
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/102948
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés