Next Meeting:
Thursday June 16 at 4pm c.t. in Room 019, MPI ground floor

Software Model Checking Seminar

Software Model Checking deals with automated verification of programs. A variety of successful tools have emerged in the recent years, some of them have found application in the industry.

We are going to learn about Software Model Checking:

  • read papers about underlying methods and algorithms,
  • play with tools,
  • discuss in the class,
  • find out what could be done better,
  • ...

    After successful participation in the seminar you will have:

  • 9 credit points,
  • a basis for a bachelor, master, PhD thesis in the area of Software Model Checking.

    Program Proposal

    Tools

  • BLAST - Berkeley Lazy Abstraction Software Verification Tool
  • MAGIC - Modular Analysis of Programs In C.
  • SLAM - The Software, Languages, Analysis and Model checking project.
  • VeriSoft - a tool for Systematic Software Testing.

    Papers

    1. Speaker: MK. 12 May 2005. Talk slides.
    Boolean and Cartesian Abstraction for Model Checking C Programs. Thomas Ball, Andreas Podelski, and Sriram K. Rajamani. In Proceedings of TACAS: Tools and Algorithms for the Construction and Analysis of Systems. Genova, Italy, April 2001.
    2. Speaker: AR. 19 May 2005
    Automatic Predicate Abstraction of C Programs. Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani. Proceedings of the Conference on Programming Language Design and Implementation (PLDI 2001), Snowbird, Utah, June 20-22, 2001.
    3.
    Bebop: A Symbolic Model Checker for Boolean Programs. T. Ball and S. K. Rajamani. Microsoft Research
    4. Speaker: MS. 2. Juni 2005
    Summarizing Procedures in Concurrent Programs. S. Qadeer, S.K. Rajamani and J. Rehof. Proceedings of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004.
    5. Speaker: RD. 9. Juni 2005. Talk slides.
    Relative Completeness of Abstraction Refinement for Software Model Checking. Thomas Ball, Andreas Podelski, Sriram K. Rajamani. In Proceedings of TACAS 2002: Tools and Algorithms for the Construction and Analysis of Systems. Grenoble, France, April 2002.
    6. Speaker: JH. 16. Juni 2005
    Lazy Abstraction. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Proceedings of the 29th Annual Symposium on Principles of Programming Languages (POPL), ACM Press, 2002, pp. 58-70.
    7. Speaker: SC. 23. Juni 2005
    Interpolation and SAT-based Model Checking. K. L. McMillan. Computer Aided Verification (CAV03), F. Somenzi and W. Hunt, eds., July 2003.
    8. Speaker: AF. 30. Juni 2005
    Abstractions from Proofs. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Kenneth L. McMillan. Proceedings of the 31st ACM Symposium on Principles of Programming Languages(POPL 2004).
    9. Speaker: FH. 7. Juli 2005
    Model-Checking Pushdown Systems. Stefan Schwoon, Dissertation, 2002. Definitions. Pre*- und Post*-Computation. Bibiography.
    10. Speaker: SB. 14. Juli 2005
    Thread-modular model checking. Cormac Flanagan and Shaz Qadeer. Proceedings of the SPIN Workshop on Software Verification, 2003.
    11.
    Thread-modular abstraction refinement. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Proceedings of the 15th International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science 2725, Springer-Verlag, 2003, pp. 262-274.
    12. Speaker: PW. 21. Juli 2005
    Race Checking by Context Inference. Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Proceedings of the International Conference on Programming Language Design and Implementation (PLDI), ACM Press, 2004.
    13.
    Model Checking for Programming Languages using VeriSoft, Patrice Godefroid, POPL'07. The journal version of this paper: Software Model Checking: The VeriSoft Approach, FMSD Vol. 26, No. 2, March 2005.
    14.
    Predicate Abstraction for Software Verification. Cormac Flanagan and Shaz Qadeer. In POPL 02, pages 191-202. ACM, January 2002.
    15.
    Constructing Quantified Invariants via Predicate Abstraction. S. K. Lahiri, and R. E. Bryant. Verification, Model Checking, and Abstract Interpretation (VMCAI '04), B. Steffen, and G. Levi, eds., LNCS 2937, Springer-Verlag, February, 2004, pp. 267-281
    Last modified: Mon Jun 13 15:58:22 CEST 2005