Publication

This page lists the publications I have (co-)authored. I provide more details of these publications on the research pages.

Table of Contents

  1. Dependency Graph
  2. Main Publications
  3. Other Publications and Posters

Dependency Graph

This graph summarises the dependencies of my publications. You can view the details of each paper by clicking on its corresponding node.

flowchart LR VerifyC["VerifyC"] Refinement["Refinement"] VeriFile["VeriFile"] TowardsEvo["TowardsEvo"] GeneticSyn["GeneticSyn"] PSL["PSL"] GoalOriented["Goal-Oriented"] TemplateBased["Template-Based"] LiFtEr["LiFtEr"] SeLFiE["SeLFiE"] SmartInduct["SmartInduct"] SmarterInduct["SmarterInduct"] PaMpeR["PaMpeR"] SimpleDataset["Dataset"] Abduction["Abduction"] %% Style definitions classDef default fill:#f9f9f9,stroke:#333,stroke-width:2px; classDef futureWork fill:#fff,stroke:#333,stroke-width:2px,stroke-dasharray: 5 5; class Abduction futureWork; click Abduction "#proof-by-abduction-in-isabellehol" "Proof By Abduction in Isabelle/HOL" click TemplateBased "#template-based-conjecturing-for-automated-induction-in-isabellehol" "Template-Based Conjecturing for Automated Induction in Isabelle/HOL" click GeneticSyn "#genetic-algorithm-for-program-synthesis" "Genetic Algorithm for Program Synthesis" click SeLFiE "#definitional-quantifiers-realise-semantic-reasoning-for-proof-by-induction" "Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction" click SmarterInduct "#faster-smarter-induction-for-isabellehol" "Faster Smarter Induction for Isabelle/HOL" click SmartInduct "#smart-induction-for-isabellehol-tool-paper" "Smart Induction for Isabelle/HOL (Tool Paper)" click SimpleDataset "#simple-dataset-for-proof-method-recommendation-in-isabellehol-dataset-description" "Simple Dataset for Proof Method Recommendation in Isabelle/HOL" click LiFtEr "#lifter-language-to-encode-induction-heuristics-for-isabellehol" "LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL" click TowardsEvo "#towards-evolutionary-theorem-proving-for-isabellehol-poster-only-paper" "Towards Evolutionary Theorem Proving for Isabelle/HOL" click PaMpeR "#pamper-proof-method-recommendation-system-for-isabellehol" "PaMpeR: Proof Method Recommendation System for Isabelle/HOL" click GoalOriented "#goal-oriented-conjecturing-for-isabellehol" "Goal-Oriented Conjecturing for Isabelle/HOL" click PSL "#a-proof-strategy-language-and-proof-script-generation-for-isabellehol" "A Proof Strategy Language and Proof Script Generation for Isabelle/HOL" click VerifyC "#a-framework-for-the-automatic-formal-verification-of-refinement-from-cogent-to-c" "A framework for the automatic formal verification of refinement from Cogent to C" click Refinement "#refinement-through-restraint-bringing-down-the-cost-of-verification" "Refinement through Restraint: Bringing Down the Cost of Verification" click VeriFile "#cogent-verifying-high-assurance-file-system-implementations" "Cogent: Verifying High-Assurance File System Implementations" VerifyC -->|is part of| Refinement Refinement --> |is used in| VeriFile TowardsEvo -->|is realised in| GeneticSyn TowardsEvo -.-> |should be used in| Abduction PSL -->|is used in| Abduction PSL -->|is used in| GoalOriented PSL -->|is used in| TemplateBased TemplateBased -->|is used in| Abduction LiFtEr -->|is used in| SmartInduct LiFtEr -->|evolves to| SeLFiE SeLFiE -->|is used in| SmarterInduct SmartInduct -->|evolves to| SmarterInduct SmarterInduct -->|is used in| TemplateBased SimpleDataset -->|is used in| PaMpeR PaMpeR -.-> |should be used in| Abduction GoalOriented -->|is used in| Abduction SmarterInduct -->|is used in| Abduction SeLFiE -->|is used in| Abduction PSL -->|integrates| SmarterInduct

Main Publications

Template-Based Conjecturing for Automated Induction in Isabelle/HOL

Genetic Algorithm for Program Synthesis

Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction

Faster Smarter Induction for Isabelle/HOL

Smart Induction for Isabelle/HOL (Tool Paper)

Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)

LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL

Towards Evolutionary Theorem Proving for Isabelle/HOL (poster-only paper)

PaMpeR: Proof Method Recommendation System for Isabelle/HOL

Goal-Oriented Conjecturing for Isabelle/HOL

A Proof Strategy Language and Proof Script Generation for Isabelle/HOL

Refinement through Restraint: Bringing Down the Cost of Verification

A framework for the automatic formal verification of refinement from Cogent to C

Cogent: Verifying High-Assurance File System Implementations

Other Publications and Posters

Proof By Abduction in Isabelle/HOL

Evolutionary Computation for Program Synthesis in SuSLik

Faster Smarter Proof by Induction in Isabelle/HOL with Definitional Quantifiers

Towards United Reasoning for Automatic Induction in Isabelle/HOL

Smart Induction for Isabelle/HOL (Tool Paper)

LiFtEr: Language to Encode Induction Heuristics

Towards United Reasoning for Automatic Induction in Isabelle/HOL

Domain-Specific Language to Encode Induction Heuristics

Towards Machine Learning Induction

Towards Machine Learning Induction

Towards Machine Learning Induction

PaMpeR: A Proof Method Recommendation System for Isabelle/HOL

Designing Games of Theorem Proving

Towards Smart Proof Search for Isabelle

Proof Strategy Language

Close Encounters of the Higher Kind - Emulating Constructor Classes in Standard ML (extended abstract)

Keep Failed Proof Attempts in Memory