Recent Trends in Program Analysis, Verification, and Testing

A reading course on recent trends in program analysis, verification and testing will be organised in the group Testing of Reactive Systems Group. Other interested Ph.D. students and researchers are most welcome to participate and suggest papers! Ph.D. students can take the course for credit points.

Papers

• May 23, 13.15, room 1406: Korat: Automated Testing Based on Java Predicates, Chandrasekhar Boyapati, Sarfraz Khurshid, Darko Marinov. Presented by Anders Hessel.
• May 31, 13.15, room 1406: Dynamically Discovering Likely Program Invariants to Support Program Evolution, Michael Ernst, Jake Cockrell, William G. Griswold, David Notkin. To be read by all course participants. Per Gustafsson will present.
• June 7, 13.15, room 1406: Parametric Shape Analysis via 3-Valued Logic, Mooly Sagiv, Thomas Reps, Reinhard Wilhelm. Ahmed Rezine will present up to (including) section 4 of the paper.
• June 14, 13.15, room 1406: Parametric Shape Analysis via 3-Valued Logic, Mooly Sagiv, Thomas Reps, Reinhard Wilhelm. Tobias Lindahl will present the rest of the paper.
• June 21, 13.15, room 1406: Specifying and Executing Behavioral Requirements: The Play-In/Play-Out Approach, David Harel, Rami Marelly. John Håkansson will present the paper.
• September 13, 13.15, room 1406: Coverage Metrics for Formal Verification, Hana Chockler, Orna Kupferman, Moshe Y. Vardi. Bengt Jonsson will present.
• September 27, 13.15, room 1406: QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs, Koen Claessen, John Hughes. Johan Blom will present.
• October 4, 13.15, room 1406:Interpolation and SAT-Based Model Checking, Kenneth L. McMillan. Bengt Jonsson will present the paper.
• October 11, 13.15, room 1406: Construction of abstract state graphs with PVS, Susanne Graf, Hassen Saidi. Lisa Kaati will present the paper.
• October 25, 13.15, room 1406: Static Analysis of Distributed Systems with Mobility Specified by Graph Grammars A Case Study, Paolo Baldan, Andrea Corradini, and Barbara König. Oskar Wibbling will present the paper.
• November 30, 13.15, room 2345: Lazy Abstraction with Interpolants, Kenneth L. McMillan. Bengt Jonsson will present.

Future Papers

Please suggest papers to be read in future seminars by editing this list (please include links to papers):

• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Patrick Cousot & Radhia Cousot.
• Boolean and Cartesian abstraction for model checking C programs Thomas Ball, Andreas Podelski and Sriram K. Rajamani
• On Test Suite Composition and Cost-Effective Regression Testing, Gregg Rothermel, Sebastian Elbaum, Alexey Malishevsky, Praveen Kallakuri, Xuemei Qiu.
• A Theory of Predicate-Complete Test Coverage and Generation, Thomas Ball, FMCO'04.

Organisers

The course is organised by Bengt Jonsson and Paul Pettersson.