PhDCourses/Analysis, Test and Verification

From Models Wiki
Revision as of 13:42, 11 February 2014 by Adim (Talk | contribs)
Jump to: navigation, search

PhD Course on "Analysis, Test and Verification in The Presence of Variability"

Here you can find information about the PhD course for Spring semester 2014.

Various Information

Teachers: Andrzej Wasowski. Claus Brabrand. Aleksandar Dimovski.

Participants: Andrzej Wasowski. Claus Brabrand. Aleksandar Dimovski. Raghava Rao Mukkamala. Stefan Stanciulescu. Iago Abal Rivas. Alexandru Florin Iosif-Lazăr. Tijs Slaats.

Registration: (Aleksandar Dimovski)

Format: Research seminar. Presentation and discussion 90 minutes a session, 15 sessions. The course participants are supposed to read the paper before the scheduled discussion slots.

Participants take turns presenting the material. Everybody is expected to actively participate in the discussions.

Assessment: Presentation of at least two papers and active participation throughout the seminar is required for passing the course.

Meetings: Our weekly meetings are every Wednesday from 09:30 AM till 11:00 AM in 4A05 or 3A01 starting from 5th February.

Meeting room:

           4A05 (29.01, 05.02, 02.04, 30.04, 14.05, 21.05, 28.05)
           3A01 (12.02, 19.02, 26.02, 12.03, 19.03, 26.03, 09.04, 23.04, 07.05)


  • Background (Software Product Lines) [1 session] - (5.02, Stefan)

"On Program Families" by Dijkstra from EWD249.pdf (notes on structured programming)

David Lorge Parnas: On the Design and Development of Program Families. IEEE Trans. Software Eng. 2(1): 1-9 (1976)

Christian Prehofer: Feature-oriented programming: A new way of object composition. Concurrency and Computation: Practice and Experience 13(6): 465-501 (2001)

Pamel Zave's FAQ:

  • Feature Interactions [1 session] (12.02, Tijs)

Feature Interaction: A Critical Review and Considered Forecast. Muffy Calder. Mario Kolberg. Evan H. Magill. Stephan Reiff-Marganiec [only read sections 1--6]

  • Model Checking [2 sessions] (1st session: 19.02, Rao) (2nd session: 26.02, Aleksandar)

Harry C. Li, Shriram Krishnamurthi, Kathi Fisler: Modular Verification of Open Features Using Three-Valued Model Checking. Autom. Softw. Eng. 12(3): 349-382 (2005)

Andreas Classen, Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay, Jean-François Raskin: Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking. IEEE Trans. Software Eng. 39(8): 1069-1089 (2013)

Andreas Classen, Maxime Cordy, Patrick Heymans, Axel Legay, Pierre-Yves Schobbens: Model checking software product lines with SNIP. STTT 14(5): 589-612 (2012) (just this or the above)

  • Representation [2 sessions] (1st session: 12.03, Alex) (2nd session: 19.03, Iago)

Paul Gazzillo, Robert Grimm: SuperC: parsing all of C by taming the preprocessor. PLDI 2012: 323-334

Christian Kästner, Paolo G. Giarrusso, Tillmann Rendel, Sebastian Erdweg, Klaus Ostermann, Thorsten Berger: Variability-aware parsing in the presence of lexical macros and conditional compilation. OOPSLA 2011: 805-824

Martin Erwig and E. Walkingshaw. The choice calculus: A representation for software variation. ACM Trans. Softw. Eng. Methodol., 21(1):6:1–6:27, Dec. 2011

  • Type Checking [2 sessions] (1st session: 26.03, ?) (2nd session: 02.04, ?)

Christian Kästner, Sven Apel, Thomas Thüm, Gunter Saake: Type checking annotation-based product lines. ACM Trans. Softw. Eng. Methodol. 21(3): 14 (2012) (or ASE 2008)

Sheng Chen, Martin Erwig, Eric Walkingshaw: An error-tolerant type system for variational lambda calculus. ICFP 2012: 29-40

  • Static Analysis and Abstract Interpretation [3 sessions] (1st session: 09.04, ?) (2nd session: 23.04, ?) (3rd session: 30.04, ?)

Brabrand, M. Ribeiro, T. Tolêdo, J. Winther, and P. Borba. Intraprocedural dataflow analysis for software product lines. Transactions on Aspect-Oriented Software Development, 10:73–108, 2013.

Bodden, T. Tolêdo, M. Ribeiro, C. Brabrand, P. Borba, and F. Mezini. SPLLIFT - statically analyzing software product lines in minutes instead of years. In PLDI’13, 2013.

Midtgaard, J., Brabrand, C. & Wasowski, A. Systematic Derivation of Static Analyses for Software Product Lines. In 2014 ACM SIGPLAN 13th International Conference on MODULARITY. (or its extended version)

  • Deductive Verification [2 sessions] (1st session: 07.05, ?) (2nd session: 14.05, ?)

Thomas Thüm, Ina Schaefer, Martin Hentschel, Sven Apel: Family-based deductive verification of software product lines. GPCE 2012: 11-20

Reiner Hähnle, Ina Schaefer: A Liskov Principle for Delta-Oriented Programming. ISoLA (1) 2012: 32-46 (this or the above, or both in the same session)

Benjamin Delaware, William R. Cook, Don S. Batory: Product lines of theorems. OOPSLA 2011: 595-608

  • Combinatorial Interaction Testing [1 session] (1st session: 21.05, ?)

D. Richard Kuhn, Dolores R. Wallace, and Albert M. Gallo. Software fault interactions and implications for software testing. IEEE Transactions on Software Engineering, 30(6):418–421, 2004.

Myra B. Cohen, Matthew B. Dwyer, and Jiangfan Shi. Constructing interaction test suites for highly-configurable systems in the presence of constraints: A greedy approach. IEEE Transactions on Software Engineering, 34:633–650, 2008

  • Analysis Strategies [1 session] (1st session: 28.05, ?)

Thomas Thüm, Sven Apel, Christian Kästner, Martin Kuhlemann, Ina Schaefer, and Gunter Saake. Analysis Strategies for Software Product Lines. Technical Report FIN-004-2012, School of Computer Science, University of Magdeburg, Germany, April 2012.

  • Formal Feature Modeling [1 session]

David Benavides, Sergio Segura and Antonio Ruiz-Cortes. Automated Analysis of Feature Models 20 Years Later: A Literature Review. Journal Information Systems, 615-636.

Don Batory. Feature models, grammars, and propositional formulas. SPLC 2005, 7-20.

David Benavides, Pablo Trinidad, and Antonio Ruiz-Cortes. Automated Reasoning on Feature Models. CAiSE 2005, 491–503.

Personal tools