This paper describes the authors' experience in teaching a cybersecurity module as part of general MSc courses, rather than a specialist MSc in Cybersecurity. There are three variants of this course which have been fully delivered: a traditional MSc generalist course, fulltime and face-to-face, largely aimed at people without much formal Computer Science training; an MSc-level degree apprenticeship for those sponsored by their employers; a purely on-line part-time MSc generalist course in Computer Science. In addition a version for second-year undergraduates is being delivered for the first time, overlapping with the writing of the paper. There are numerous comments and curriculum suggestions for cybersecurity, and the authors' had to choose what was relevant, what would appeal to the students, and what would leverage the authors' strengths.

Across various countries and jurisdictions, we have seen reports of a “graduate skills gap”, with higher-than-desired graduate unemployment and underemployment, as well as reports from employers that there is a mismatch between the competencies desired by employers and those evidenced by graduates. Graduate employment prospects are related to many complex intersecting factors, including human capital, individual attributes, individual career-building behaviours, labour market factors, and social capital. Alongside the graduate skills gap, there are also reports internationally of a “digital skills gap”, with increasing demand for digital skills and a proclaimed shortage of diverse digital skills evidenced by the workforce. These circumstances appear to promote positive employment outcomes for computing graduates. However, there are reports in many jurisdictions, including the UK, of skills-gap-related issues for computing graduates. In response to these concerns, curricula guidance in the computing and engineering disciplines are increasingly promoting competency-based education (CBE) to develop graduates' work readiness better and, hence, reduce the skills gap. Authentic Assessment, i.e. Assessment that addresses important problems or questions that require students to effectively and creatively apply their knowledge and disciplinary and personal skills, mirroring the challenges faced by adults or professionals in the real-world context, has also been advocated to reduce skills gaps between education and professional life. However, the link between CBE and Authentic Assessment in the computing discipline could benefit from further exploration. This paper explores the relationship between CBE and authentic assessment. Based on the guiding research question: “How can authentic assessment be employed to promote competency in computing degree programmes?”, the paper begins by providing theoretical underpinnings in the form of working definitions for competency and authentic assessment and the link between the two. This paper follows a proof-of-concept research approach conducted by evolutionary prototyping to develop a framework for exploring the relationship between authentic assessment and competency. The paper documents the validation of the framework by applying it to examples of practices from UK universities involved in the study. These illustrative examples show the framework in action. The paper concludes with a discussion of how the framework promotes learner competency development by authentic assessment. This approach has implications for enhancing how computing graduates address digital skills gaps and has the potential to be customised and adopted more broadly across STEM disciplines.

Many factors influence computing graduate employment prospects, including human capital, social capital, individual attributes, individual career-building behaviours, perceived employability, and labour market factors. Whilst most computing graduates go on to be beneficially employed, a small minority remain under-employed or unemployed. Computing curricular recommendations increasingly advocate a competency-based approach to bolster graduates' perceived employability. Hence, the discipline is evolving to incorporate competency-based approaches. However, competency-based can mean any of three different types of competency: technical, personal and professional. Technical Competency is the ability to apply acquired content knowledge and skills to develop solutions to unseen problems. Personal Competency is the personal behaviours and interpersonal skills required for success in the modern workplace. Professional Competency is Technical and Personal combined and applied in a real-world context.

We present results of an in-depth survey of nearly 100 introductory programming (CS1) instructors in 18 countries spanning six continents. Although CS1 is well studied, relatively few broadly-scoped studies have been conducted, and none prior have exceeded regional scale. In addition, CS1 is a notoriously fickle and often changing course, and many might find it beneficial to know what other instructors are doing across the globe; perhaps more so as we continue to understand the impact of the COVID-19 pandemic on computing education and as the effects of Generative AI take hold. Expanding upon several surveys conducted in Australasia, the UK, and Ireland, this survey facilitates a direct comparison of global trends in CS1. The survey goes beyond environmental factors such as languages used, and examines why CS1 instructors teach what they do, in the ways they do. In total the survey spans 84 institutions and 91 courses in which a total of over 40,000 students are enrolled.

