Computing and Information Systems - Research Publications
Permanent URI for this collection
Search Results
1 - 7 of 7
-
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.
-
ItemLightweight Nontermination Inference with CHCs(SPRINGER INTERNATIONAL PUBLISHING AG, 2021)Non-termination is an unwanted program property (considered a bug) for some software systems, and a safety property for other systems. In either case, automated discovery of preconditions for non-termination is of interest. We introduce NtHorn, a fast lightweight non-termination analyser, able to deduce non-trivial sufficient conditions for non-termination. Using Constrained Horn Clauses (CHCs) as a vehicle, we show how established techniques for CHC program transformation and abstract interpretation can be exploited for the purpose of non-termination analysis. NtHorn is comparable in power to the state-of-the-art non-termination analysis tools, as measured on standard competition benchmark suites (consisting of integer manipulating programs), while typically solving problems an order of magnitude faster.
-
ItemDisjunctive Interval Analysis(SPRINGER INTERNATIONAL PUBLISHING AG, 2021)We revisit disjunctive interval analysis based on the Boxes abstract domain. We propose the use of what we call range decision diagrams (RDDs) to implement Boxes, and we provide algorithms for the necessary RDD operations. RDDs tend to be more compact than the linear decision diagrams (LDDs) that have traditionally been used for Boxes. Representing information more directly, RDDs also allow for the implementation of more accurate abstract operations. This comes at no cost in terms of analysis efficiency, whether LDDs utilise dynamic variable ordering or not. RDD and LDD implementations are available in the Crab analyzer, and our experiments confirm that RDDs are well suited for disjunctive interval analysis.
-
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, symbolic execution and constraints(Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020)Abstract interpretation is a static analysis framework for sound over-approximation of all possible runtime states of a program. Symbolic execution is a framework for reachability analysis which tries to explore all possible execution paths of a program. A shared feature between abstract interpretation and symbolic execution is that each – implicitly or explicitly – maintains constraints during execution, in the form of invariants or path conditions. We investigate the relations between the worlds of abstract interpretation, symbolic execution and constraint solving, to expose potential synergies.
-
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.