burkhart.wolff

All courses will take place at Salle Firtech, Bat. 490, 9:00 - 12:00.

The Material below is tentative !!!

• C1 10.12. [BW]: Course Primer, Introduction to Testing, A Gentle Introduction to Isabelle/HOL Exercise 1
• 17.12. : Shifted because strike and snow ...
• C2 7.1. [BW] : (Unit)-Tests based on Data Models, Exercise 2
• C3 14.1 [BW] : (Unit)-Tests based on Data Models, cont., Exercise 3
• C4 21.1. [BW] : Sequence-Tests with HOL-TestGen
• C5 28.1. [BW] : Testing Reactive Systems
• C6 4.2. [BW] : White-Box-Tests based on Symbolic Execution with HOL-TestGen
• C7 11.2. [BW] :Finite Sequence Testing with Hidden State
• C8 18.2. [BW] :IOTS-Testing and IO-Conformance

Downloads : Isabelle (Use Version 2009, not 2009-1!) , HOL-TestGen
Exam : 5.3.2009 ???
Resume due: 5.3.2009 (submit electronically to ~wolff@lri.fr !)

Bibliography:

• [1] Model-Checking oriented Program-Based Testing: Test Input Generation with Java PathFinder
• [2] Symbolic Execution oriented Program-Based Testing: JPF-SE: A Symbolic Execution Extension to Java PathFinder
• [3] Compositional Symbolic Execution oriented Program-Based Testing:Demand-Driven Compositional Symbolic Execution PEX System Description
• [4] Random-based Testing: Testing Monadic Code with QuickCheck, QuickCheck Tutorial
• [5] Unit-Sequence-Reactive Testing: Test-sequence generation with hol-testgen - with an application to firewall testing
• [6] Application: Firewall Testing, Model-based Firewall Conformance Testing
• [7] Symbolic IOCO : A Symbolic Framework for Model-Based Testing,Testing of Reactive Systems The IOCO testing theory
• [8] Tools :Tools for Test Case Generation
• [9] Testing Non-Determinism: Optimal Strategies For Testing Nondeterministic Systems
• [10] Large-Scale Industrial Application: Using Model-Based Testing for Quality Assurance of Protocol Documentation
• [11] Invariant Generation By Tests: From Tests To Proofs
• [12] Testing Pointer Programs : Test Input Generation for Programs with Pointers