Satisfiability modulo theories (SMT) solvers check the satisfiability of quantifier-free first-order logic formulae over different theories. We consider the theory of non-linear real arithmetic where the formulae are logical combinations of polynomial constraints. Here a commonly used tool is the cylindrical algebraic decomposition (CAD) to decompose the real space into cells where the constraints are truth-invariant through the use of projection polynomials. A CAD encodes more information than necessary for checking satisfiability. One approach to address this is to repackage the CAD theory into a search-based algorithm: one that guesses sample points to satisfy the formula, and generalizes guesses that conflict constraints to cylindrical cells around samples which are avoided in the continuing search. Such an approach can lead to a satisfying assignment more quickly, or conclude unsatisfiability with far fewer cells. A notable example of this approach is Jovanović and de Moura's NLSAT algorithm. Since these cells are being produced locally to a sample there is scope to use fewer projection polynomials than the traditional CAD projection. The original NLSAT algorithm reduced the set a little; while Brown's single cell construction reduced it much further still. However, it refines a cell polynomial-by-polynomial, meaning the shape and size of the cell produced depends on the order in which the polynomials are considered. The present paper proposes a method to construct such cells levelwise, i.e. built level-by-level according to a variable ordering instead of polynomial-by-polynomial for all levels. We still use a reduced number of projection polynomials, but can now consider a variety of different reductions and use heuristics to select the projection polynomials in order to optimize the shape of the cell under construction. The new method can thus improve the performance of the NLSAT algorithm. We formulate all the necessary theory that underpins the algorithm as a proof system: while not a common presentation for work in this field, it is valuable in allowing an elegant decoupling of heuristic decisions from the main algorithm and its proof of correctness. We expect the symbolic computation community may find uses for it in other areas too. In particular, the proof system could be a step towards formal proofs for non-linear real arithmetic. This work has been implemented in the SMT-RAT solver and the benefits of the levelwise construction are validated experimentally on the SMT-LIB benchmark library. We also compare several heuristics for the construction and observe that each heuristic has strengths offering potential for further exploitation of the new approach.

McCallum-style Cylindrical Algebra Decomposition (CAD) is a major improvement on the original Collins version, and has had many subsequent advances, notably for total or partial equational constraints. But it suffers from a problem with nullification. The recently-justified Lazard-style CAD does not have this problem. However, transporting the equational constraints work to Lazard-style does reintroduce nullification issues. This paper explains the problem, and the solutions to it, based on the second author’s Ph.D. thesis and the Brown–McCallum improvement to Lazard.

In the UK, a thriving computer science education community of practice is emerging, supported by national and international professional body/learned society specialist interest groups, and being developed through relevant research and practice conferences. A key group within this emerging community of practice are early career academics who are required to overcome significant obstacles in the early stages of their academic career, from developing an independent research career, delivering high quality learning and teaching, continuing their own professional development, alongside wider academic service commitments. Institutional-level, but generally subject-agnostic, support for early career colleagues in the UK is supplemented by nationwide developmental sessions and initiatives such as journal clubs. This poster reports on a developing pilot scheme to support early career CS academics through cross-institutional mentoring from experienced academics, as well as buddying groups of similar career stage colleagues.

There exists a significant gap between the requirements specified within higher education qualifications and the requirements sought by employers. The former, commonly expressed in terms of learning outcomes, provide a measure of capability, of what skills have been learnt (an input measure); the latter, commonly expressed in terms of role descriptions, provide a measure of competency, of what a learner has become skilful in (an output measure). Accreditation traditionally provides a way of translating and embedding industry-relevant content into education programmes but current approaches make fully addressing this requirements gap, referred to here as the Capability-Competency Chasm, very difficult. This paper explores current efforts to address this global challenge, primarily through STEM examples that apply within the United Kingdom and European Union, before proposing a way of bridging this chasm through the use of a 21stCentury (C21) skills taxonomy. The concept of C21 Skills Hours as a new input measurement for learning within qualifications is introduced, and an illustrative example is presented to show the C21 skills taxonomy in action. The paper concludes with a discussion of how such a taxonomy can also be used to support a microcredentialing framework that aligns to existing competency frameworks, enabling formal, non-formal and informal learning to all be recognized. A C21 Skills taxonomy can therefore be used to bridge the gap between capability (input) and competency (output), providing a common language both for learning and demonstrating a skill. This approach has profound implications for addressing current and future skills gaps as well as for supporting a transition to more personalised learning within schools, colleges and universities and more lifelong learning both during and outside of employment.

