ETH Logo

Seminar: Research Topics in Software Engineering

Bertrand Meyer, Spring 2013

General

News

22.2.2013 — Tutors for each paper have been added to the lecture schedule below. Please contact them if e.g. you have some difficulty with your paper, need some feedback on slides.

20.2.2013 — Thanks for filling in the Doodle poll! We have assigned papers and presentation slots - please see below and contact the teaching assistants ASAP if there are any problems (e.g. unable to attend assigned slot).

18.1.2013 — The initial version of this page is up.

Course description

This seminar is an opportunity to become familiar with current research in software engineering and more generally with the methods and challenges of scientific research. Each student will be asked to study some papers from the recent software engineering literature and review them. This is in exercise in critical review and analysis.

Conditions for getting the credit points:

The theme selected for the 2013 session of the seminar is "Verification of Contract-Equipped Programs". This is a highly active research field on which many papers have been published recently.

Proposed papers

Clicking on the title of a paper will take you either the full text in PDF format, or the publisher's website where you should be able to download a copy (provided you are logged into the ETH network). If you are struggling to find a copy of a paper, please contact one of the teaching assistants.

  1. Views: compositional reasoning for concurrent programs
    T. Dinsdale-Young, L. Birkedal, P. Gardner, M. Parkinson, and H. Yang
    In Proc. POPL 2013. ACM, 2013.

  2. Automated error diagnosis using abductive inference
    I. Dillig, T. Dillig, and A. Aiken
    In Proc. PLDI 2012. ACM, 2012.

  3. Automating induction with an SMT solver
    K.R.M. Leino
    In Proc. VMCAI 2012, LNCS 7148. Springer, 2012.

  4. Object Ownership in Program Verification (Aliasing in Object-Oriented Programming)
    W. Dietl and P. Müller
    To appear. 2012.

  5. Simplifying Loop Invariant Generation Using Splitter Predicates
    R. Sharma, I. Dillig, T. Dillig, and A. Aiken
    In Proc. CAV 2011, LNCS 6806. Springer 2011.

  6. Verification of semantic commutativity conditions and inverse operations on linked data structures
    D. Kim and M. Rinard
    In Proc. PLDI 2011. ACM 2011.

  7. Automated Fixing of Programs with Contracts
    Y. Wei, Y. Pei, C.A. Furia, L.S. Silva, S. Buchholz, B. Meyer and A. Zeller
    In Proc. ISSTA 2010. ACM, 2010.

  8. Complete functional synthesis
    V. Kuncak, M. Mayer, R. Piskac, and P. Suter
    In Proc. PLDI 2010. ACM, 2010.

  9. Dafny: An Automatic Program Verifier for Functional Correctness
    K.R.M. Leino
    In Proc. LPAR 2010, LNCS 6355. Springer, 2010.

  10. Local Verification of Global Invariants in Concurrent Programs
    E. Cohen, M. Moskal, W. Schulte, and S. Tobies
    In Proc. CAV 2010, LNCS 6174. Springer, 2010.

  11. VCC: A Practical System for Verifying Concurrent C
    E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies
    In Proc. TPHOLs 2009, LNCS 5674. Springer, 2009.

  12. Deny-Guarantee Reasoning
    M. Dodds, X. Feng, M.J. Parkinson and V. Vafeiadis
    In Proc. ESOP 2009, LNCS 5502. Springer, 2009.

  13. A basis for verifying multi-threaded programs
    K.R.M. Leino and P. Müller
    In Proc. ESOP 2009, LNCS 5502. Springer, 2009.

  14. Programs that test themselves
    B. Meyer, A. Fiva, I. Ciupa, A. Leitner, Y. Wei, and E. Stapf
    IEEE Computer 42(9). IEEE, 2009.

  15. Using the Spec# language, methodology, and tools to write bug-free programs
    K.R.M. Leino and Peter Mülller
    LASER Summer School 2007/2008, LNCS 6029. Springer, 2009.

  16. Bounded Verification of Voting Software
    G. Dennis, K. Yessenov, and D. Jackson
    In Proc. VSTTE 2008, LNCS 5295. Springer, 2008.

  17. Secret Ninja Formal Methods
    J.R. Kiniry and D.M. Zimmerman
    In Proc. FM 2008, LNCS 5014. Springer, 2008

  18. Separation logic, abstraction and inheritance
    M.J. Parkinson and G.M. Bierman
    In Proc. POPL 2008. ACM, 2008.

  19. jStar: Towards practical verification for Java
    D. Distefano and M.J. Parkinson
    In Proc. OOPSLA 2008. ACM, 2008.

  20. Practical reasoning about invocations and implementations of pure methods
    Á. Darvas and K.R.M. Leino
    In Proc. FASE 2007, LNCS 4422. Springer, 2007.

  21. A Marriage of Rely/Guarantee and Separation Logic
    V. Vafeiadis and M. Parkinson
    In Proc. CONCUR 2007, LNCS 4703. Springer, 2007.

  22. A Logic for Bytecode
    F.Y. Bannwart and P. Müller
    In Proc. BYTECODE 2005, ENTCS 141. Elsevier, 2005.

  23. Boogie: A Modular Reusable Verifier for Object-Oriented Programs
    M. Barnett, B.E. Chang, R. DeLine, B. Jacobs, K.R.M. Leino
    In Proc. FMCO 2005, LNCS 4111. Springer, 2005.

  24. An overview of JML tools and applications
    L. Burdy, Y. Cheon, D.R. Cok, M.D. Ernst, J.R. Kiniry, G.T. Leavens, K.R.M. Leino, and E. Poll
    International Journal on Software Tools for Technology Transfer, Volume 7 Issue 3. Springer, 2005.

  25. Verification of object-oriented programs with invariants
    M. Barnett, R. DeLine, M. Fähndrich, K.R.M. Leino, and W. Schulte
    Journal of Object Technology, Vol. 3, No. 6. 2004.

  26. Friends Need a Bit More: Maintaining Invariants Over Shared State
    M. Barnett, D.A. Naumann
    In Proc. MPC 2004, LNCS 3125. Springer, 2004.

  27. Jass — Java with Assertions
    D. Bartetzko, C. Fischer, M. Möller, and H. Wehrheim
    In Proc. RV 2001, ENTCS Vol. 55, Issue 2. Elsevier, 2001.

  28. A Programming Logic for Sequential Java
    A. Poetzsch-Heffter and P. Müller
    In Proc. ESOP 1999, LNCS 1576. Springer, 1999.

  29. Using Dynamic Analysis to Discover Polynomial and Array Invariants.
    ThanhVu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest: International Conference on Software Engineering (ICSE) 2012: 683-693

  30. A Data Driven Approach for Algebraic Loop Invariants.
    R. Sharma, S. Gupta, B. Hariharan, A. Aiken, P. Liang and A. V. Nori.
    In Proceedings of the European Symposium on Programming, March 2013.

  31. DySy: Dynamic symbolic execution for invariant inference.
    C. Csallner, N. Tillmann, and Y. Smaragdakis.
    In ICSE, pages 281-290, 2008.

