Teaching Concurrency with the Disappearing Formal Method. Sekerinski, E. In Dongol, B., Petre, L., & Smith, G., editors, Formal Methods Teaching, Third International Workshop and Tutorial, volume 11758, of Lecture Notes in Computer Science, pages 135–149, October, 2019. Springer.
doi  abstract   bibtex   1 download  
The Gries-Owicki non-interference condition is fundamental to concurrent programming, but difficult to explain as it relies on proof outlines rather than only pre- and postconditions. This paper reports on teaching a practical course on concurrent programming using hierarchical state diagrams to visualize concurrent programs and argue for their correctness, including non-interference.
@inproceedings{Sekerinski19DisappearingFormalMethod,
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Teaching {Concurrency} with the {Disappearing} {Formal} {Method}},
	volume = {11758},
	isbn = {978-3-030-32441-4},
	doi = {10.1007/978-3-030-32441-4_9},
	abstract = {The Gries-Owicki non-interference condition is fundamental to concurrent programming, but difficult to explain as it relies on proof outlines rather than only pre- and postconditions. This paper reports on teaching a practical course on concurrent programming using hierarchical state diagrams to visualize concurrent programs and argue for their correctness, including non-interference.},
	booktitle = {Formal {Methods} {Teaching}, {Third} {International} {Workshop} and {Tutorial}},
	publisher = {Springer},
	author = {Sekerinski, Emil},
	editor = {Dongol, Brijesh and Petre, Luigia and Smith, Graeme},
	month = oct,
	year = {2019},
	keywords = {Guarded commands, Non-interference, State diagrams},
	pages = {135--149},
}

Downloads: 1