When all participants are more fluent in Dutch, we switch to Dutch.
This is a weekly working group for advanced students (roughly master level) and interested staff members. In this group, we read papers with various subjects from computer science that have been (or can be) approached by formal methods. The aim is a precise understanding of the goals, methods and results of the paper, and to investigate the possibilities for a better presentation for these things.
We have various subjects and sources: we have read papers about graph algorithms, concurrency, lazyness in functional languages, geometric algorithms, delay-insensitive circuits, process algebras, etc. The papers come from scientific journals, conferences, or the web. Some of them were written by ourselves.
The last paper we read before the summer was:
W.H. Hesselink: Verification of concurrent algorithms: revisiting
mutual exclusion by Lycklama-Hadzilacos (draft, 2010).
Before that, we read:
R.V. van Nieuwpoort, G. Wrzesinska, C.J.H. Jacobs, H.E. Bal:
Satin: a high-level and efficient grid programming model. ACM TOPLAS
32 Article 9, 2010.
S. Markstrum, D. Marino, M. Esquivel, T. Millstein, C. Andreae, J. Noble:
JavaCOP: declarative pluggable types for Java. ACM TOPLAS 32,
no. 2, article 4, 2010.
M. Frigo, C.E. Leiserson, H. Prokop, S. Ramachandran:
Cache-Oblivious Algorithms.
D.J. Pearce, P.H.J. Kelly, C. Hankin: Efficient field-sensitive pointer
analysis of C. ACM TOPLAS 30, no. 1, article 4, 2007.
M. Naik and J. Palsberg: A type system equivalent to a model checker.
ACM TOPLAS 30, no. 5, article 29, 2008.
D. Sangiorgi: On the origins of bisimulation and coinduction.
ACM TOPLAS 31, no 4, article 15, 2009.
P.E. McKenney: Memory Barriers: a hardware view for software hackers,
April 2009. Web.
A. Aravind and W.H. Hesselink: Nonatomic dual bakery for mutual exclusion.
Draft, November 2009.
R. Guerraoui, D. Kostic, R.R. Levy, V. Quema: A high throughput atomic
storage algorithm. Web.
J.M. Morris, A. Bunkenburg, and M. Tyrrell: Term transformers: a new
approach to state. ACM TOPLAS 31, no 4, article 16, 2009.
L.G. Valiant: Evolvability. J. ACM 56, no 1, article 3, 2009.
W.N. Scherer III, D. Lea, M.L. Scott: Scalable synchronous queues
Comm. ACM 52 (May 2009) no 5.
A.L. de Moura, R. Ierusalimschy: Revisiting coroutines.
ACM TOPLAS 31, no 2, article 6, 2009.
W.H. Hesselink, M.I. Lali: Formalizing a hierarchical file system
(submitted to a conference).
Jim Larson: Erlang for Concurrent Programming. Communications ACM 52
(2009) 48-56.
J.M. Morris and M. Tyrrell: Dually Nondeterministic Functions,
ACM TOPLAS 30 (6), paper 34 (2008).
W. Weimer and G.C. Necula: Exceptional Situations and program Reliability.
ACM TOPLAS 30 (2), paper 30 (2008).
R. Lammel: Google's MapReduce programming model - revisited. Science of
Computer Programming 70 (2008) 1-30.
J. Yang, P. Twohey, D. Engler:
Using model checking to find serious file system errors.
ACM Trans. on Computer Systems 24 (2006) 393-423.
E. Scott, A. Johnstone: Right nulled GLR parsers.
ACM Transactions on Programming Languages and Systems 28 (2006) 577-618.
W.H. Hesselink, J.C. Hummelen, H.T. Jonkman,
H.G. Reker, G.R. Renardel de Lavalette, M.H. van der Veen:
Kekulé Cells for Molecular Computation,
in a draft of October 2006.
P.A. Buhr, A.S. Harji: Implicit signal monitors. ACM TOPLAS 27 (2005)
1270-1343.
Raymond Boute: Functional declarative language design and predicate calculus:
a practical approach. ACM TOPLAS 27 (2005) 988-1047.
M.M. Michael: Scalable lock-free dynamic memory allocation (web)
N. Benton, L. Cardelli, C. Fournet: Modern Concurrency Abstractions for C#.
ACM TOPLAS 26 (2004)769-804.
R.J.M. Hughes, S.D. Swierstra: Polish parsers, step by step (web).
Gao H., Groote J.F., Hesselink W.H.:
Lock-free parallel and concurrent garbage collection by mark&sweep.
Science of Computer Programming 64 (2007) 341-374.
Sergei Gorlatch: Send-receive considered harmful: myths and realities of
message passing. ACM TOPLAS 26 (2004) 47-56.
Participation does not ask much in the way of preparation. You will get no credit points for it. At the sessions, you are supposed to fully participate. When you join the group, you are expected to come or to notify your absence.
Participation to the group is a good preparation for the final master project, not necessarily under my supervision. You learn to read the scientific literature carefully and critically, which is also a good preparation for writing scientific papers. The meetings are weekly, throughout the year except for the summer. When you are interested, there is usually in short term a good moment to join the group. For more information: come along and ask me (Bernoulliborg office 374).
Back to my
educational page
or my
home page.
Wim H. Hesselink