Syllabus

The table below gives the planned syllabus for the seminar. The syllabus lists the topics and papers to be discussed.

This syllabus is provisional and subject to change. If it is necessary to revise the schedule, then this page will be updated to reflect the changes.

Date Paper or Topic
Jan. 22 Overview, background on JML-related research, planning
Jan. 29 Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll. Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. In Formal Methods for Components and Objects (FMCO) 2005, Revised Lectures, pages 342-363. Volume 4111 of Lecture Notes in Computer Science, Springer Verlag, 2006.
The original publication is available at springerlink.com or directly from http://dx.doi.org/10.1007/11804192_16.
[Corrected PDF]
Feb. 5 Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. In CASSIS 2004. Volume 3362 of Lecture Notes in Computer Science, Springer Verlag, 2004. [PDF]
Feb. 12 K. Rustan M. Leino and Peter Müller. Object invariants in dynamic contexts. In ECOOP 2004, LNCS vol. 3086, Springer, 2004. [PDF]
Feb. 19 K. Rustan M. Leino and Peter Müller. Modular verification of static class invariants. In FM 2005. [PDF]
Feb. 26 Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular Invariants for Layered Object Structures. Science of Computer Programming, 62(3):253-286, Elsevier, Oct. 2006. http://dx.doi.org/10.1016/j.scico.2006.03.001
Also ETH Zurich, Technical Report 424, October 2003, revised March 2004, March 2005. [abstract] [Preprint PDF]
Mar. 5 No class
Mar. 12 Spring break, no class
Mar. 19 Bart Jacobs, K. Rustan M. Leino, Frank Piessens, and Wolfram Schulte. In SEFM 2005 Safe Concurrency for Aggregate Objects with Invariants. [PDF]
Mar. 26 Yoonsik Cheon and Ashaveena Perumendla. Specifying and Checking Method Call Sequences of Java Programs. To appear in Software Quality Journal, 2006.
Department of Computer Science, The University of Texas at El Paso, TR #05-36, November 2005. This is an extended version of the paper appeared in Proceedings of the 2005 International Conference on Software Engineering Research and Experience (SERP '05), Las Vegas, Nevada, June 27-30, 2005, pages 511-516. [PDF]
Apr. 2 Steve M. Shaner, Gary T. Leavens, David A. Naumann, Modular Verification of Higher-Order Methods with Mandatory Calls Specified by Model Programs. Department of Computer Science, Iowa State University, TR #07-04, March 2007. [PDF]
Apr. 9 Kerry Trentelman and Marieke Huisman Extending JML Specifications with Temporal Logic. In AMAST '02: Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology, pages 334-348. Volume 2422 of Lecture Notes in Computer Science, Springer-Verlag, 2002. [Postscript]
Apr. 16 Lilian Burdy and Mariela Pavlova. Java Bytecode Specification and Verification. In SAC 2006, ACM, 2006. [PDF]
Apr. 23 Mike Barnett, David A. Naumann, Wolfram Schulte, and Qi Sun. 99.44% pure: Useful Abstractions in Specifications. In FTfJP 2004. [PDF]

Last modified Monday, March 26, 2007.