Zobrazeno 1 - 10
of 133
pro vyhledávání: '"Reger, Giles"'
Publikováno v:
Principles of Systems Design 2022, Lecture Notes in Computer Science, vol 13660. Springer, Cham
Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this paper we survey our work on integrating induction directly into the saturation-based proof search framework of fir
Externí odkaz:
http://arxiv.org/abs/2402.18954
Software performance testing requires a set of inputs that exercise different sections of the code to identify performance issues. However, running tests on a large set of inputs can be a very time-consuming process. It is even more problematic when
Externí odkaz:
http://arxiv.org/abs/2205.14749
Autor:
Reger, Giles
Publikováno v:
EPTCS 311, 2019, pp. 37-41
I argue that the most interesting goal facing researchers in automated reasoning is being able to solve problems that cannot currently be solved by existing tools and methods. This may appear obvious, and is clearly not an original thought, but focus
Externí odkaz:
http://arxiv.org/abs/1912.12958
Autor:
Dawes, Joshua Heneage, Reger, Giles
Techniques for runtime verification often utilise specification languages that are (i) reasonably expressive, and (ii) relatively abstract (i.e. they operate on a level of abstraction that separates them from the system being monitored). Inspired by
Externí odkaz:
http://arxiv.org/abs/1806.02621
Autor:
Reger, Giles
Publikováno v:
EPTCS 254, 2017, pp. 1-14
This paper presents a proposal (story) of how statically detecting unreachable objects (in Java) could be used to improve a particular runtime verification approach (for Java), namely parametric trace slicing. Monitoring algorithms for parametric tra
Externí odkaz:
http://arxiv.org/abs/1708.07228
This paper attempts to address the question of how best to assure the correctness of saturation-based automated theorem provers using our experience developing the theorem prover Vampire. We describe the techniques we currently employ to ensure that
Externí odkaz:
http://arxiv.org/abs/1704.03391
Modern saturation-based Automated Theorem Provers typically implement the superposition calculus for reasoning about first-order logic with or without equality. Practical implementations of this calculus use a variety of literal selections and term o
Externí odkaz:
http://arxiv.org/abs/1604.08055
This work extends the existing MACE-style finite model finding approach to multi-sorted first order logic. This existing approach iteratively assumes increasing domain sizes and encodes the related ground problem as a SAT problem. When moving to the
Externí odkaz:
http://arxiv.org/abs/1604.08040
This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also conta
Externí odkaz:
http://arxiv.org/abs/1510.04821
This report documents the program and the outcomes of Dagstuhl Seminar 22451 "Principles of Contract Languages". At the seminar, participants discussed the fundamental aspects of software contracts. Topics included the format and expressiveness of co
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::372e96df61c3da76341f162bd7a37d7d