LIVIVO - The Search Portal for Life Sciences

zur deutschen Oberfläche wechseln
Advanced search

Search results

Result 1 - 10 of total 26

Search options

  1. Book ; Online: Formal Methods and CyberSecurity

    Davenport, James H.

    2019  

    Abstract: 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 ... ...

    Abstract 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.

    Comment: To appear in "Short Papers FROM 2019"
    Keywords Computer Science - Cryptography and Security ; Computer Science - Software Engineering
    Publishing date 2019-09-07
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  2. Book ; Online: A Poly-algorithmic Approach to Quantifier Elimination

    Davenport, James H. / Tonks, Zak P. / Uncu, Ali K.

    2023  

    Abstract: Cylindrical Algebraic Decomposition (CAD) was the first practical means for doing real quantifier elimination (QE), and is still a major method, with many improvements since Collins' original method. Nevertheless, its complexity is inherently doubly ... ...

    Abstract Cylindrical Algebraic Decomposition (CAD) was the first practical means for doing real quantifier elimination (QE), and is still a major method, with many improvements since Collins' original method. Nevertheless, its complexity is inherently doubly exponential in the number of variables. Where applicable, virtual term substitution (VTS) is more effective, turning a QE problem in $n$ variables to one in $n-1$ variables in one application, and so on. Hence there is scope for hybrid methods: doing VTS where possible then using CAD. This paper describes such a poly-algorithmic implementation, based on the second author's Ph.D. thesis. The version of CAD used is based on a new implementation of Lazard's recently-justified method, with some improvements to handle equational constraints.

    Comment: To appear in Proceedings SYNASC 2023
    Keywords Computer Science - Symbolic Computation ; 68W30 ; I.1.2
    Publishing date 2023-02-13
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  3. Book ; Online: A Practical Overview of Quantum Computing

    Davenport, James H. / Jones, Jessica R. / Thomason, Matthew

    Is Exascale Possible?

    2023  

    Abstract: Despite numerous advances in the field and a seemingly ever-increasing amount of investment, we are still some years away from seeing a production quantum computer in action. However, it is possible to make some educated guesses about the operational ... ...

    Abstract Despite numerous advances in the field and a seemingly ever-increasing amount of investment, we are still some years away from seeing a production quantum computer in action. However, it is possible to make some educated guesses about the operational difficulties and challenges that may be encountered in practice. We can be reasonably confident that the early machines will be hybrid, with the quantum devices used in an apparently similar way to current accelerators such as FPGAs or GPUs. Compilers, libraries and the other tools relied upon currently for development of software will have to evolve/be reinvented to support the new technology, and training courses will have to be rethought completely rather than ``just'' updated alongside them. The workloads we are likely to see making best use of these hybrid machines will initially be few, before rapidly increasing in diversity as we saw with the uptake of GPUs and other new technologies in the past. This will again be helped by the increase in the number of supporting libraries and development tools, and by the gradual re-development of existing software, to make use of the new quantum devices. Unfortunately, at present the problem of error correction is still largely unsolved, although there have been many advances. Quantum computation is very sensitive to noise, leading to frequent errors during execution. Quantum calculations, although asymptotically faster than their equivalents in ``traditional'' HPC, still take time, and while the profiling tools and programming approaches will have to change drastically, many of the skills honed in the current HPC industry will not suddenly become obsolete, but continue to be useful in the quantum era.

    Comment: 9 pages, 0 figures
    Keywords Computer Science - Distributed ; Parallel ; and Cluster Computing ; Computer Science - Emerging Technologies ; B.m ; B.8.1
    Subject code 028
    Publishing date 2023-06-21
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  4. Book ; Online: Lazard-style CAD and Equational Constraints

    Davenport, James H. / Nair, Akshar S. / Sankaran, Gregory K. / Uncu, Ali K.

    2023  

    Abstract: 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. ... ...

    Abstract 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. With a single equational constraint, we can gain the same improvements in Lazard-style as in McCallum-style CAD . Moreover, our approach does not fail where McCallum would due to nullification. Unsurprisingly, it does not achieve the same level of improvement as it does in the non-nullified cases. We also consider the case of multiple equational constraints.

    Comment: 9 pages
    Keywords Computer Science - Symbolic Computation ; 68W30 ; I.1.2
    Publishing date 2023-02-11
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  5. Book ; Conference proceedings: Intelligent computer mathematics

    Davenport, James H

    18th symposium, Calculemus 2011 and 10th international conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011 ; proceedings

    (Lecture notes in computer science : Lecture notes in artificial intelligence ; 6824)

    2011  

    Institution Calculemus
    MKM
    Event/congress Calculemus (18, 2011.07.18-23, Bertinoro) ; International Conference on Mathematical Knowledge Management (10, 2011.07.18-23, Bertinoro) ; MKM (10, 2011.07.18-23, Bertinoro) ; Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (18, 2011.07.18-23, Bertinoro)
    Author's details James H. Davenport ... (eds.)
    Series title Lecture notes in computer science : Lecture notes in artificial intelligence ; 6824
    Keywords Computeralgebra ; Automatisches Beweisverfahren ; Mathematik ; Künstliche Intelligenz ; Wissensmanagement
    Language English
    Size XIII, 312 S.
    Publisher Springer
    Publishing place Heidelberg u.a.
    Document type Book ; Conference proceedings
    Note Literaturangaben
    ISBN 3642226728 ; 9783642226724 ; 9783642226731 ; 3642226736
    Database Former special subject collection: coastal and deep sea fishing

    More links

    Kategorien

    Order via subito

    This service is chargeable due to the Delivery terms set by subito. Orders including an article and supplementary material will be classified as separate orders. In these cases, fees will be demanded for each order.

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  6. Book ; Conference proceedings: Intelligent computer mathematics

    Davenport, James H

    18th symposium, Calculemus 2011 and 10th international conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011 ; proceedings

    (Lecture notes in computer science : Lecture notes in artificial intelligence ; 6824)

    2011  

    Institution Calculemus
    MKM
    Event/congress Calculemus (18, 2011.07.18-23, Bertinoro) ; International Conference on Mathematical Knowledge Management (10, 2011.07.18-23, Bertinoro) ; MKM (10, 2011.07.18-23, Bertinoro) ; Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (18, 2011.07.18-23, Bertinoro)
    Author's details James H. Davenport ... (eds.)
    Series title Lecture notes in computer science : Lecture notes in artificial intelligence ; 6824
    Keywords Computeralgebra ; Automatisches Beweisverfahren ; Mathematik ; Künstliche Intelligenz ; Wissensmanagement
    Language English
    Size XIII, 312 S.
    Publisher Springer
    Publishing place Heidelberg u.a.
    Document type Book ; Conference proceedings
    Note Literaturangaben
    ISBN 3642226728 ; 9783642226724 ; 9783642226731 ; 3642226736
    Database Library catalogue of the German National Library of Science and Technology (TIB), Hannover

    More links

    Kategorien

    Order via subito

    This service is chargeable due to the Delivery terms set by subito. Orders including an article and supplementary material will be classified as separate orders. In these cases, fees will be demanded for each order.

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  7. Book ; Online: Proving UNSAT in SMT

    Abraham, Erika / Davenport, James H. / England, Matthew / Kremer, Gereon

    The Case of Quantifier Free Non-Linear Real Arithmetic

    2021  

    Abstract: We discuss the topic of unsatisfiability proofs in SMT, particularly with reference to quantifier free non-linear real arithmetic. We outline how the methods here do not admit trivial proofs and how past formalisation attempts are not sufficient. We note ...

    Abstract We discuss the topic of unsatisfiability proofs in SMT, particularly with reference to quantifier free non-linear real arithmetic. We outline how the methods here do not admit trivial proofs and how past formalisation attempts are not sufficient. We note that the new breed of local search based algorithms for this domain may offer an easier path forward.

    Comment: Presented at the 3rd International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2021)
    Keywords Computer Science - Logic in Computer Science
    Publishing date 2021-08-11
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  8. Book ; Online: Levelwise construction of a single cylindrical algebraic cell

    Nalbach, Jasper / Ábrahám, Erika / Specht, Philippe / Brown, Christopher W. / Davenport, James H. / England, Matthew

    2022  

    Abstract: Satisfiability Modulo Theories (SMT) solvers check the satisfiability of quantifier-free first-order logic formulas. We consider the theory of non-linear real arithmetic where the formulae are logical combinations of polynomial constraints. Here a ... ...

    Abstract Satisfiability Modulo Theories (SMT) solvers check the satisfiability of quantifier-free first-order logic formulas. 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 real space into cells where the constraints are truth-invariant through the use of projection polynomials. An improved approach 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 fewer cells. A notable example of this approach is Jovanovi\'c and de Moura's NLSAT algorithm. Since these cells are produced locally to a sample we might need 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, the shape and size of the cell produced depends on the order in which the polynomials are considered. This paper proposes a method to construct such cells levelwise, i.e. built level-by-level according to a variable ordering. 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 optimise the shape of the cell under construction. We formulate all the necessary theory as a proof system: while not a common presentation for work in this field, it allows an elegant decoupling of heuristics from the algorithm and its proof of correctness.
    Keywords Computer Science - Symbolic Computation
    Subject code 511
    Publishing date 2022-12-19
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  9. Book ; Online: Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings

    Ábrahám, Erika / Davenport, James H. / England, Matthew / Kremer, Gereon

    2020  

    Abstract: 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 ... ...

    Abstract 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 Jovanovic 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.
    Keywords Computer Science - Symbolic Computation ; Computer Science - Logic in Computer Science
    Subject code 000
    Publishing date 2020-03-12
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  10. Article: Teaching Programming for Mathematical Scientists

    Betteridge, Jack / Chan, Eunice Y.S. / Corless, Robert M. / Davenport, James H. / Grant, James

    Abstract: Over the past thirty years or so the authors have been teaching various programming for mathematics courses at our respective Universities, as well as incorporating computer algebra and numerical computation into traditional mathematics courses. These ... ...

    Abstract Over the past thirty years or so the authors have been teaching various programming for mathematics courses at our respective Universities, as well as incorporating computer algebra and numerical computation into traditional mathematics courses. These activities are, in some important ways, natural precursors to the use of Artificial Intelligence in Mathematics Education. This paper reflects on some of our course designs and experiences and is therefore a mix of theory and practice. Underlying both is a clear recognition of the value of computer programming for mathematics education. We use this theory and practice to suggest good techniques for and to raise questions about the use of AI in Mathematics Education.
    Keywords covid19
    Publisher ArXiv
    Document type Article
    Database COVID19

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

To top