Proof-carrying code is an application of software verification techniques to the problem of ensuring the safety of mobile code. However, previous proof-carrying code systems have assumed that mobile code will faithfully execute the instructions of the program. Realistic implementations of computing systems are susceptible to probabilistic behaviours that can alter the execution of a program in ways that can result in corruption or security breaches. We investigate the use of a probabilistic bytecode language to model deterministic programs that are executed on probabilistic computing systems. To model probabilistic safety properties, a probabilistic logic is adapted to out bytecode instruction language, and soundness is proven. A sketch of a completeness proof of the logic is also shown.

Communication protocols, a class of critical systems, play an important role in industry. These protocols are critical because the tolerance for faults in these systems is low and it is highly desirable that these systems work correctly. Therefore, an effective methodology for describing and verifying that these systems behave according to their specifications is vitally important. Model checking is a verification technique in which a mathematically precise model of the system, either concrete or with abstraction, is built and a specification of how the system should behave is given. Then the system is considered correct if its model satisfies its specification. However, due to their size and complexity, critical systems, such as communication systems, are notoriously resistant to formal modelling and verification. In this thesis, we propose using graph transformation systems (GTSs), a visual semantic modelling approach, to model the behaviour of dynamically evolving communication protocols. Then, we show how a GTS model can facilitate verification of invariant properties of potentially unbounded communication systems. Finally, due to the use of similar isomorphic components in communication systems, we show how to exploit symmetries of these dynamically evolving models described by GTSs, to reduce the size of the model under verification. We use graph transformation systems to provide an expressive and intuitive visual description of the system state as a graph and for the computations of the system as a finite set of rules that transform the state graphs. Our model is well-suited for describing the behaviour of individual components, error-free communication channels amongst the components, and dynamic component creation and elimination. Thus, the structure of the generated model closely resembles the way in which communication protocols are typically separated into three levels: the first describing local features or components, the second characterizing interactions among components, and the third showing the evolution of the component set. The graph transformation semantics follows this scheme, enabling a clean separation of concerns when describing a protocol. This separation of concerns is a necessity for formal analysis of system behaviour. We prove that the finite set of graph transformation rules that describe behaviour of the system can be used to perform verification for invariant properties of the system. We show that if a property is preserved by the finite set of transformation rules describing the system model, and if the initial state satisfies the property, then the property is an invariant of the system model. Therefore, our verification method may avoid the explicit analysis of the potentially enormous state space that the transformation rules encode. In this thesis, we also develop symmetry reduction techniques applicable to dynamically evolving GTS models. The necessity to extend the existing symmetry reduction techniques arises because these techniques are not applicable to dynamic models such as those described by GTSs, and, in addition, these existing techniques may offer only limited reduction to systems that are not fully symmetric. We present an algorithm for generating a symmetry-reduced quotient model directly from a set of graph transformation rules. The generated quotient model is bisimilar to the model under verification and may be exponentially smaller than that model.

None

Not available / text

Not available / text

The design of complex digital hardware is challenging and error-prone. With short design cycles and increasing complexity of designs, functional verification has become the most expensive and time-consuming aspect of the digital design process. Sequential equivalence checking (SEC) has been proposed as a verification framework to perform a true sequential check of input/output equivalence between two designs. SEC provides several benefits that can enable a faster and more efficient way to design and verify large and complex digital hardware. It can be used to prove that micro-architectural optimizations needed for design closure preserve design functionality, and thus avoid the costly and incomplete functional verification regression traditionally used for such purposes. Moreover, SEC can be used to validate sequential synthesis transformations and thereby enable design and verification at a higher-level of abstraction. Use of sequential synthesis leads to shorter design cycles and can result in a significant improvement in design quality. In this dissertation, we study the problem of sequential redundancy identification to enable robust sequential equivalence checking solutions. In particular, we focus on the use of a transformation-based verification framework to synergistically leverage various transformations to simplify and decompose large problems which arise during sequential redundancy identification to enable an efficient and highly scalable SEC solution. We make five main contributions in this dissertation. First, we introduce a novel sequential redundancy identification framework that dramatically increases the scalability of SEC. Second, we propose the use of a flexible and synergistic set of transformation and verification algorithms for sequential redundancy identification. This more general approach enables greater speed and scalability and identifies a significantly greater degree of redundancy than previous approaches. Third, we introduce the theory and practice of transformation-based verification in the presence of constraints. Constraints are pervasively used in verification testbenches to specify environmental assumptions to prevent illegal input scenarios. Fourth, we develop the theoretical framework with corresponding efficient implementation for optimal sequential redundancy identification in the presence of constraints. Fifth, we address the scalability of transformation-based verification by proposing two new structural abstraction techniques. We also study the synergies between various transformation algorithms and propose new strategies for using these transformations to enable scalable sequential redundancy identification. / text

