Search
Search Results
-
Enabling Floating-Point Arithmetic in the Coq Proof Assistant
Floating-point arithmetic is a well-known and extremely efficient way of performing approximate computations over the real numbers. Although it...
-
Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant
We present an abstract development of Gödel’s incompleteness theorems, performed with the help of the Isabelle/HOL proof assistant. We analyze...
-
Experiences from Exporting Major Proof Assistant Libraries
The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving....
-
A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry
We present an automatic theorem prover for projective incidence geometry. This prover does not consider coordinates. Instead, it follows a...
-
A proof system of the CaIT calculus
The Internet of Things (IoT) can realize the interconnection of people, machines, and things anytime, anywhere. Most of the existing research mainly...
-
Formal Verification of Completeness Theorem in Grundlagen der Geometrie
Hilbert’s Grundlagen der Geometrie remains a pivotal work in formal proof and modern mathematics, influencing geometric reasoning. This paper...
-
A manifesto for applicable formal methods
Recently, formal methods have been used in large industrial organisations (including AWS, Facebook/Meta, and Microsoft) and have proved to be an...
-
The Isabelle/Naproche Natural Language Proof Assistant
is an emerging natural proof assistant that accepts input in the controlled natural language ForTheL....
-
Formal Reasoning Using Distributed Assertions
When a proof system checks a formal proof, we can say that its kernel asserts that the formula is a theorem in a particular logic. We describe a...
-
SimIMA: a virtual Simulink intelligent modeling assistant
Intelligent virtual model assistance is a key challenge in cultivating model-driven engineering proliferation and growth. Such assistance will help...
-
Security requirements specification by formal methods: a research metadata analysis
In recent years, the field of security requirements specification by formal methods has changed radically. The security requirement specification is...
-
Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM
Assurance cases are often required to certify critical systems. The use of formal methods in assurance can improve automation, increase confidence,...
-
On the use of formal methods to model and verify neuronal archetypes
Having a formal model of neural networks can greatly help in understanding and verifying their properties, behavior, and response to external factors...
-
Formalizing the Equivalence of Formal Systems in Propositional Logic in Coq
In the field of artificial intelligence, propositional logic provides a precise and efficient reasoning structure for computers to simulate human...
-
Formal verification of cP systems using Coq
P systems are widely used to solve computationally hard problems. In this study, we formally verify cP systems (P systems with complex objects) in...
-
JEFL: Joint Embedding of Formal Proof Libraries
The heterogeneous nature of the logical foundations used in different interactive proof assistant libraries has rendered discovery of similar...
-
Making an eBPF Virtual Machine Faster on Microcontrollers: Verified Optimization and Proof Simplification
As a revolutionary kernel extension technology, Berkeley Packet Filters (BPF) has been applied for various operating systems from different domains,...
-
A Formal Treatment of Bidirectional Ty**
There has been much progress in designing bidirectional type systems and associated type synthesis algorithms, but mainly on a case-by-case basis. To...
-
CoProver: A Recommender System for Proof Construction
Interactive Theorem Provers (ITPs) are an indispensable tool in the arsenal of formal method experts as a platform for construction and (formal)...
-
Leroy and Blazy Were Right: Their Memory Model Soundness Proof is Automatable
Xavier Leroy and Sandrine Blazy in 2007 conducted a formal verification, using the Coq proof assistant, of a memory model for low-level imperative...