Formal Methods

The reading group was established in 1997 to bring people interested in formal methods together, to serve as a study group to help its members in understanding the background for and the current advances in formal methods research, and to serve as a sounding board for new ideas in this area. The primary interests of the group are in automated verifications (model-checking and theorem-proving), decision procedures, and refinement. We are also interested in a variety of topics, including automata-theory, programming languages semantics, etc.

The group is open to students/faculty/visitors at all levels, and includes tea and cookies.

Presently, the group meets on Wednesday afternoons, 3:00-5:00 p.m. in BA5256.

You are welcome to join us on any day. However, for announcements about the current paper or other information of interest, you may want to join the mailing list. To do so, please contact M. Chechik.

Visitors And Talks:

2004-04-30 :: Arie and Ric "current work" Department of Computer Science, UofT
2004-04-06 :: Eric Wohlstadter "Middleware to Sweeten Quality-of-Service Policy Interactions" University of California, Davis
2004-03-25 :: Arie "current work" Department of Computer Science, UofT
2004-03-05 :: Martin Robillard "Finding and Describing Concerns Using Structural Program Dependencies" University of British Columbia
2004-02-21 :: Ioannis Kassios "current work" Department of Computer Science, UofT
2004-01-31 :: Wendy Liu "current work" Department of Computer Science, UofT

Papers Read:

2004-08-04 :: Bishop Brock and J. Strother Moore, A Mechanically Checked Proof of a Comparator Sort Algorithm, [1999], vol., pp..
2004-07-28 :: Cedric Fournet, Tony Hoare, Sriram K. Rajamani, Jakob Rehof, Struct-Free Conformance, [2004], vol., pp..
2004-07-21 :: Thomas Reps, Mooly Sagiv, Reinhard Wilhelm, Static Program Analysis via 3-Valued Logic, [2004], vol., pp..
2004-07-07 :: T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck, Parameterized Verification with Automatically Computed Inductive Assertions, [2001], vol., pp..
2004-06-23 :: Back and von Wrrght, Compositional Action System Refinement, [2004], vol.15, pp..
2004-06-02 :: Rutger Dijkstra, Computation Calculus Bridhing a Formalization Gap, Science of Computer Programming [2000], vol.37, pp.3-36.
2004-05-26 :: Joakim von Wright, From Kleene Algebra to Refinement Algebra, MPC [2002], vol., pp..
2004-04-06 :: Eric Wohlstadter, Stefan Tai, Thomas Mikalsen, Isabelle Rouvellou, and Premkumar Devanbu, Middleware to Sweeten Quality-of-Service Policy Interactions, ICSE [2004], vol., pp..
2004-03-23 :: Sagar Chaki, Edmund M.Clarke, J.Ouaknine, Natasha Sharygina, and Nishant Sinha, Integrated Formal Methods, IFM [2004], vol., pp..
2004-03-16 :: Ilya Shlyakhter, Robert Seater, Daniel Jackson, Manu Sridharan, Mana Taghdiri, Debugging Oversonstrained Declearative Models Using Unsatisfiable Cores, ASE [2003], vol., pp..
2004-03-14 :: R.Giegerich and C.Meyer, Algebraic Dynamic Programming, AMAST [2002], vol., pp..
2004-03-05 :: Martin Robillard and Gail Murphy, Concern Graphs: Finding and Describing Concerns Using Structural Program Dependencies, ICSE [2002], vol., pp..
2004-02-06 :: Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Lazy Abstraction, POPL [2002], vol., pp..
2004-01-23 :: Michael Jackson, The Meaning of Requirements, Annals of Software Engineering [1997], vol.3, pp..
2004-01-15 :: Luca de Alfaro and Tom Henzinger, Interface Automata, [], vol., pp..
2004-01-09 :: Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, Marcin Jurdzinski, and Freddy Y. C. Mang, Interface compatibility Checking for Software Modules, CAV [2002], vol., pp..