The early career of a computer science (CS) academic in the UK is increasingly challenging in terms of balancing research aspirations, learning and teaching responsibilities, wider academic service commitments, alongside their own professional development. The development of an early-career CS academic is mediated in part by the strength of the community of practice with which they are able to access and engage. And not just ones that operate within their department or institution; but also communities of practice that exist at a national and international level, often through professional bodies, learned societies and research networks. This poster presents the emerging work-in-progress to address some of these social, cultural and structural challenges in developing a CS education community of practice in the UK. Building on recent work, we identify a number of specific actions and recommendations to supplement the current formal institutional requirements with enhanced national-level academic practice support and professional development, alongside local and regional professional mentoring.

This poster shares the progress related to an evaluation of computer science degree professional body accreditation, framed through an ongoing national review in the United Kingdom (UK). While this review substantially focuses on the UK, other countries, including South Africa and Ireland, have adopted a similar accreditation regime; furthermore, this work is evaluated in the context of the Washington Accord review, taking into account the memorandum's impetus for increased consistency in the UK. In parallel with this international review, the UK's Engineering Council is seeking to enhance and modernise the processes and procedures for degree accreditation (which includes the award of the protected professional title "Chartered Engineer") and the introduction of the new set of accreditation expectations on approved institutions. The review includes consideration of the value of accreditation to universities, students and employers. It was initiated in 2016 following two major national reviews looking at computer science and wider STEM degree accreditation. The intent is to better understand the value of professional body accreditation in computer science, as well as how to co-create improved outcomes for all accreditation stakeholders.

We present a new algorithm for determining the satisfiability of conjunctions of non-linear polynomial constraints over the reals, which can be used as a theory solver for satisfiability modulo theory (SMT) solving for non-linear real arithmetic. The algorithm is a variant of Cylindrical Algebraic Decomposition (CAD) adapted for satisfiability, where solution candidates (sample points) are constructed incrementally, either until a satisfying sample is found or sufficient samples have been sampled to conclude unsatisfiability. The choice of samples is guided by the input constraints and previous conflicts. The key idea behind our new approach is to start with a partial sample; demonstrate that it cannot be extended to a full sample; and from the reasons for that rule out a larger space around the partial sample, which build up incrementally into a cylindrical algebraic covering of the space. There are similarities with the incremental variant of CAD, the NLSAT method of Jovanović and de Moura, and the NuCAD algorithm of Brown; but we present worked examples and experimental results on a preliminary implementation to demonstrate the differences to these, and the benefits of the new approach.

The Institute of Coding (IoC) is a new £40m+ initiative by the UK Government to “transform the digital skills profile of the country”. In the context of widespread national and international educational and economic policy interventions, it responds to the apparently contradictory data that the United Kingdom (UK) has a digital skills shortage across a variety of sectors, yet its higher education system produces computing graduates every year who end up unemployed, or underemployed. The Institute is a large-scale national intervention to address some of the perceived issues with formal educational routes versus industry-focused skills and training, for example: technical skills versus “soft” or “work-ready” skills; industry-readiness versus “deep education”; inclusion and diversity of the current and future technical workforce; and managing expectations for the broad digital, data and computational skills demands of employers across a wide range of economic sectors. Alongside these activities at the higher education-industry interface, we have also seen substantial computer science curriculum reform across the four nations of the UK. In this paper, we outline the background, evidence base and rationale for the IoC (especially within the complex UK policy context); its key themes, current activities and outputs; as well as anticipate its likely impact over the coming years. Furthermore, we reflect on the potential replicability of aspects of the Institute (and related initiatives in the UK) to other nations or regions with similar ambitions to address the “digital skills crisis”.

