Thesis (MSc)--Stellenbosch University, 2013. / ENGLISH ABSTRACT: The search for non-terminating paths within a program is a crucial part of software verification, as the detection of anfinite path is often the only manner of falsifying program termination - the failure of a termination prover to verify termination does not necessarily imply that a program is non-terminating. This document describes the development and implementation of two focussed techniques for investigating the non-termination of affine loops. The developed techniques depend on the known non-termination concepts of recurrent sets and Jordan matrix decomposition respectively, and imply the decidability of single-variable and cyclic affine loops. Furthermore, the techniques prove to be practically capable methods for both the location of non-terminating paths, as well as the generation of preconditions for non-termination. / AFRIKAANSE OPSOMMING: Sagtewareveri kasie vereis of die bewys van die beeindiging van 'n program, of die deteksie van oneindige uitvoerings. In hierdie tesis ontwikkel en implementeer ons twee tegnieke om oor die oneindige eienskap van a ene lusse te beslis. Die tegnieke wat ontwikkel word is gebaseer op konsepte soos Jordan matriksdekomposisie en herhaalde groepe wat al in die verlede gebruik is om die beeindiging van lusse te ondersoek. Die tegnieke kan gebruik word om die uitvoerbaarheid van beide een-veranderlike en sikliese a ene lusse te bepaal. Feitlik alle nie-eindige a ene lusse kan ge denti seer word en die toestande waaronder hierdie oneindige eienskap verskyn kan beskryf word.

Thesis (MSc)--Stellenbosch University, 2013. / ENGLISH ABSTRACT: The amount of information that users of social networks consume on a daily basis is steadily increasing. The resulting information overload is usually associated with a loss of control over the management of information sources, leaving users feeling overwhelmed. To address this problem, social networks have introduced tools with which users can organise the people in their networks. However, these tools do not integrate any automated processing. Twitter has lists that can be used to organise people in the network into topic-based groups. This feature is a powerful organisation tool that has two main obstacles to widespread user adoption: the initial setup time and continual curation. In this thesis, we investigate the problem of constructing topic-based Twitter lists. We identify two subproblems, an unsupervised and supervised task, that need to be considered when tackling this problem. These subproblems correspond to a clustering and classification approach that we evaluate on Twitter data sets. The clustering approach is evaluated using multiple representation techniques, similarity measures and clustering algorithms. We show that it is possible to incorporate a Twitter user’s social graph data into the clustering approach to find topic-based clusters. The classification approach is implemented, from a statistical relational learning perspective, with kLog. We show that kLog can use a user’s tweet content and social graph data to perform accurate topic-based classification. We conclude that it is feasible to construct useful topic-based Twitter lists with either approach. / AFRIKAANSE OPSOMMING: Die stroom van inligting wat sosiale-netwerk gebruikers op ’n daaglikse basis verwerk, is aan die groei. Vir baie gebruikers, skep hierdie oordosis inligting ’n gevoel dat hulle beheer oor hul inligtingsbronne verloor. As ’n oplossing, het sosiale-netwerke meganismes geïmplementeer waarmee gebruikers die inligting in hul netwerk kan bestuur. Hierdie meganismes is nie selfwerkend nie, maar kort toevoer van die gebruiker. Twitter het lyste geïmplementeer waarmee gebruikers ander mense in hul sosiale-netwerk kan groepeer. Lyste is ’n kragtige organiserings meganisme, maar tog vind grootskaal gebruik daarvan nie plaas nie. Gebruikers voel dat die opstelling te veel tyd in beslag neem en die onderhoud daarvan te veel moeite is. Hierdie tesis ondersoek die probleem om onderwerp-gerigte Twitter lyste te skep. Ons identisifeer twee subprobleme wat aangepak word deur ’n nie-toesig en ’n toesighoudende metode. Hierdie twee metodes hou verband met trosvorming en klassifikasie onderskeidelik. Ons evalueer beide die trosvorming en klassifikasie op twee Twitter datastelle. Die trosvorming metode word geëvalueer deur te kyk na verskillende voorstellingstegnieke, eendersheid maatstawwe en trosvorming algoritmes. Ons wys dat dit moontlik is om ’n gebruiker se Twitter netwerkdata in te sluit om onderwerp-gerigte groeperinge te vind. Die klassifikasie benadering word geïmplementeer met kLog, vanuit ’n statistiese relasionele leertoerie perspektief. Ons wys dat akkurate onderwerp-gerigte klassifikasie resultate verkry kan word met behulp van gebruikers se tweet-inhoud en sosiale-netwerk data. In beide gevalle wys ons dat dit moontlik is om onderwerp-gerigte Twitter lyste, met goeie resultate, te bou.