People feel discomfort when they receive feedback about their relational value that is inconsistent with their self-esteem and certainty when they receive feedback that is consistent (Stinson et al., 2010). Feeling discomfort prompts additional feedback-seeking to confirm or disprove the original feedback (Swann, 1987). Feeling certainty does not. People base their self-views on years of experience and so are more likely to seek self-view consistent feedback (Swann, 1987). Participants were given high relational value feedback to invoke discomfort in individuals with low self-esteem (LSEs) but not individuals with high self-esteem (HSEs). Participants were then able to seek additional relational-value feedback. LSEs were expected to seek self-esteem consistent feedback to reduce discomfort whereas HSEs were not expected to seek additional feedback because they would not be experiencing discomfort. Results did not support these hypotheses for all participants: Single LSEs sought feedback as a function of self-esteem but mated LSEs did not. / Graduate

Not available / text

Not available / text

Darbe pateiktas sezoninių prognozių, sudarytų DEMETER (Development of a European Multimodel Ensemble system for seasonal to inTERannual prediction) projekte naudotų modelių, statistinis patikimumo įvertinimas. Pagrindinis darbo tikslas - įvertinti prognostinės sistemos darbą, kurią sudaro 6 globaliniai jungtiniai atmosferos-vandenyno modeliai, sukurti įvairiuose meteorologijos centruose. Sezoninio prognozavimo sistemos gebėjimams apibūdinti analizuojami DEMETER duomenys, paleisti kiekvienais metais per 1990-2001 metų laikotarpį vasario, gegužės, rugpjūčio ir lapkričio mėnesių pirmą dieną. Pradinės atmosferos ir sausumos paviršiaus modelių sąlygos paimtos iš ECMWF Re-Analysis (ERA-40) duomenų bazės. Kiekvienas prognozės paleidimas šešiems mėnesiams į priekį sudaro ansamblį iš 9 narių. Multimodelio prognozės šiame darbe buvo verifikuojamos su stebėjimais, išmatuotais 17 meteorologijos stotyse, kurių duomenys gauti iš Lietuvos hidrometeorologijos tarnybos archyvo. 1 ir 2 darbo skyriuose pateikta bendrą sezoninių prognozių samprata, pažymėtas jų naudingumas, trumpai aptartas sudarymo principas bei verifikacijos būdai. 2 skyrius skirtas DEMETER sudarančių modelių charakteristikoms aprašyti. 3 skyriuje išdėstyti dažnaiusiai taikomi nepertraukiamų parametrų, tokių kaip oro temperatūra, prognozių verifikacijos metodai bei aprašyta šio darbo eiga, išvardintos programos, naudotos atliekant skaičiavimus ir pavaizduojant rezultatus grafiškai. 4 skyriuje pateikta verifikacijos rezultatų... [toliau žr. visą tekstą] / In this study, results concerning statistical verification of DEMETER (Development of a European Multimodel Ensemble system for seasonal to inTERannual prediction) seasonal forecasts over Lithuania is presented. The main task is assessing multimodel prediction system performance. The system comprises the global coupled ocean-atmosphere models of several institutions. In order to assess seasonal dependence on forecast skills, the DEMETER hindcasts have been started from the 1st February, 1st May, 1st August and 1st November, the analyzed period is 1990-2001. The atmospheric and land-surface initial conditions are taken from the ECMWF Re-Analysis (ERA-40) dataset. The ocean initial conditions are obtained from ocean-only runs forced by ERA-40 fluxes, except in the case of MPI that used a coupled initialization method. Ech hindcast has been integrated for 6 months and comprises an ensemble of 9 members. Multimodel forecasts were verified against observations of 17 meteorological stations obtained from the Lithuanian Hydrometerological Service. In section 1 and 2 of this paper a general definition of seasonal forecast are introduced and some characteristics of statistical forecast verification are discussed as well as the short description of DEMETER multimodel members is given. Section 3 explores some basic and the most common in use technics of continuous forecasts verification. Based on statistical verificatiom methods, described in previous section, an analysis of each... [to full text]