Show simple item record

dc.contributor.advisorButterfield, Andrew
dc.contributor.authorBresciani, Riccardo
dc.date.accessioned2018-08-14T10:44:51Z
dc.date.available2018-08-14T10:44:51Z
dc.date.issued2013
dc.identifier.citationRiccardo Bresciani, 'Probabilistic program verification in the style of the unifying theories of programming', [thesis], Trinity College (Dublin, Ireland). School of Computer Science & Statistics, 2013, pp. 188
dc.identifier.otherTHESIS 10277
dc.identifier.urihttp://hdl.handle.net/2262/83763
dc.description.abstractWe present a novel framework to reason on programs based on probability distributions on the state space of a program: they are functions from program states to real numbers in the range [0..1], which can be used to represent the probability of a program being in that state. Such framework can be used to provide an elegant semantics in the style of UTP to a variety of programming languages using both probabilistic and nondeterministic constructs: the use of probability distributions allows us to give programs a semantics which is based on homogeneous relations. The behaviour of probabilistic nondeterministic programs is treated algebraically via this framework, and as a result it is straightforward to derive algebraic expressions for the probability of some properties to hold for a given program. Moreover our framework unifies all of the different kinds of choice under a single “generic choice” construct, and the usual choice constructs (disjunction, conditional choice, probabilistic choice, and nondeterministic choice) can be viewed as some of its specific instances. Later on we will discuss also other possible specific instances (namely conditional probabilistic choice, switching probabilistic choice, conditional nondeterministic choice, nondeterministic probabilistic choice, and fair nondeterministic choice). The use of probability allows us to introduce the notion of probabilistic refinement, which generalises the traditional one: this is important in view of formal verification of probabilistic properties of programs via refinement-based techniques.
dc.format1 volume
dc.language.isoen
dc.publisherTrinity College (Dublin, Ireland). School of Computer Science & Statistics
dc.relation.isversionofhttp://stella.catalogue.tcd.ie/iii/encore/record/C__Rb15651563
dc.subjectComputer Science, Ph.D.
dc.subjectPh.D. Trinity College Dublin
dc.titleProbabilistic program verification in the style of the unifying theories of programming
dc.typethesis
dc.contributor.sponsorScience Foundation Ireland
dc.type.supercollectionthesis_dissertations
dc.type.supercollectionrefereed_publications
dc.type.qualificationlevelDoctoral
dc.type.qualificationnameDoctor of Philosophy (Ph.D.)
dc.rights.ecaccessrightsopenAccess
dc.contributor.sponsorGrantNumber08/RFP/CMS1277; 03/CE2/I303_1
dc.format.extentpaginationpp. 188
dc.description.noteTARA (Trinity’s Access to Research Archive) has a robust takedown policy. Please contact us if you have any concerns: rssadmin@tcd.ie


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record