Research Articles (Computer Science)

Permanent URI for this collection

https://scholar.sun.ac.za/handle/10019.1/96340

Browse

Browsing Research Articles (Computer Science) by Title

Now showing 1 - 8 of 8
  • Thumbnail Image
    Item
    An assessment of algorithms for deriving failure deterministic finite automata
    (South African Institute of Computer Scientists and Information Technologists, 2017) Nxumalo, Madoda; Kourie, Derrick G.; Cleophas, Loek; Watson, Bruce W.
    Failure deterministic finite automata (FDFAs) represent regular languages more compactly than deterministic finite automata (DFAs). Four algorithms that convert arbitrary DFAs to language-equivalent FDFAs are empirically investigated. Three are concrete variants of a previously published abstract algorithm, the DFA-Homomorphic Algorithm (DHA). The fourth builds a maximal spanning tree from the DFA to derive what it calls a delayed input DFA. A first suite of test data consists of DFAs that recognise randomised sets of finite length keywords. Since the classical Aho-Corasick algorithm builds an optimal FDFA from such a set (and only from such a set), it provides benchmark FDFAs against which the performance of the general algorithms can be compared. A second suite of test data consists of random DFAs generated by a specially designed algorithm that also builds language-equivalent FDFAs, some of which may have non-divergent cycles. These random FDFAs provide (not necessarily tight) lower bounds for assessing the effectiveness of the four general FDFA generating algorithms.
  • Thumbnail Image
    Item
    Comparing leaf and root insertion
    (South African Institute of Computer Scientists and Information Technologists, 2009) Geldenhuys, Jaco; Van der Merwe, Brink
    We consider two ways of inserting a key into a binary search tree: leaf insertion which is the standard method, and root insertion which involves additional rotations. Although the respective cost of constructing leaf and root insertion binary search trees trees, in terms of comparisons, are the same in the average case, we show that in the worst case the construction of a root insertion binary search tree needs approximately 50% of the number of comparisons required by leaf insertion.
  • Thumbnail Image
    Item
    Fast test suite-driven model-based fault localisation with application to pinpointing defects in student programs
    (Springer, 2019) Birch, Geoff; Fischer, Bernd; Poppleton, Michael
    Fault localisation, i.e. the identification of program locations that cause errors, takes significant effort and cost. We describe a fast model-based fault localisation algorithm that, given a test suite, uses symbolic execution methods to fully automatically identify a small subset of program locations where genuine program repairs exist. Our algorithm iterates over failing test cases and collects locations where an assignment change can repair exhibited faulty behaviour. Our main contribution is an improved search through the test suite, reducing the effort for the symbolic execution of the models and leading to speed-ups of more than two orders of magnitude over the previously published implementation by Griesmayer et al. We implemented our algorithm for C programs, using the KLEE symbolic execution engine, and demonstrate its effectiveness on the Siemens TCAS variants. Its performance is in line with recent alternative model-based fault localisation techniques, but narrows the location set further without rejecting any genuine repair locations where faults can be fixed by changing a single assignment. We also show how our tool can be used in an educational context to improve self-guided learning and accelerate assessment. We apply our algorithm to a large selection of actual student coursework submissions, providing precise localisation within a sub-second response time. We show this using small test suites, already provided in the coursework management system, and on expanded test suites, demonstrating the scalability of our approach. We also show compliance with test suites does not reliably grade a class of “almost-correct” submissions, which our tool highlights, as being close to the correct answer. Finally, we show an extension to our tool that extends our fast localisation results to a selection of student submissions that contain two faults.
  • Thumbnail Image
    Item
    Identification of broadly neutralizing antibody epitopes in the HIV-1 envelope glycoprotein using evolutionary models
    (BioMed Central, 2013-12-02) Lacerda, Miguel; Moore, Penny L.; Ngandu, Nobubelo K.; Seaman, Michael; Gray, Elin S.; Murrell, Ben; Krishnamoorthy, Mohan; Nonyane, Molati; Madiga, Maphuti; Wibmer, Constantinos K.; Sheward, Daniel; Bailer, Robert T.; Gao, Hongmei; Greene, Kelli M.; Karim, Salim S. A.; Mascola, John R.; Korber, Bette T. M.; Montefiori, David C.; Morris, Lynn; Williamson, Carolyn; Seoighe, Cathal; the CAVD-NSDP Consortium
    Background Identification of the epitopes targeted by antibodies that can neutralize diverse HIV-1 strains can provide important clues for the design of a preventative vaccine. Methods We have developed a computational approach that can identify key amino acids within the HIV-1 envelope glycoprotein that influence sensitivity to broadly cross-neutralizing antibodies. Given a sequence alignment and neutralization titers for a panel of viruses, the method works by fitting a phylogenetic model that allows the amino acid frequencies at each site to depend on neutralization sensitivities. Sites at which viral evolution influences neutralization sensitivity were identified using Bayes factors (BFs) to compare the fit of this model to that of a null model in which sequences evolved independently of antibody sensitivity. Conformational epitopes were identified with a Metropolis algorithm that searched for a cluster of sites with large Bayes factors on the tertiary structure of the viral envelope. Results We applied our method to ID50 neutralization data generated from seven HIV-1 subtype C serum samples with neutralization breadth that had been tested against a multi-clade panel of 225 pseudoviruses for which envelope sequences were also available. For each sample, between two and four sites were identified that were strongly associated with neutralization sensitivity (2ln(BF) > 6), a subset of which were experimentally confirmed using site-directed mutagenesis. Conclusions Our results provide strong support for the use of evolutionary models applied to cross-sectional viral neutralization data to identify the epitopes of serum antibodies that confer neutralization breadth.
  • Thumbnail Image
    Item
    Java Pathfinder at SV-COMP 2019 (Competition Contribution)
    (Springer, 2019) Artho, Cyrille; Visser, Willem
    This paper gives a brief overview of Java Pathfinder, or jpf-core. We describe the architecture of JPF, its strengths, and how it was set up for SV-COMP 2019.
  • Thumbnail Image
    Item
    Revival of the magnetar PSR J1622–4950 : observations with MeerKAT, Parkes, XMM-Newton, Swift, Chandra, and NuSTAR
    (American Astronomical Society, 2018) Camilo, F.; Serylak, M.; Buchner, S.; Merryfield, M.; Kaspi, V. M.; Archibald, R. F.; Bailes, M.; Jameson, A.; Van Straten, W.; Sarkissian, J.; Reynolds, J. E.; Johnston, S.; Hobbs, G.; Abbott, T. D.; Adam, R. M.; Adams, G. B.; Alberts, T.; Andreas, R.; Asad, K. M. B.; Baker, D. E.; Baloyi, T.; Bauermeister, E. F.; Baxana, T.; Bennett, T. G. H.; Bernardi, G.; Booisen, D.; Booth, R. S.; Botha, D. H.; Boyana, L.; Brederode, L. R. S.; Burge, J. P.; Cheetham, T.; Conradie, J.; Conradie, J. P.; Davidson, D. B.; De Bruin, G.; De Swardt, B.; De Villiers, C.; De Villiers, D. I. L.; De Villiers, M. S.; De Villiers, W.; De Waal, C.; Dikgale, M. A.; Du Toit, G.; Du Toit, L. J.; Esterhuyse, S. W. P.; Fanaroff, B.; Fataar, S.; Foley, A. R.; Foste, G.; Fourie, D.; Gamatham, R.; Gatsi, T.; Geschke, R.; Goedhart, S.; Grobler, T. L.; Gumede, S. C.; Hlakola, M. J.; Hokwana, A.; Hoorn, D. H.; Horn, D.; Horrell, J.; Hugo, B.; Isaacson, A.; Jacobs, O.; Jansen Van Rensburg, J. P.; Jonas, J. L.; Jordaan, B.; Joubert, A.; Joubert, F.; Jozsa, G. I. G.; Julie, R.; Julius, C. C.; Kapp, F.; Karastergiou, A.; Karels, F.; Kariseb, M.; Karuppusamy, R.; Kasper, V.; Knox-Davies, E. C.; Koch, D.; Kotze, P. P. A.; Krebs, A.; Kriek, N.; Kriel, H.; Kusel, T.; Lamoor, S.; Lehmensiek, R.; Liebenberg, D.; Liebenberg, I.; Lord, R. T.; Lunsky, B.; Mabombo, N.; Macdonald, T.; Macfarlane, P.; Madisa, K.; Mafhungo, L.; Magnus, L. G.; Magozore, C.; Mahgoub, O.; Main, J. P. L.; Makhathini, S.; Malan, J. A.; Malgas, P.; Manley, J. R.; Manzini, M.; Marais, L.; Marais, N.; Marais, S. J.; Maree, M.; Martens, A.; Matshawule, S. D.; Matthysen, N.; Mauch, T.; McNally, L. D.; Merry, B.; Millenaar, R. P.; Mjikelo, C.; Mkhabela, N.; Mnyandu, N.; Moeng, I. T.; Mokone, O. J.; Monama, T. E.; Montshiwa, K.; Moss, V.; Mphego, M.; New, W.; Ngcebetsha, B.; Ngoasheng, K.; Niehaus, H.; Ntuli, P.; Nzama, A.; Obies, F.; Obrocka, M.; Ockards, M. T.; Olyn, C.; Oozeer, N.; Otto, A. J.; Padayachee, Y.; Passmoor, S.; Patel, A. A.; Paula, S.; Peens-Hough, A.; Pholoholo, B.; Prozesky, P.; Rakoma, S.; Ramaila, A. J. T.; Rammala, I.; Ramudzuli, Z. R.; Rasivhaga, M.; Ratcliffe, S.; Reader, H. C.; Renil, R.; Richter, L.; Robyntjies, A.; Rosekrans, D.; Rust, A.; Salie, S.; Sambu, N.; Schollar, C. T. G.; Schwardt, L.; Seranyane, S.; Sethosa, G.; Sharpe, C.; Siebrits, R.; Sirothia, S. K.; Slabber, M. J.; Smirnov, O.; Smith, S.; Sofeya, L.; Songqumase, N.; Spann, R.; Stappers, B.; Steyn, D.; Steyn, T. J.; Strong, R.; Struthers, A.; Struthers, A.; Stuart, C.; Sunnylall, P.; Swart, P. S.; Taljaard, B.; Tasse, C.; Taylor, G.; Theron, I. P.; Thondikulam, V.; Thorat, K.; Tiplady, A.; Toruvanda, O.; Van Aardt, J.; Van Balla, T.; Van den Heever, L.; Van der Byl, A.; Van der Merwe, C.; Van der Merwe, P.; Van Niekerk, P. C.; Van Rooyen, R.; Van Staden, J. P.; Van Tonder, V.; Van Wyk, R.; Wait, I.; Walker, A. L.; Wallace, B.; Welz, M.; Williams, L. P.; Xaia, B.; Young, N.; Zitha, S.
    New radio (MeerKAT and Parkes) and X-ray (XMM-Newton, Swift, Chandra, and NuSTAR) observations of PSR J1622–4950 indicate that the magnetar, in a quiescent state since at least early 2015, reactivated between 2017 March 19 and April 5. The radio flux density, while variable, is approximately 100× larger than during its dormant state. The X-ray flux one month after reactivation was at least 800× larger than during quiescence, and has been decaying exponentially on a 111 ± 19 day timescale. This high-flux state, together with a radio-derived rotational ephemeris, enabled for the first time the detection of X-ray pulsations for this magnetar. At 5%, the 0.3–6 keV pulsed fraction is comparable to the smallest observed for magnetars. The overall pulsar geometry inferred from polarized radio emission appears to be broadly consistent with that determined 6–8 years earlier. However, rotating vector model fits suggest that we are now seeing radio emission from a different location in the magnetosphere than previously. This indicates a novel way in which radio emission from magnetars can differ from that of ordinary pulsars. The torque on the neutron star is varying rapidly and unsteadily, as is common for magnetars following outburst, having changed by a factor of 7 within six months of reactivation.
  • Thumbnail Image
    Item
    Symbolic pathfinder for SV-COMP (Competition Contribution)
    (Springer, 2019) Noller, Yannic; Pasareanu, Corina S.; Fromherz, Aymeric; Le, Xuan-Bach D.; Visser, Willem
    This paper describes the benchmark entry for Symbolic Pathfinder, a symbolic execution tool for Java bytecode. We give a brief description of the tool and we describe the particular run configuration that was used in the SV-COMP competition. Furthermore, we comment on the competition results and we outline some directions for future work.
  • Thumbnail Image
    Item
    Tool support for correctness-by-construction
    (Springer, 2019) Runge, Tobias; Schaefer, Ina; Cleophas, Loek; Thum, Thomas; Kourie, Derrick; Watson, Bruce W.
    Correctness-by-Construction (CbC) is an approach to incrementally create formally correct programs guided by pre- and postcondition specifications. A program is created using refinement rules that guarantee the resulting implementation is correct with respect to the specification. Although CbC is supposed to lead to code with a low defect rate, it is not prevalent, especially because appropriate tool support is missing. To promote CbC, we provide tool support for CbC-based program development. We present CorC, a graphical and textual IDE to create programs in a simple while-language following the CbC approach. Starting with a specification, our open source tool supports CbC developers in refining a program by a sequence of refinement steps and in verifying the correctness of these refinement steps using the theorem prover KeY. We evaluated the tool with a set of standard examples on CbC where we reveal errors in the provided specification. The evaluation shows that our tool reduces the verification time in comparison to post-hoc verification.