Thesis (PhD)--Stellenbosch University, 2013. / Please refer to full text to view abstract.

Thesis (MSc)--Stellenbosch University, 2013. / ENGLISH ABSTRACT: Probabilistic symbolic execution is a new approach that extends the normal symbolic execution with probability calculations. This approach combines symbolic execution and model counting to estimate the number of input values that would satisfy a given path condition, and thus is able to calculate the execution probability of a path. The focus has been on programs that manipulate primitive types such as linear integer arithmetic in object-oriented programming languages such as Java. In this thesis, we extend probabilistic symbolic execution to handle data structures, thus allowing support for reference types. Two techniques are proposed to calculate the probability of an execution when the programs have structures as inputs: an approximate approach that assumes probabilities for certain choices stay fixed during the execution and an accurate technique based on counting valid structures. We evaluate these approaches on an example of a Binary Search Tree and compare it to the classic approach which only take symbolic values as input. / AFRIKAANSE OPSOMMING: Probabilistiese simboliese uitvoering is ’n nuwe benadering wat die normale simboliese uitvoering uitbrei deur waarksynlikheidsberekeninge by te voeg. Hierdie benadering kombineer simboliese uitvoering en modeltellings om die aantal invoerwaardes wat ’n gegewe padvoorwaarde sal bevredig, te beraam en is dus in staat om die uitvoeringswaarskynlikheid van ’n pad te bereken. Tot dus vêr was die fokus op programme wat primitiewe datatipes manipuleer, byvoorbeeld lineêre heelgetalrekenkunde in objek-geörienteerde tale soos Java. In hierdie tesis brei ons probabilistiese simboliese uitvoering uit om datastrukture, en dus verwysingstipes, te dek. Twee tegnieke word voorgestel om die uitvoeringswaarskynlikheid van ’n program met datastrukture as invoer te bereken. Eerstens is daar die benaderingstegniek wat aanneem dat waarskynlikhede vir sekere keuses onveranderd sal bly tydens die uitvoering van die program. Tweedens is daar die akkurate tegniek wat gebaseer is op die telling van geldige datastrukture. Ons evalueer hierdie benaderings op ’n voorbeeld van ’n binêre soekboom en vergelyk dit met die klassieke tegniek wat slegs simboliese waardes as invoer neem.