Lecture

When and where

Day Time Location
Monday 8:30-10:00 RZ F 21

Lecture schedule

Below you will find the schedule of paper presentations, as well as (in brackets) the tutors for each paper. Please contact your tutor e.g. if you are having difficulty with your assigned paper, or would like some feedback on some slides.

Date Presenter(s)   Paper (Tutor) Slides
18.2.2013 Bertrand Meyer
Julian Tschannen		 (1) Introduction;
(2) Example seminar: "Automatic Verification of Advanced Object-Oriented Features: The AutoProof Approach"		 —
slides
25.2.2013 Bertrand Meyer How to give a technical presentation slides
 4.3.2013 T. Martiel
A.S. Al-Sibahi		 Paper #18 (S. van Staden)
Paper #1 (S. van Staden)		 slides
slides
11.3.2013 I. Steinmann
T. Hartmann		 Paper #24 (M. Nordio)
Paper #16 (H-C. Estler)		 slides
slides
18.3.2013 E. Rudel
R. Fuchs		 Paper #17 (M. Nordio)
Paper #5 (C. Poskitt)		 slides
slides
25.3.2013 C. Zeller
R. Schmocker
L. Baesso		 Paper #7 (Y. Pei)
Paper #4 (J. Tschannen)
Paper #23 (C. Poskitt)		 slides
slides
slides
 1.4.2013 No seminar (Easter holiday)
 8.4.2013 No seminar (cancelled)
15.4.2013 P. Spettel
G. Singh
M. Hoffmann		 Paper #9 (N. Polikarpova)
Paper #29 (A. Kolesnichenko)
Paper #22 (C. Poskitt)		 slides
slides
slides
22.4.2013 M. Lanter
V. Dancheva
F. Froese		 Paper #13 (M. Nordio)
Paper #30 (J. Tschannen)
Paper #27 (C. Poskitt)		 slides
slides
slides
29.4.2013 P. Antonucci
C. Papastergiou		 Paper #15 (M. Nordio)
Paper #14 (Y. Pei)		 slides
slides
 6.5.2013 P. Bielik Paper #11 (C. Poskitt) slides
13.5.2013 M. Egg
S. Heiniger
F. Besser		 Paper #31 (C.A. Furia)
Paper #2 (C.A. Furia)
Paper #10 (N. Polikarpova)		 slides
slides
slides
20.5.2013 No seminar (Whitsuntide)
27.5.2013 P. Zimmermann
Benjamin Morandi		 Paper #20 (C. Poskitt)
Prototyping a concurrency model		 slides
—

Assistants