PhDCourses/Analysis, Test and Verification
PhD Course on "Analysis, Test and Verification in The Presence of Variability"
Here you can find information about the PhD course for Spring semester 2015.
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: email@example.com (Aleksandar Dimovski)
Format: Research seminar. Presentation and discussion 90 minutes a session, 10 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 one paper and active participation throughout the seminar is required for passing the course.
Grading: PASS / FAIL based on fulfilling the above assessment condition.
Meetings: Our weekly meetings are every Monday from 12:30 till 13:55 starting from 13th April.
4A05 (13.04, 20.04, 27.04, 04.05, 11.05, 18.05, 01.06, 08.06, 15.06, 22.06)
- 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: http://www2.research.att.com/~pamela/faq.html
- 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)
Rao (19-02-2014): Media: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, Aleksandar) (2nd session: 02.04, Stefan)
Sheng Chen, Martin Erwig, Eric Walkingshaw: An error-tolerant type system for variational lambda calculus. ICFP 2012: 29-40
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)
- Static Analysis and Abstract Interpretation [1 sessions] (1st session: 09.04, Claus)
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: 30.04, Alex) (2nd session: 14.05, Tijs)
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, Iago)
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, Rao)
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.