Related papers: Certifying Differential Equation Solutions from Co…
Uncertainty is unavoidable in modeling dynamical systems and it may be represented mathematically by differential inclusions. In the past, we proposed an algorithm to compute validated solutions of differential inclusions; here we provide…
Derandomization techniques are often used within advanced randomized algorithms. In particular, pseudorandom objects, such as hash families and expander graphs, are key components of such algorithms, but their verification presents a…
This paper presents an overview of the verification framework ALICE in its current version 0.7. It is based on the generic theorem prover Isabelle [Pau03a]. Within ALICE a software or hardware component is specified as a state-full…
We consider the problem of how to verify the security of probabilistic oblivious algorithms formally and systematically. Unfortunately, prior program logics fail to support a number of complexities that feature in the semantics and…
Formal programming language semantics are imperative when trying to verify properties of programs in an automated manner. Using a new approach, Din et al. strengthen the ability of reasoning about concurrent programs by proposing a modular…
Auto2 is a recently introduced prover for the proof assistant Isabelle. It is designed to be both highly customizable from within Isabelle, and also have a powerful proof search mechanism. In this paper, we apply auto2 to the verification…
Large language models have recently demonstrated advanced capabilities in solving IMO and Putnam problems; yet their role in research mathematics has remained fairly limited. The key difficulty is verification: suggested proofs may look…
We formalise the basics of the double-pushout approach to graph transformation in the proof assistant Isabelle/HOL and provide associated machine-checked proofs. Specifically, we formalise graphs, graph morphisms and rules, and a definition…
We have developed an automated procedure for symbolic and numerical testing of formulae extracted from the NIST Digital Library of Mathematical Functions (DLMF). For the NIST Digital Repository of Mathematical Formulae, we have developed…
Separation logic is successful for software verification in both theory and practice. Decision procedure for symbolic heaps is one of the key issues. This paper proposes a cyclic proof system for symbolic heaps with general form of…
An Isabelle/HOL formalisation of G\"odel's two incompleteness theorems is presented. The work follows \'Swierczkowski's detailed proof of the theorems using hereditarily finite (HF) set theory. Avoiding the usual arithmetical encodings of…
In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "apply-style" proof scripts since they enable rapid exploration…
Many cyber-physical systems (CPS) are safety-critical, so it is important to formally verify them, e.g. in formal logics that show a model's correctness specification always holds. Constructive Differential Game Logic (CdGL) is such a logic…
Deciding which sub-tool to use for a given proof state requires expertise specific to each ITP. To mitigate this problem, we present PaMpeR, a Proof Method Recommendation system for Isabelle/HOL. Given a proof state, PaMpeR recommends proof…
Automated theorem provers are now commonly used within interactive theorem provers to discharge an increasingly large number of proof obligations. To maintain the trustworthiness of a proof, the automatically found proof must be verified…
This paper introduces a proof calculus for real-analytic differential-algebraic dynamic logic, enabling correct transformations of differential-algebraic equations. Applications include index reductions from differential-algebraic equations…
Computer algebra systems are a great help for mathematical research but sometimes unexpected errors in the software can also badly affect it. As an example, we show how we have detected an error of Mathematica computing determinants of…
We propose an approach for searching for counterexamples of statements about algebraic structures with a medium-sized signature using the Isabelle proof assistant in an efficient, parallel manner. We contribute a Python client Isabelle…
Document preparation systems like LaTeX offer the ability to render mathematical expressions as one would write these on paper. Using LaTeX, LaTeXML, and tools generated for use in the National Institute of Standards (NIST) Digital Library…
This paper explores verification of constituent systems within the context of the Symphony tool platform for Systems of Systems (SoS). Our SoS modelling language, CML, supports various contractual specification elements, such as state…