This Innovative Practice Full Paper explores the diversity of challenges relating to the teaching of cybersecurity in UK higher education degree programmes, through the lens of national policy, to the impact on pedagogy and practice. There is a serious demand for cybersecurity specialists, both in the UK and globally; there is thus significant and growing higher education provision related to specialist undergraduate and postgraduate courses focusing on varying aspects of cybersecurity. To make our digital systems and products more secure, all in IT need to know some cybersecurity - thus, there is a case for depth as well as breadth; this is not a new concern, but it is a growing one. Delivering cybersecurity effectively across general computer science programmes presents a number of challenges related to pedagogy, resources, faculty and infrastructure, as well as responding to industry requirements. Computer science and cognate engineering disciplines are evolving to meet these demands - both at school-level, as well as at university - however, doing so is not without challenges. This paper explores the progress made to date in the UK, building on previous work in cybersecurity education and accreditation by highlighting key challenges and opportunities, as well as identifying a number of enhancement activities for use by the international cybersecurity education community. It frames these challenges through concerns with the quality and availability of underpinning educational resources, the competencies and skills of faculty (especially focusing on pedagogy, progression and assessment), and articulating the necessary technical resources and infrastructure related to delivering rigorous cybersecurity content in general computer science and cognate degrees. Though this critical evaluation of an emerging national case study of cybersecurity education in the UK, we also present a number of recommendations across policy and practice - from pedagogic principles and developing effective cybersecurity teaching practice, challenges in the recruitment, retention and professional development of faculty, to supporting diverse routes into post-compulsory cybersecurity education (and thus, diverse careers) - to provide the foundation for potential replicability and portability to other jurisdictions contemplating related education and skills reform initiatives and interventions.

This poster presents a model for the value provided by professional body accreditation of computer science degree programmes in the United Kingdom (UK). We introduce how one large UK professional computing body -- BCS, The Chartered Institute for IT (BCS)-- addresses degree accreditation, as well as recent changes to content and process. Whilst comparable accreditation regimes exist in a number of other jurisdictions, we provide the opportunity for exploring future extensions to, and the portability of, the UK model.

This Innovative Practice Full 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.

