Research Articles (Computer Science)
Permanent URI for this collection
Browse
Recent Submissions
- ItemTool 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.
- ItemJava Pathfinder at SV-COMP 2019 (Competition Contribution)(Springer, 2019) Artho, Cyrille; Visser, WillemThis 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.
- ItemSymbolic pathfinder for SV-COMP (Competition Contribution)(Springer, 2019) Noller, Yannic; Pasareanu, Corina S.; Fromherz, Aymeric; Le, Xuan-Bach D.; Visser, WillemThis 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.
- ItemFast test suite-driven model-based fault localisation with application to pinpointing defects in student programs(Springer, 2019) Birch, Geoff; Fischer, Bernd; Poppleton, MichaelFault 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.
- ItemComparing leaf and root insertion(South African Institute of Computer Scientists and Information Technologists, 2009) Geldenhuys, Jaco; Van der Merwe, BrinkWe 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.