IA072 Seminar on Concurrency

Programme

  • 25. 2. 2011 - Arrangements
  • 4. 3. 2011 - Marek Trtík - Patrick Cousot and Radhia Cousot: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL 1977. (part I)
  • 11. 3. 2011 - Marek Trtík - Patrick Cousot and Radhia Cousot: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL 1977. (part II)
  • 18. 3. 2011 - cancelled (spring holidays)
  • 25. 3. 2011 - Martin Milata - Seth Hallem, Benjamin Chelf, Yichen Xie, and Dawson Engler: A System and Language for Building System-Specific Static Analyses, PLDI 2002.
  • 1. 4. 2011 - Jirka Slabý - STANSE
  • 8. 4. 2011 - cancelled (no speaker found)
  • 15. 4. 2011 - Pavel Čadek - M. Weiser: Program Slicing, IEEE Transactions on Software Engineering, 1984.
  • 22. 4. 2011 - cancelled
  • 29. 4. 2011 - Fanda Blahoudek - C. Calcagno, D. Distefano, P. O’Hearn, and H. Yang: Compositional Shape Analysis by means of Bi-Abduction, POPL 2009. (part I)
  • 6. 5. 2011 - Jiří Šimša - Systematic Testing of Distributed and Multi-Threaded Systems

    To build confidence in correct operation of distributed and multi-threaded programs, software engineers inspect code and run tests. However, the concurrent nature of such programs greatly complicates these tasks. In testing, this problem is commonly addressed by chance-based methods, which execute a long sequence of tests hoping that eventually all possible behaviors (and faults) of a program will be encountered. In the first part of this talk we highlight the design and implementation of an alternative to chance-based methods called "systematic testing". This approach repeatedly executes a test while controlling the order in which concurrent events in the program execute. This mechanism is used to guide repeated execution of the same test down different paths and, by doing so, enumerate different behaviors of the program. This approach has been implemented as part of the dBug tool and has been successfully used to automatically detect concurrency errors in unmodified binaries of distributed and multi-threaded programs. The second part of the talk discusses some of the case studies carried out with dBug, including a recent project on systematic testing of a flexible storage system Stasis.

 

Other papers to present:

Předchozí
Následující