The UK is not the only country with a serious digital skills crisis, but it is one with a formal Government inquiry (The Shadbolt Report) and response. It also has very detailed tracking of people into, through and out of higher education into employment. The Institute of Coding (https://instituteofcoding.org/) is a new £40m+ initiative by the UK Government to transform the digital skills profile of England. It responds to the apparently contradictory data that the country has a digital skills shortage across a variety of sectors, yet has unemployed computing graduates every year. The Institute is a large-scale national intervention funded by Government, industry and universities to address some of the perceived issues with formal education versus industry skills and training, for example: technical skills versus soft skills, industry-readiness versus "deep education", and managing expectations for the diverse digital, data and computational skills demands of employers across a wide range of economic sectors. Its work ranges from the development of specialist, in-demand digital skills to the provision of work experience, employability skills and ensuring work-readiness of computing graduates, and the provision of digital skills for those from a non-digital background. It is also addressing under-representation and under-achievement by a variety of groups, notably women (only 16% of university students) but also ethnic minorities and other groups.

Parallel surveys of introductory programming courses were conducted in Australasia and the UK, with a view to examining the programming languages being used, the preferred integrated development environments (if any), and the reasons for these choices, alongside a number of other key aspects of these courses. This paper summarises some of the similarities and differences between the findings of the two surveys. In the UK, Java is clearly the dominant programming language in introductory programming courses, with Eclipse as the dominant environment. Java was also the dominant language in Australasia six years ago, but now shares the lead with Python; we speculate on the reasons for this. Other differences between the two surveys are equally interesting. Overall, however, there appears to be a reasonable similarity in the way these undergraduate courses are conducted in the UK and in Australasia. While the degree structures differ markedly between and within these regions -- a possible explanation for some of the differences -- some of the similarities are noteworthy and have the potential to provide insight into approaches in other regions and countries.

We consider the problem of determining multiple steady states for positive real values in models of biological networks. Investigating the potential for these in models of the mitogen-activated protein kinases (MAPK) network has consumed considerable effort using special insights into the structure of corresponding models. Here we apply combinations of symbolic computation methods for mixed equality/inequality systems, specifically virtual substitution, lazy real triangularization and cylindrical algebraic decomposition. We determine multistationarity of an 11-dimensional MAPK network when numeric values are known for all but potentially one parameter. More precisely, our considered model has 11 equations in 11 variables and 19 parameters, 3 of which are of interest for symbolic treatment, and furthermore positivity conditions on all variables and parameters.

When using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is likely not the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This observation motivates our article and definition of a Truth Table Invariant CAD (TTICAD). In ISSAC 2013 the current authors presented an algorithm that can efficiently and directly construct a TTICAD for a list of formulae in which each has an equational constraint. This was achieved by generalising McCallum's theory of reduced projection operators. In this paper we present an extended version of our theory which can be applied to an arbitrary list of formulae, achieving savings if at least one has an equational constraint. We also explain how the theory of reduced projection operators can allow for further improvements to the lifting phase of CAD algorithms, even in the context of a single equational constraint. The algorithm is implemented fully in Maple and we present both promising results from experimentation and a complexity analysis showing the benefits of our contributions.

When building a cylindrical algebraic decomposition (CAD) savings can be made in the presence of an equational constraint (EC): an equation logically implied by a formula.

This article makes the key observation that when using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is not always the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This motivates our definition of a Truth Table Invariant CAD (TTICAD). We generalise the theory of equational constraints to design an algorithm which will efficiently construct a TTICAD for a wide class of problems, producing stronger results than when using equational constraints alone. The algorithm is implemented fully in Maple and we present promising results from experimentation.

This article is a continuation of our earlier work [3], which introduced triangular decompositions of semi-algebraic systems and algorithms for computing them. Our new contributions include theoretical results based on which we obtain practical improvements for these decomposition algorithms.

Regular chains and triangular decompositions are fundamental and well-developed tools for describing the complex solutions of polynomial systems. This paper proposes adaptations of these tools focusing on solutions of the real analogue: semi-algebraic systems.

This paper has two parts. In the first part we give a simple and constructive proof that quantifier elimination in real algebra is doubly exponential, even when there is only one free variable and all polynomials in the quantified input are linear. The general result is not new, but we hope the simple and explicit nature of the proof makes it interesting. The second part of the paper uses the construction of the first part to prove some results on the effects of projection order on CAD construction -- roughly that there are CAD construction problems for which one order produces a constant number of cells and another produces a doubly exponential number of cells, and that there are problems for which all orders produce a doubly exponential number of cells. The second of these results implies that there is a true singly vs. doubly exponential gap between the worst-case running times of several modern quantifier elimination algorithms and CAD-based quantifier elimination when the number of quantifier alternations is constant.

Given an elementary function with algebraic branch cuts, we show how to decide which sheet of the associated Riemann surface we are on at any given point. We do this by establishing a correspondence between the Cylindrical Algebraic Decomposition (CAD) of the complex plane defined by the branch cuts and a finite subset of sheets of the Riemann surface. The key advantage is that we no longer have to deal with the difficult 'constant problem'.

Simplification has been long recognised to be a fundamental problem within computer algebra [17]. However, even for the class of elementary functions, it has not been resolved in a satisfactory way.Algorithms were presented in [4, 2] to solve this problem, and it was seen that both methods had their own strengths and weaknesses. Also, not all functions could be handled by either of the methods alone. The current paper continues this line of development by combining the two methods, and reporting on progress made with the various sub-algorithms involved.

In [5], we introduced an algorithm for deciding whether a proposed simplification of elementary functions was correct in the presence of branch cuts. This algorithm used multivalued function simplification followed by verification that the branches were consistent.In [14] an algorithm was presented for zero-testing functions defined by ordinary differential equations, in terms of their power series.The purpose of the current paper is to investigate merging the two techniques. In particular, we will show an explicit reduction to the constant problem [16].

We present an algorithm for simplifying a large class of elementary functions in the presence of branch cuts. This algorithm works by:(a) verifying that the proposed simplification is correct as a simplification of multi-valued functions;(b) decomposing C (or Cn in the case of multivariate simplifications) according to the branch cuts of the relevant functions;(c) checking that the proposed identity is valid on each component of that decomposition.This process can be interfaced to an assume facility, and, if required, can verify that simplifications are valid "almost everywhere".

We describe a new arithmetic model for real algebraic numbers with an exact equality determination. The model represents a real algebraic number as a pair of an arbitrary precision numerical value and a symbolic expression. For the numerical part we currently (another representation could be used) use the dyadic exact real number and for the symbolic part we use a square-free polynomial for the real algebraic number. In this model we show that we can decide exactly the equality of real algebraic numbers.

. Rabin's algorithm is commonly used in computer algebra systems and elsewhere for primality testing. This paper presents an experience with this in the Axiom* computer algebra system. As a result of this experience, we suggest certain strengthenings of the algorithm. Introduction It is customary in computer algebra to use the algorithm presented by Rabin [1980] to determine if numbers are prime (and primes are needed throughout algebraic algorithms). As is well known, a single iteration of Rabin's algorithm, applied to the number N , has probability at most 0.25 of reporting "N is probably prime", when in fact N is composite. For most N , the probability is much less than 0.25. Here, "probability" refers to the fact that Rabin's algorithm begins with the choice of a "random" seed x, not congruent to 0 modulo N . In practice, however, true randomness is hard to achieve, and computer algebra systems often use a fixed set of x --- for example Axiom release 1 uses the set f3; 5; 7; 11;...

This paper explains how Scratchpad solves the problem of presenting a categorical view of factorization in unique factorization domains, i.e. a view which can be propagated by functors such as SparseUnivariatePolynomial or Fraction. This is not easy, as the constructive version of the classical concept of UniqueFactorizationDomain cannot be so propagated. The solution adopted is based largely on Seidenberg's conditions (F) and (P), but there are several additional points that have to be borne in mind to produce reasonably efficient algorithms in the required generality. The consequence of the algorithms and interfaces presented in this paper is that Scratchpad can factorize in any extension of the integers or finite fields by any combination of polynomial, fraction and algebraic extensions: a capability far more general than any other computer algebra system possesses.

We propose a new algorithm, similar to Hermite’s method for the integration of rational functions, for the resolution of Risch differential equations in closed form, or proving that they have no resolution. By requiring more of the presentation of our differential fields (in particular that the exponentials be weakly normalised), we can avoid the introduction of arbitrary constants which have to be solved for later. We also define a class of fields known as exponentially reduced, and show that solutions of Risch differential equations which arise from integrating in these fields satisfy the “natural” degree constraints in their main variables, and we-conjecture (after Risch and Norman) that this is true in all variables.

It is proved that, under the usual restrictions, the denominator of the integral of a purely logarithmic function is the expected one, that is, all factors of the denominator of the integrand have their multiplicity decreased by one. Furthermore, it is determined which new logarithms may appear in the integration.

The factoring of integers is an important problem, and one well-suited to computers, and many algorithms have been proposed for this. This paper compares various algorithms, and discusses the choice of parameters for the algorithms, based on experiments with numbers from 1013 to 1020. We conclude with recommendations on the design of a factoring algorithm.

A number of recent papers have considered the quadratic hash method when the table size is a prime number. This paper shows that, contrary to what is normally assumed, the method can be used for tables whose size is a power of 2 without the usual drawback that the period of search is significantly less than the table size.