Computing and Information Systems - Research Publications
Permanent URI for this collection
Search Results
1 - 10 of 15
-
ItemNo Preview AvailableProgramming to Learn: Logic and Computation from a Programming Perspective(Association for Computing Machinery, 2022-07-07)Programming problems are commonly used as a learning and assessment activity for learning to program. We believe that programming problems can be effective for broader learning goals. In our large-enrolment course, we have designed special programming problems relevant to logic, discrete mathematics, and the theory of computation, and we have used them for formative and summative assessment. In this report, we reflect on our experience. We aim to leverage our students' programming backgrounds by offering a code-based formalism for our mathematical syllabus. We find we can translate many traditional questions into programming problems of a special kind - calling for 'programs' as simple as a single expression, such as a formula or automaton represented in code. A web-based platform enables self-paced learning with rapid contextual corrective feedback, and helps us scale summative assessment to the size of our cohort. We identify several barriers arising with our approach and discuss how we have attempted to negate them. We highlight the potential of programming problems as a digital learning activity even beyond a logic and computation course.
-
ItemString Abstract Domains and Their Combination(SPRINGER INTERNATIONAL PUBLISHING AG, 2022)We survey recent developments in string static analysis, with an emphasis on how string abstract domains can be combined. The paper has formed the basis for an invited presentation given to LOPSTR 2021 and PPDP 2021.
-
ItemTeaching Simple Constructive Proofs with Haskell Programs(OPEN PUBL ASSOC, 2022)In recent years we have explored using Haskell alongside a traditional mathematical formalism in our large-enrolment university course on topics including logic and formal languages, aiming to offer our students a programming perspective on these mathematical topics. We have found it possible to offer almost all formative and summative assessment through an interactive learning platform, using Haskell as a lingua franca for digital exercises across our broad syllabus. One of the hardest exercises to convert into this format are traditional written proofs conveying constructive arguments. In this paper we reflect on the digitisation of this kind of exercise. We share many examples of Haskell exercises designed to target similar skills to written proof exercises across topics in propositional logic and formal languages, discussing various aspects of the design of such exercises. We also catalogue a sample of student responses to such exercises. This discussion contributes to our broader exploration of programming problems as a flexible digital medium for learning and assessment.
-
ItemAbstract Interpretation over Non-Lattice Abstract Domains(Springer, 2013)The classical theoretical framework for static analysis of programs is abstract interpretation. Much of the power and elegance of that framework rests on the assumption that an abstract domain is a lattice. Nonetheless, and for good reason, the literature on program analysis provides many examples of non-lattice domains, including non-convex numeric domains. The lack of domain structure, however, has negative consequences, both for the precision of program analysis and for the termination of standard Kleene iteration. In this paper we explore these consequences and present general remedies.
-
ItemOptimal Bounds for Floating-Point Addition in Constant Time(IEEE, 2019-06)Reasoning about floating-point numbers is notoriously difficult, owing to the lack of convenient algebraic properties such as associativity. This poses a substantial challenge for program analysis and verification tools which rely on precise floating-point constraint solving. Currently, interval methods in this domain often exhibit slow convergence even on simple examples. We present a new theorem supporting efficient computation of exact bounds of the intersection of a rectangle with the preimage of an interval under floating-point addition, in any radix or rounding mode. We thus give an efficient method of deducing optimal bounds on the components of an addition, solving the convergence problem.
-
ItemConstraint Programming for Dynamic Symbolic Execution of JavaScript(Springer, 2019-01-01)Dynamic Symbolic Execution (DSE) combines concrete and symbolic execution, usually for the purpose of generating good test suites automatically. It relies on constraint solvers to solve path conditions and to generate new inputs to explore. DSE tools usually make use of SMT solvers for constraint solving. In this paper, we show that constraint programming (CP) is a powerful alternative or complementary technique for DSE. Specifically, we apply CP techniques for DSE of JavaScript, the de facto standard for web programming. We capture the JavaScript semantics with MiniZinc and integrate this approach into a tool we call Aratha. We use G-Strings, a CP solver equipped with string variables, for solving path conditions, and we compare the performance of this approach against state-of-the-art SMT solvers. Experimental results, in terms of both speed and coverage, show the benefits of our approach, thus opening new research vistas for using CP techniques in the service of program analysis.
-
ItemCombining String Abstract Domains for JavaScript Analysis: An Evaluation(SPRINGER INTERNATIONAL PUBLISHING AG, 2017-01-01)Strings play a central role in JavaScript and similar scripting languages. Owing to dynamic features such as the eval function and dynamic property access, precise string analysis is a prerequisite for automated reasoning about practically any kind of runtime property. Although the literature presents a considerable number of abstract domains for capturing and representing specific aspects of strings, we are not aware of tools that allow flexible combination of string abstract domains. Indeed, support for string analysis is often confined to a single, dedicated string domain. In this paper we describe a framework that allows us to combine multiple string abstract domains for the analysis of JavaScript programs. It is implemented as an extension of SAFE, an open-source static analysis tool. We investigate different combinations of abstract domains that capture various aspects of strings. Our evaluation suggests that a combination of a few, simple abstract domains suffice to outperform the precision of state-of-the-art static analysis tools for JavaScript.
-
ItemSymbolic execution with invariant inlay: Evaluating the potential(IEEE Conference Publishing Services, 2018)Dynamic symbolic execution (DSE) is a non-standard execution mechanism which, loosely, executes a program symbolically and, simultaneously, on concrete input. DSE is attractive because of several uses in software engineering, including the generation of test data suites with large coverage relative to test suite size. However, DSE struggles in the face of execution path explosion, and is often unable to cover certain kinds of difficult-to-reach program points. Invariant inlay is a technique that aims to improve a DSE tool by interspersing code with invariants, generated automatically using off-the-shelf tools for static program analysis using abstract interpretation. To capitalise fully on a static analyzer, invariant inlay applies certain instrumentations and testability transformations to the program source. In this paper we outline the invariant inlay approach, and how we have evaluated the idea, in order to determine its usefulness for programs with complex control flow.
-
ItemLeveraging abstract interpretation for efficient dynamic symbolic execution(IEEE Press, 2017)Dynamic Symbolic Execution (DSE) is a technique to automatically generate test inputs by executing a program with concrete and symbolic values simultaneously. A key challenge in DSE is scalability; executing all feasible program paths is not possible, owing to the potentially exponential or infinite number of paths. Loops are a main source of path explosion, in particular where the number of iterations depends on a program's input. Problems arise because DSE maintains symbolic values that capture only the dependencies on symbolic inputs. This ignores control dependencies, including loop dependencies that depend indirectly on the inputs. We propose a method to increase the coverage achieved by DSE in the presence of input-data dependent loops and loop dependent branches. We combine DSE with abstract interpretation to find indirect control dependencies, including loop and branch indirect dependencies. Preliminary results show that this results in better coverage, within considerably less time compared to standard DSE.
-
ItemString constraint solving: past, present and future(University of Santiago de Compostela, 2020-01-01)String constraint solving is an important emerging field, given the ubiquity of strings over different fields such as formal analysis, automated testing, database query processing, and cybersecurity. This paper highlights the current state-of-the-art for string constraint solving, and identifies future challenges in this field.