James H. Davenport

James H. Davenport, Matthew England, Scott McCallum

This paper presents two enhancements to cylindrical algebraic decomposition (CAD) based quantifier elimination (QE) for cases in which multiple equational constraints are present in the given input formula $ϕ^*$. The first enhancement provides more detail in the output when there is a conceptual partition of the set of variables of $ϕ^*$ into parameters and unknowns. In such cases, we describe how to partition the parameter space so that: (1) in each open set of the partition the number $ν$ of associated unknowns is a finite constant or is infinite; and (2) for each such open set for which $ν$ is finite, an expression for the unknowns in terms of the parameters is provided. The second enhancement is an efficiency gain achievable in certain situations. Indeed, when certain conditions are met, the second CAD equational projection step can be reduced more significantly than is supported by the prior existing theory. Relevant theorems and worked examples for both enhancements are provided. Application areas include approximation theory, cuspidal manipulator classification, and biological/chemical systems.

Alexandra Gkolia, Nikhil Fernandes, Nicolas Pizzo et al.

The sudden change of moving the majority of teaching online at Universities due to the global Covid-19 pandemic has caused an increased amount of workload for academics. One of the contributing factors is answering a high volume of queries coming from students. As these queries are not limited to the synchronous time frame of a lecture, there is a high chance of many of them being related or even equivalent. One way to deal with this problem is to cluster these questions depending on their topic. In our previous work, we aimed to find an improved method of clustering that would give us a high efficiency, using a recurring LDA model. Our data set contained questions posted online from a Computer Science course at the University of Bath. A significant number of these questions contained code excerpts, which we found caused a problem in clustering, as certain terms were being considered as common words in the English language and not being recognised as specific code terms. To address this, we implemented tagging of these technical terms using Python, as part of preprocessing the data set. In this paper, we explore the realms of tagging data sets, focusing on identifying code excerpts and providing empirical results in order to justify our reasoning.

Antonio Cerone, Markus Roggenbach, James Davenport et al.

This white paper argues that formal methods need to be better rooted in higher education curricula for computer science and software engineering programmes of study. To this end, it advocates (i) improved teaching of formal methods; (ii) systematic highlighting of formal methods within existing, `classical' computer science courses; and (iii) the inclusion of a compulsory formal methods course in computer science and software engineering curricula. These recommendations are based on the observations that (a) formal methods are an essential and cost-effective means to increase software quality; however (b) computer science and software engineering programmes typically fail to provide adequate training in formal methods; and thus (c) there is a lack of computer science graduates who are qualified to apply formal methods in industry. This white paper is the result of a collective effort by authors and participants of the 1st International Workshop on "Formal Methods, Fun for Everybody" which was held in Bergen, Norway, 2-3 December 2019. As such, it represents insights based on learning and teaching computer science and software engineering (with or without formal methods) at various universities across Europe.

Nikhil Fernandes, Alexandra Gkolia, Nicolas Pizzo et al.

There has been an increasingly popular trend in Universities for curriculum transformation to make teaching more interactive and suitable for online courses. An increase in the popularity of online courses would result in an increase in the number of course-related queries for academics. This, coupled with the fact that if lectures were delivered in a video on demand format, there would be no fixed time where the majority of students could ask questions. When questions are asked in a lecture there is a negligible chance of having similar questions repeatedly, but asynchronously this is more likely. In order to reduce the time spent on answering each individual question, clustering them is an ideal choice. There are different unsupervised models fit for text clustering, of which the Latent Dirichlet Allocation model is the most commonly used. We use the Hierarchical Dirichlet Process to determine an optimal topic number input for our LDA model runs. Due to the probabilistic nature of these topic models, the outputs of them vary for different runs. The general trend we found is that not all the topics were being used for clustering on the first run of the LDA model, which results in a less effective clustering. To tackle probabilistic output, we recursively use the LDA model on the effective topics being used until we obtain an efficiency ratio of 1. Through our experimental results we also establish a reasoning on how Zeno's paradox is avoided.

James H. Davenport

Formal methods have been largely thought of in the context of safety-critical systems, where they have achieved major acceptance. Tens of millions of people trust their lives every day to such systems, based on formal proofs rather than ``we haven't found a bug'' (yet!). Why is ``we haven't found a bug'' an acceptable basis for systems trusted with hundreds of millions of people's personal data? This paper looks at some of the issues in CyberSecurity, and the extent to which formal methods, ranging from ``fully verified'' to better tool support, could help. Alas The Royal Society (2016) only recommended formal methods in the limited context of ``safety critical applications'': we suggest this is too limited.

Tom Crick, James H. Davenport, Alastair Irons et al.

This paper presents a national case study-based analysis of the numerous dimensions to cybersecurity education and how they are prioritised, implemented and accredited; from understanding the interaction of hardware and software, moving from theory to practice (and vice versa), to human factors, policy and politics (as well as various other important facets). A multitude of model curricula and recommendations have been presented and discussed in international fora in recent years, with varying levels of impact on education, policy and practice. This paper address three key questions: i) what is taught and what should be taught for cybersecurity to general computer science students; ii) should cybersecurity be taught stand-alone or in an integrated manner to general computer science students; and iii) can accreditation by national professional, statutory and regulatory bodies enhance the provision of cybersecurity within a body's jurisdiction? Evaluating how cybersecurity is taught in all aspects of computer science is clearly a task of considerable size, one that is beyond the scope of this paper. Instead a case study-based research approach -- primarily focusing on the UK -- has been adopted to evaluate the evidence of the teaching of cybersecurity within general computer science to university-level students. Thus, in the context of widespread international computer science/engineering curriculum reform, what does this need to embed cybersecurity knowledge and skills mean more generally for institutions and educators, and how can we teach this subject more effectively? Through this UK case study, and by contrasting with related initiatives in the US, we demonstrate the positive effect that national accreditation requirements can have, and offer some recommendations both for future research and curriculum developments.

Zongyan Huang, Matthew England, David Wilson et al.

Cylindrical Algebraic Decomposition (CAD) is a key tool in computational algebraic geometry, best known as a procedure to enable Quantifier Elimination over real-closed fields. However, it has a worst case complexity doubly exponential in the size of the input, which is often encountered in practice. It has been observed that for many problems a change in algorithm settings or problem formulation can cause huge differences in runtime costs, changing problem instances from intractable to easy. A number of heuristics have been developed to help with such choices, but the complicated nature of the geometric relationships involved means these are imperfect and can sometimes make poor choices. We investigate the use of machine learning (specifically support vector machines) to make such choices instead. Machine learning is the process of fitting a computer model to a complex function based on properties learned from measured data. In this paper we apply it in two case studies: the first to select between heuristics for choosing a CAD variable ordering; the second to identify when a CAD problem instance would benefit from Groebner Basis preconditioning. These appear to be the first such applications of machine learning to Symbolic Computation. We demonstrate in both cases that the machine learned choice outperforms human developed heuristics.