North-east corner elevation, Sunshine Coast University Library, Maroochydore

View to north-east corner elevation, with entrance stair and timber batten screen to verandah.

Entrance stair, Sunshine Coast University Library, Maroochydore

View to entrance stair as seen from exterior court.

South elevation elevation, Sunshine Coast University Library, Maroochydore

View to south-east elevation with corrugated steel cladding, plywood, concrete block and colonnade, as seen from exterior.

South-east elevation, Sunshine Coast University Library, Maroochydore

View to south-east elevation; entrance stair, plywood and sheet steel cladding and colonnade, as seen from exterior.

Timber batten screen to north-east elevation, Sunshine Coast University Library, Maroochydore

View of timber batten screen to verandah behind and entrance stair, as seen from exterior.

Batten screen to north-east elevation, Sunshine Coast University Library, Maroochydore

View of timber batten screen to north-east elevation with verandah behind.

Screen to verandah, Sunshine Coast University Library, Maroochydore

View of steel-framed timber screen to verandah.

Second floor reading area interior, Sunshine Coast University Library, Maroochydore

View of second floor reading area with rigid frames and air-conditioning ducting.

South-east elevation, Sunshine Coast University Library, Maroochydore

View to south-east elevation as seen from exterior.

North-west elevation, Sunshine Coast University Library, Maroochydore

North-west elevation as seen from Building K.

Entrance elevation, Sunshine Coast University Library, Maroochydore

View to entrance verandah on north-east elevation and sunshades to north-west elevation.

Trace Semantics for the Owicki-Gries Theory Integrated with the Progress Logic from UNITY

The theory of Owicki and Gries has been used as a platform for safety-based verifcation and derivation of concurrent programs. It has also been integrated with the progress logic of UNITY which has allowed newer techniques of progress-based verifcation and derivation to be developed. However, a theoretical basis for the integrated theory has thus far been missing. In this paper, we provide a theoretical background for the logic of Owicki and Gries integrated with the logic of progress from UNITY. An operational semantics for the new framework is provided which is used to prove soundness of the progress logic.

Probabilistic Action System Trace Semantics

Action systems are a construct for reasoning about concurrent, reactive systems, in which concurrent behaviour is described by interleaving atomic actions. Sere and Troubitsyna have proposed an extension to action systems in which actions may be expressed and composed using discrete probabilistic choice as well as demonic nondeterministic choice. In this paper we develop a trace-based semantics for probabilistic action systems. This semantics provides a simple theoretical base on which practical refinement rules for probabilistic action systems may be justified.