5 citations · 8 across the 11 of their papers we have counts for
13 papers
Vibe Coding an LLM-powered Theorem Prover
Zhe Hou
We present Isabellm, an LLM-powered theorem prover for Isabelle/HOL that performs fully automatic proof synthesis. Isabellm works with any local LLM on Ollama and APIs such as Gemi…
A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Quantum Teleportation
Shang-Wei Lin, Tzu-Fan Wang, Yean-Ru Chen +3
Boolean satisfiability (SAT) solving is a fundamental problem in computer science. Finding efficient algorithms for SAT solving has broad implications in many areas of computer sci…
Geometric Theory for Program Testing
Bernhard Moller, Tony Hoare, Zhe Hou +1
Formal methods for verification of programs are extended to testing of programs. Their combination is intended to lead to benefits in reliable program development, testing, and evo…
An Executable Formal Model of the VHDL in Isabelle/HOL
Wilayat Khan, Zhe Hou, David Sanan +3
In the hardware design process, hardware components are usually described in a hardware description language. Most of the hardware description languages, such as Verilog and VHDL,…
Extracting Optimal Explanations for Ensemble Trees via Logical Reasoning
Gelin Zhang, Zhe Hou, Yanhong Huang +4
Ensemble trees are a popular machine learning model which often yields high prediction performance when analysing structured data. Although individual small decision trees are deem…
N-PAT: A Nested Model-Checker
Hadrien Bride, Cheng-Hao Cai, Jin Song Dong +4
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 desc…
Silas: High Performance, Explainable and Verifiable Machine Learning
Hadrien Bride, Zhe Hou, Jie Dong +2
This paper introduces a new classification tool named Silas, which is built to provide a more transparent and dependable data analytics service. A focus of Silas is on providing a…
GRAVITAS: A Model Checking Based Planning and Goal Reasoning Framework for Autonomous Systems
Hadrien Bride, Jin Song Dong, Ryan Green +3
While AI techniques have found many successful applications in autonomous systems, many of them permit behaviours that are difficult to interpret and may lead to uncertain results.…
A formalisation of the SPARC TSO memory model for multi-core machine code
Zhe Hou, David Sanan, Alwen Tiu +2
SPARC processors have many applications in mission-critical industries such as aviation and space engineering. Hence, it is important to provide formal frameworks that facilitate t…
Modular Labelled Sequent Calculi for Abstract Separation Logics
Zhé Hóu, Ranald Clouston, Rajeev Goré +1
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" be…
Completeness for a First-order Abstract Separation Logic
Zhe Hou, Alwen Tiu
Existing work on theorem proving for the assertion language of separation logic (SL) either focuses on abstract semantics which are not readily available in most applications of pr…
Proof search for propositional abstract separation logics via labelled sequents
Zhe Hou, Ranald Clouston, Rajeev Gore +1
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 particu…
A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
Zhe Hou, Alwen Tiu, Rajeev Gore
We present a labelled sequent calculus for Boolean BI, a classical variant of O'Hearn and Pym's logic of Bunched Implication. The calculus is simple, sound, complete, and enjoys cu…