https://www.um.edu.mt/library/oar/handle/123456789/65299 2026-04-11T01:30:40Z 2026-04-11T01:30:40Z https://www.um.edu.mt/library/oar/handle/123456789/73739 2021-04-15T07:17:22Z 2019-01-01T00:00:00Z

Title: Residual-based combination of static and runtime verification Abstract: While verification techniques attempt to solve the problem of checking that a program satisfies a property they can fail and give an indeterminate verdict. In a survey of literature we identify approaches that improve this by allowing a verification technique to produce a new proof obligation by either transforming a property and/or transforming a program. Here we choose to focus on techniques that transform a property. To reason about these we present an abstract formal framework that characterises properties in terms of the programs that satisfy them. In turn we are able to characterise a residual property that is equivalent to the original property for the program under verification. We instantiate this approach for both state- and event-based properties, showing how the conjunction of properties can be wielded to produce effective residual properties to reduce the verification effort for subsequent techniques. We validate further this approach for state-based properties in the context of industrial project involving a payments ecosystem and untrusted client applications, where a enforced model of behaviour allows us to verify or partially evaluate at pre-deployment certain regulations specified as universally quantified propositions. Our main contribution is an approach for the combination of static and runtime verification for automata-based properties. Existing such approaches focus on the reduction of instrumentation of a program, while we present an approach to the reduction of structural elements of a property. We focus on dynamic event automata (DEA) as event-based properties that monitor both the program control-flow and the program data-state. We give an intraprocedural approach to analysing a property against a program. This allows us to collect knowledge about the behaviour of each procedure individually (ignoring possible outside behaviour) to produce a residual of the whole-program. The algorithm can easily be adapted to the interprocedural case. Moreover, by adding an assertion propagation algorithm and the use of an SMT solver we show how this can be optimised by pruning the possible behaviour and evaluating property guards. We validated this approach on both Java programs and Solidity smart contracts, showing moderate overhead improvements but significant progress in reducing the property. Description: PH.D.COMPUTER SCIENCE

2019-01-01T00:00:00Z https://www.um.edu.mt/library/oar/handle/123456789/73717 2021-04-15T07:10:10Z 2019-01-01T00:00:00Z

Title: Macroprogramming using an embedded DSL approach Abstract: Software applications were traditionally developed using a monolithic approach and developed as a single instance. As distributed systems emerged, these traditional methods were no longer suitable. In the domain of wireless sensor networks, an application is developed to run across multiple nodes, and devices must communicate and collaborate together. The general trend is for a software developer to write a single program which is loaded on all the devices. In the case of heterogeneous networks where the systems making up the network vary in architecture, capabilities and characteristics a different approach is used — different programs are written and loaded on each different system. Such an approach requires expertise programming different systems, and the interactions between disparate systems need to be explicitly handled by the programmer. In this thesis, we propose a model for programming heterogeneous systems using a single macroprogram, thereby achieving a higher level of abstraction and enabling applications to be described at the macro-level. We combine techniques from macroprogramming and multi-target compilation, using an embedded DSL approach to generate target-specific code for different domains on different ends of the spectrum. On one end of the spectrum, we apply the model to wireless sensor networks where challenges exist around optimising code for execution on heavily resource constrained devices. At the other end of the spectrum, we propose a framework for writing smart contracts spanning multiple diverse blockchain systems. Each domain brings its’ own challenges, however the model is shown to be applicable to different domains. Description: PH.D.COMPUTER SCIENCE

2019-01-01T00:00:00Z https://www.um.edu.mt/library/oar/handle/123456789/65461 2020-12-10T14:46:49Z 2019-01-01T00:00:00Z

Title: Interpreting neural networks via activation maximization Abstract: Decision trees are models whose structure allows for tracing an explanation of how the final decision was taken. Neural networks known as ’black box’ models, do not readily and explicitly offer an explanation of how the decision was reached. However since Neural Networks are capable of learning knowledge representation it will be very useful to interpret the model’s decisions. In this project the Visual Relationship Detection problem will be explored in the form of different Neural Network implementations and training methods. These implementations include two Convolutional Neural Network architectures (VGG16 and SmallVGG) and two Feed Forward Neural Networks trained using Geometric features and Geometric with Language Features. These models will be treated as two kinds of problems, one is the Multi-Label Classification problem and the other is the Single-Label Classification problem. Activation Maximisation will be used to interpret the different Convolutional Neural Networks under different training methods by maximizing a specific class output to visualize what it is learning. This study is grounded in the recognition of spatial relations between objects in images. Activation Maximization will shed light on what models are learning about objects in 2D images which should give insight into how the system can be improved. The spatial relation problem is one where given a subject and an object the correct spatial preposition is predicted. This problem extends beyond just predicting one correct spatial preposition as there are multiple possible relationships associated between two objects. Description: B.SC.(HONS)COMP.SCI.

2019-01-01T00:00:00Z https://www.um.edu.mt/library/oar/handle/123456789/65460 2020-12-10T14:45:36Z 2019-01-01T00:00:00Z

Title: Real-time GI for dynamic environments using temporal filtering Abstract: Real-time rendering applications have traditionally shunned from implementing fully dynamic global illumination solutions due to their high computational cost, despite the added value in terms of realism and image quality the latter can afford. However, with the recent advent of rendering hardware accelerating ray tracing-based methods, new avenues of research have opened up that investigate the use of offline global illumination rendering techniques for real-time purposes. In this dissertation, we propose a method for interactive global illumination that reformulates IGI, a traditionally CPU-based rendering approach, and augments the derived solution with information from previously rendered frames. Theproposedmethodisfullydynamic,inthatnopre-computationisrequiredand scene objects such as light sources, geometry and materials may be updated without any performance penalty. We evaluate the method’s performance in both static and dynamic scenes, and compare the resulting image quality against ground truth images generated from an unbiased offline renderer. Results are promising and show that the method may be viably used for interactive applications, without degrading the quality of the output. Description: B.SC.(HONS)COMP.SCI.

2019-01-01T00:00:00Z