Zobrazeno 1 - 10
of 65
pro vyhledávání: '"Gore, Rajeev"'
We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong L\"ob logic $\sf{iSL}$, an intuitionistic modal logic with a provability interpretation. A novel meas
Externí odkaz:
http://arxiv.org/abs/2309.00486
Autor:
Bride, Hadrien, Cai, Cheng-Hao, Dong, Jin Song, Gore, Rajeev, Hóu, Zhé, Mahony, Brendan, McCarthy, Jim
N-PAT is a new model-checking tool that supports the verification of nested-models, i.e. models whose behaviour depends on the results of verification tasks. In this paper, we describe its operation and discuss mechanisms that are tailored to the eff
Externí odkaz:
http://arxiv.org/abs/2005.05520
We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and fo
Externí odkaz:
http://arxiv.org/abs/1910.05215
Autor:
Goré, Rajeev, Lellmann, Björn
We give a linear nested sequent calculus for the basic normal tense logic Kt. We show that the calculus enables backwards proof-search, counter-model construction and syntactic cut-elimination. Linear nested sequents thus provide the minimal amount o
Externí odkaz:
http://arxiv.org/abs/1907.01270
Autor:
Brizhinev, Dmitry, Goré, Rajeev
We describe a successful attempt to formally verify a simple genetic algorithm written in Java. To this end, we compare several formal verification tools designed for Java, and select Krakatoa as the most appropriate for the task. Based on our experi
Externí odkaz:
http://arxiv.org/abs/1809.03162
Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that manipulate resources such as memory locations. These logics are "abstract" because they are independent of any particular concrete resource model.
Externí odkaz:
http://arxiv.org/abs/1710.10805
Android is an operating system that has been used in a majority of mobile devices. Each application in Android runs in an instance of the Dalvik virtual machine, which is a register-based virtual machine (VM). Most applications for Android are develo
Externí odkaz:
http://arxiv.org/abs/1504.01842
Autor:
Clouston, Ranald, Goré, Rajeev
Nakano's "later" modality, inspired by G\"{o}del-L\"{o}b provability logic, has been applied in type systems and program logics to capture guarded recursion. Birkedal et al modelled this modality via the internal logic of the topos of trees. We show
Externí odkaz:
http://arxiv.org/abs/1501.03293
Autor:
Goré, Rajeev, Thomson, Jimmy
Publikováno v:
The Journal of Symbolic Logic, 2019 Jun 01. 84(2), 439-451.
Externí odkaz:
https://www.jstor.org/stable/26788458
Separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are "abstract" because they are independent of any particular concrete memory model. Their assertion languages, called propositi
Externí odkaz:
http://arxiv.org/abs/1307.5592