Search

Under construction. 👷⚒️🚧

Project List

Here is a list of my current and former projects with a focus on Search. The acronyms correspond to the names used in the project dependency graph.

Project Dependency Graph

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