PhDCourses/Analysis, Test and Verification

From Models Wiki
(Difference between revisions)
Jump to: navigation, search
(CURRICULUM)
 
(8 intermediate revisions by 2 users not shown)
Line 3: Line 3:
  
  
Here you can find information about the PhD course for Spring semester 2014.
+
Here you can find information about the PhD course for Spring semester 2015.
  
  
Line 15: Line 15:
 
'''Registration''': adim@itu.dk (Aleksandar Dimovski)
 
'''Registration''': adim@itu.dk (Aleksandar Dimovski)
  
'''Format''': Research seminar. Presentation and discussion 90 minutes a session, 15 sessions.  
+
'''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.
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.
  
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.
  
'''Assessment''': Presentation of at least two papers 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 Wednesday from 09:30 AM till 11:00 AM in 4A05 or 3A01 starting from 5th February.
+
'''Meetings''': Our weekly meetings are every Monday from 12:30 till 13:55 starting from 13th April.
  
 
'''Meeting room''':
 
'''Meeting room''':
             4A05 (29.01, 05.02, 02.04, 30.04, 14.05, 21.05, 28.05)
+
             4A05 (13.04, 20.04, 27.04, 04.05, 11.05, 18.05, 01.06, 08.06, 15.06, 22.06)
 
+
            3A01 (12.02, 19.02, 26.02, 12.03, 19.03, 26.03, 09.04, 23.04, 07.05)
+
  
 
== '''CURRICULUM''' ==
 
== '''CURRICULUM''' ==
  
* '''Background (Software Product Lines)''' [1 session] - (5.02, Stefan)
+
* '''Background (Software Product Lines)''' [1 session] - ('''5.02''', Stefan)
  
 
"On Program Families" by Dijkstra from EWD249.pdf (notes on structured programming)
 
"On Program Families" by Dijkstra from EWD249.pdf (notes on structured programming)
Line 41: Line 40:
 
Pamel Zave's FAQ: http://www2.research.att.com/~pamela/faq.html
 
Pamel Zave's FAQ: http://www2.research.att.com/~pamela/faq.html
  
* '''Feature Interactions''' [1 session] (12.02, Tijs)
+
* '''Feature Interactions''' [1 session] ('''12.02''', Tijs)
  
 
[http://www.dcs.gla.ac.uk/~muffy/papers/calder-kolberg-magill-reiff.pdf Feature Interaction: A Critical Review and Considered Forecast]. Muffy Calder. Mario Kolberg. Evan H. Magill. Stephan Reiff-Marganiec [only read sections 1--6]
 
[http://www.dcs.gla.ac.uk/~muffy/papers/calder-kolberg-magill-reiff.pdf 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)
+
* '''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)
+
Rao (19-02-2014): [http://link.springer.com/article/10.1007%2Fs10515-005-2643-9 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, 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)
Line 53: Line 52:
 
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)
 
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)
+
* '''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
 
Paul Gazzillo, Robert Grimm: SuperC: parsing all of C by taming the preprocessor. PLDI 2012: 323-334
Line 61: Line 60:
 
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
 
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'', ?)
+
* '''Type Checking''' [2 sessions] (1st session: '''26.03''', Aleksandar) (2nd session: '''02.04''', Stefan)
 
+
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
 
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, ?)
+
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.
 
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.
Line 75: Line 74:
 
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)
 
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, ?)
+
* '''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
 
Thomas Thüm, Ina Schaefer, Martin Hentschel, Sven Apel: Family-based deductive verification of software product lines. GPCE 2012: 11-20
Line 83: Line 82:
 
Benjamin Delaware, William R. Cook, Don S. Batory: Product lines of theorems. OOPSLA 2011: 595-608
 
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, ?)
+
* '''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.  
 
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.  
Line 89: Line 88:
 
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
 
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, ?)
+
* '''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.
 
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.

Latest revision as of 11:16, 23 March 2015

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.


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: adim@itu.dk (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.

Meeting room:

           4A05 (13.04, 20.04, 27.04, 04.05, 11.05, 18.05, 01.06, 08.06, 15.06, 22.06)

CURRICULUM

  • 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.

Personal tools
Namespaces
Variants
Actions
Navigation
Toolbox