Thesis (MSc (Mathematical Sciences)--University of Stellenbosch, 2010. / ENGLISH ABSTRACT: In this thesis, a pricing mechanism to stimulate cooperation between nodes in ad hoc networks is explored. The model incorporates incentives for users to act as transit nodes and carry the traffic between other nodes on multi-hop paths, and to be rewarded with their own ability to send traffic. The thesis investigates the consequences of this pricing model by means of simulation of a network and illustrates the way in which network resources are allocated to users according to their geographical position. Moreover, since modelling node movements is an important aspect in ad hoc network simulation, a collective mobility model, the adaptive mobility model, is used to maximise the area coverage of the nodes. / AFRIKAANSE OPSOMMING: In hierdie tesis word ’n koste meganisme gebruik om samewerking te stimuleer tussen nodusse in ad hoc netwerke. Die model inkorporeer trekpleisters deur gebruikers te beloon om verkeer te stuur deur op te tree as transito nodusse, en verkeer tussen nodusse op multi-skakel paaie te dra. Die tesis ondersoek die ge- volge van die koste model deur die simulering van ’n netwerk, en demonstreer die manier waarop die netwerk hulpbronne geallokeer word aan gebruikers gebaseer op hulle geografiese posisie. Siende dat die modellering van nodus bewegings ’n belangrike aspek is in ad hoc netwerk simulasie, word ’n kollek- tiewe mobiliteits model sowel as ’n veranderlike mobiliteits model gebruik om die dekkings areas van die nodusse te maksimeer.

Thesis (MSc)--Stellenbosch University, 2012. / ENGLISH ABSTRACT: see full text for abstract / AFRIKAANSE OPSOMMING: sien volteks vir opsomming

Thesis (MSc (Mathematical Sciences)--University of Stellenbosch, 2010. / ENGLISH ABSTRACT: Binary Decision Diagrams (BDDs) are data structures that have been used to solve various problems in different aspects of computer aided design and formal verification. The large memory and time requirements of BDD applications are the major constraints that usually prevent the use of BDDs since there is a limited amount of memory available on a machine. One way of overcoming this resource limitation problem is to utilize the memory available on a network of workstations (NOW). This requires the distribution of the computation and memory requirements involved in the manipulation of BDDs over a NOW. In this thesis, an algorithm for manipulating BDDs on a NOW is presented. The algorithm makes use of the breadth-first technique to manipulate BDDs so that various BDD operations can be started concurrently on the different workstations on the NOW. The design and implementation details of the distributed BDD package are described. The various approaches considered in order to optimize the performance of the algorithm are also discussed. Experimental results demonstrating the performance and capabilities of the distributed package and the benefits of the different optimization approaches are given. / AFRIKAANSE OPSOMMING: Binêre besluitnemingsbome (BBBs) is data strukture wat gebruik word om probleme in verskillende areas van Rekenaarwetenskap, soos by voorbeeld rekenaargesteunde ontwerp en formele verifikasie, op te los. Die tyd- en spasiekoste van BBB-gebaseerde toepassings is die hoofrede waarom BBBs nie altyd gebruik kan word nie; die geheue van ’n enkele is ongelukkig te beperkend. Een manier om hierdie hulpbronprobleem te omseil, is om die gedeelde geheue van die werkstasies in ’n netwerk van werkstasies (Engels: “network of workstations”, oftewel, ’n NOW) te benut. Dit is dus nodig om die berekening en geheuevoorvereistes van die BBB bewerking oor die NOW te versprei. Hierdie tesis bied ’n algoritme aan om BBBs op ’n NOW te hanteer. Die algoritme gebruik die breedte-eerste soektegniek, sodat BBB operasies gelyklopend kan uitvoer. Die details van die ontwerp en implementasie van die verspreide BBB bilbioteek word beskryf. Verskeie benaderings om die gedrag van die biblioteek te optimeer word ook aangespreek. Empiriese resultate wat die werkverrigting en kapasiteit van die biblioteek meet, en wat die uitwerking van die onderskeie optimerings aantoon, word verskaf.

Thesis (MSc)--Stellenbosch University, 2004. / ENGLISH ABSTRACT: It is possible to improve on the accuracy of a single neural network by using an ensemble of diverse and accurate networks. This thesis explores diversity in ensembles and looks at the underlying theory and mechanisms employed to generate and combine ensemble members. Bagging and boosting are studied in detail and I explain their success in terms of well-known theoretical instruments. An empirical evaluation of their performance is conducted and I compare them to a single classifier and to each other in terms of accuracy and diversity. / AFRIKAANSE OPSOMMING: Dit is moontlik om op die akkuraatheid van 'n enkele neurale netwerk te verbeter deur 'n ensemble van diverse en akkurate netwerke te gebruik. Hierdie tesis ondersoek diversiteit in ensembles, asook die meganismes waardeur lede van 'n ensemble geskep en gekombineer kan word. Die algoritmes "bagging" en "boosting" word in diepte bestudeer en hulle sukses word aan die hand van bekende teoretiese instrumente verduidelik. Die prestasie van hierdie twee algoritmes word eksperimenteel gemeet en hulle akkuraatheid en diversiteit word met 'n enkele netwerk vergelyk.

Thesis (MSc) -- Stellenbosch University, 2004. / ENGLISH ABSTRACT: The Internet is fast evolving into a commercial platform that carries a mixture of narrow- and broadband applications such as voice, video, and data. Users expect a certain level of guaranteed service from their service providers and consequently the need exists for efficient Internet traffic engineering to enable better Quality of Service (QoS) capabilities. Multi-protocol Label Switching (MPLS) is a label switching protocol that has emerged as an enabling technology to achieve efficient traffic engineering for QoS management in IP networks. The ability of the MPLS protocol to create explicit virtual connections called Label Switched Paths (LSPs) to carry network traffic significantly enhances the traffic engineering capabilities of communication networks. The MPLS protocol supports two options for explicit LSP selection: offline LSP computation using an optimization method and dynamic route selection where a single node makes use of current available network state information in order to compute an explicit LSP online. This thesis investigates various methods for the selection of explicit bandwidth guaranteed LSPs through dynamic route selection. We address the problem of computing a sequence of optimal LSPs where each LSP can carry a specific traffic demand and we assume that no prior information regarding the future traffic demands are available and that the arrival sequence of LSP requests to the network is unknown. Furthermore, we investigate the rerouting abilities of the online LSP selection methods to perform MPLS failure restoration upon link failure. We propose a new online routing framework known as Least Interference Optimization (LIO) that utilizes the current bandwidth availability and traffic flow distribution to achieve efficient traffic engineering. We present the Least Interference Optimization Algorithm (LIOA) that reduces the interference among competing network flows by balancing the number and quantity of flows carried by a link for the setup of bandwidth guaranteed LSPs in MPLS networks. The LIOA routing strategy is evaluated and compared against well-known routing strategies such as the Minimum Hop Algorithm (MHA), Minimum Interference Routing Algorithm (MIRA), Open Shortest Path First (OSPF) and Constraint Shortest Path First (CSPF) by means of simulation. Simulation results revealed that, for the network topologies under consideration, the routing strategies that employed dynamic network state information in their routing decisions (LIOA, CSPF and MIRA) generally outperformed the routing strategies that only rely on static network information (OSPF and MHA). In most simulation experiments the best performance was achieved by the LIOA routing strategy while the MHA performed the worse. Furthermore we observed that the computational complexity of the MIRA routing strategy does not translate into equivalent performance gains. We employed the online routing strategies for MPLS failure recovery upon link failure. In particular we investigated two aspects to determine the efficiency of the routing strategies for MPLS rerouting: the suitability of the LSP configuration that results due to the establishment of LSPs prior to link failure and the ability of the online routing strategy to reroute failed LSPs upon link failure. Simulation results revealed similar rerouting performance for all online routing strategies under investigation, but a LSP configuration most suitable for online rerouting was observed for the LIOA routing strategy. / AFRIKAANSE OPSOMMING:Die Internet is voordurend besig om te evoleer in 'n medium wat 'n wye reeks moderne kommunikasietegnologiee ondersteun, insluitende telefoon, video en data. Internet gebruikers verwag gewaarborgde diens van hul diensverskaffers en daar bestaan dus 'n vraag na doeltreffende televerkeerbeheer vir gewaarborgde Internet diensgehalte. Multiprotokol Etiketskakeling (MPLS) is 'n etiketskakeling protokol wat doeltreffende televerkeerbeheer en diensgehalte moontlik maak deur die eksplisiete seleksie van virtuele konneksies vir die transmissie van netwerkverkeer in Internetprotokol (IP) netwerke. Hierdie virtuele konneksies staan bekend as etiketgeskakelde paaie. Die MPLS protokol ondersteun tans twee moontlikhede vir eksplisiete seleksie van etiketgeskakelde paaie: aflyn padberekening met behulp van optimeringsmetodes en dinamiese aanlyn padseleksie waar 'n gekose node 'n eksplisiete pad bereken deur die huidige stand van die netwerk in ag te neem. In hierdie tesis word verskeie padseleksiemetodes vir die seleksie van eksplisiete bandwydte-gewaarborgde etiketgeskakelde paaie deur mid del van dinamiese padseleksie ondersoek. Die probleem om 'n reeks optimale etiketgeskakelde paaie te bereken wat elk 'n gespesifeerde verkeersaanvraag kan akkommodeer word aangespreek. Daar word aanvaar dat geen informasie in verband met die toekomstige verkeersaanvraag bekend is nie en dat die aankomsvolgorde van etiketgeskakelde pad verso eke onbekend is. Ons ondersoek verder die herroeteringsmoontlikhede van die aanlyn padseleksiemetodes vir MPLS foutrestorasie in die geval van skakelonderbreking. Vir hierdie doel word 'n nuwe aanlyn roeteringsraamwerk naamlik Laagste Inwerking Optimering (LIO) voorgestel. LIO benut die huidige beskikbare bandwydte en verkeersvloeidistribusie van die netwerk om doeltreffende televerkeerbeheer moontlik te maak. Ons beskryf 'n Laagste Inwerking Optimering Algoritme (LIOA) wat die inwerking tussen kompeterende verkeersvloei verminder deur 'n balans te handhaaf tussen die aantal en kwantiteit van die verkeersvloeistrome wat gedra word deur elke netwerkskakel. Die LIOA roeteringstrategie word geevalueer met behulp van simulasie en die resultate word vergelyk met ander bekende roeteringstrategiee insluitende die Minimum Node Algorithme (MHA), die Minimum Inwerking Algoritme (MIRA), die Wydste Kortste Pad Eerste Algoritme (OSPF) en die Beperkte Kortste Pad Eerste Algoritme (CSPF). Die resultate van die simulasie-eksperimente to on dat, vir die netwerk topologiee onder eksperimentasie, die roeteringstratgiee wat roeteringsbesluite op dinamiese netwerk informasie baseer (LIOA, MIRA, CSPF) oor die algemeen beter vaar as die wat slegs staatmaak op statiese netwerkinformasie (MHA, OSPF). In die meeste simulasie-eksperimente vaar die LIOA roeteringstrategie die beste en die MHA roeteringstrategie die slegste. Daar word verder waargeneem dat die komputasiekomplesiteit van die MIRA roeteringstrategie nie noodwendig weerspieel word in die sukses van roeteringsuitkoms nie. In die geval waar die aanlyn roeteringstrategiee aangewend word vir MPLS foutrestorasie, toon die resultate van simulasie-eksperimente dat al die roeteringstrategiee min of meer dieselfde uitkoms lewer ten opsigte van herroetering van onderbreekte verkeersvloei. Die konfigurasie van etiketgeskakelde paaie deur die LIOA roeteringstrategie voor skakelonderbreking is egter die geskikste vir televerkeer herroetering na skakelonderbreking

Thesis (MSc)--Stellenbosch University, 2002. / ENGLISH ABSTRACT: The Internet is evolving into a commercial platform requiring enhanced protocols and an expanded physical infrastructure allowing a better delivery from IP. Multi-protocol Label Switching (MPLS) is a technology enabling traffic engineering and virtual private network (VPN) provisioning. MPLS achieves traffic engineering by carrying the traffic over virtual connections called Label Switched Paths (LSPs) which are engineered based on QoS requirements such as delay, jitter and packet loss minimization or throughput maximization. This thesis proposes path finding and traffic distribution methods to be deployed in MPLS networks for traffic engineering LSPs. A flow optimization model based on a pre-planned routing approach separating path finding and traffic distribution is presented. This model is augmented by a threshold routing approach which routes the traffic based on thresholds expressing the maximum load level reached by network links. This routing approach moves the traffic away from thresholdmarked links to achieve low-utilized links/paths. The performance and routing capabilities of these methods are evaluated through designed software. A routing architecture implementing a two-layer signalling model for MPLS network is proposed and evaluated through simulation. v / AFRIKAANSE OPSOMMING:Die verandering van die Internet in 'n kommersiele platform met verbeterde protokolle en 'n uitgebreide fisieke infrastruktuur stel die internetprotokol (IP) in staat tot beter lewering. Multiprotokol- etiketskakeling (MPLS), is 'n tegnologie vir die voorsiening van televerkeerbeheer en virtuele privaatnetwerke (VPN). MPLS verskaf televerkeerbeheer deur die verkeer te dra oar virtuele konneksies, wat bekend staan as etiketgeskakelde paaie, waarvan die ontwerp gebaseer is op vereistes vir diensgehalte soos vertraging, ritteling en die minimering van pakketverlies of maksimering van deurvoer. Hierdie tesis stel nuwe padvind- en verkeerdistribusiemetodes voor wat aangewend word in MPLSnetwerke om etiketgeskakelde paaie te beheer. 'n Model vir vloei-optimering-gebaseer op voorafbeplande roetering wat padvinding en verkeerdistribusie skei-word aangebied. Hierdie model word uitgebrei deur 'n benadering van drempelroetering wat die verkeer roeteer en gebaseer is op drempels wat die maksimum ladingsvlak voorstel wat bereik kan word deur netwerkskakels. Hierdie roeteringsbenadering skuif die verkeer weg van drempelgemerkte skakels en bereik daardeur laaggebruikte skakelsjpaaie. Die prestasie en roeteringsvaardigheid van hierdie metodes word gevalueer deur selfontwikkelde programmatuur. 'n Argitektuur vir roetering wat 'n dubbellaagseinmodel implementeer vir 'n MPLS-netwerk, word aangebied en gevalueer met simulasie.