On the public citation graph
TacTok: semantics-aware proof synthesis
0 signed · 108 inferred · view as graph
Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.
Is this your work? Sign in with ORCID and put your name on the
claims that are yours.
Reference health. See whether every reference in this work resolves to a
known work and none has been retracted — and get a dated CiteStamped
badge you can embed.
What this work says
Outgoing claims: the papers this work cites, builds on, or argues with.
inferredcites →https://doi.org/10.1007/3-540-45949-9openalex-snapshot
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
inferredcites →https://doi.org/10.1007/3-540-69778-0_2openalex-snapshot
A Science of Reasoning (Extended Abstract)
inferredcites →https://doi.org/10.1007/978-1-4020-8157-6_30openalex-snapshot
AstrÉe: Verification of Absence of Runtime Error
inferredcites →https://doi.org/10.1007/978-3-540-78800-3_24openalex-snapshot
Z3: An Efficient SMT Solver
inferredcites →https://doi.org/10.1007/978-3-642-17511-4_20openalex-snapshot
Dafny: An Automatic Program Verifier for Functional Correctness
inferredcites →https://doi.org/10.1007/978-3-642-24364-6_2openalex-snapshot
Automatic Proof and Disproof in Isabelle/HOL
inferredcites →https://doi.org/10.1007/978-3-642-39799-8_1openalex-snapshot
First-Order Theorem Proving and Vampire
inferredcites →https://doi.org/10.1007/978-3-642-45221-5_49openalex-snapshot
System Description: E 1.8
inferredcites →https://doi.org/10.1007/bfb0031814openalex-snapshot
HOL Light: A tutorial introduction
inferredcites →https://doi.org/10.1007/s10817-013-9286-5openalex-snapshot
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
inferredcites →https://doi.org/10.1007/s10817-018-9458-4openalex-snapshot
Hammer for Coq: Automation for Dependent Type Theory
inferredcites →https://doi.org/10.1007/s11786-014-0173-1openalex-snapshot
Recycling Proof Patterns in Coq: Case Studies
inferredcites →https://doi.org/10.1016/j.cor.2007.01.010openalex-snapshot
Staffing a software project: A constraint satisfaction and optimization-based approach
inferredcites →https://doi.org/10.1016/j.jal.2005.10.002openalex-snapshot
TPS: A hybrid automatic-interactive system for developing proofs
inferredcites →https://doi.org/10.1038/323533a0openalex-snapshot
Learning representations by back-propagating errors
inferredcites →https://doi.org/10.1109/32.988709openalex-snapshot
Generating software test data by evolution
inferredcites →https://doi.org/10.1109/ase.2015.60openalex-snapshot
Repairing Programs with Semantic Code Search (T)
inferredcites →https://doi.org/10.1109/ase.2017.8115630openalex-snapshot
ICoq: Regression proof selection for large-scale verification projects
inferredcites →https://doi.org/10.1109/cmpsac.2004.1342667openalex-snapshot
N-gram-based detection of new malicious code
inferredcites →https://doi.org/10.1109/fose.2007.29openalex-snapshot
The Current State and Future of Search Based Software Engineering
inferredcites →https://doi.org/10.1109/icassp.1995.479394openalex-snapshot
Improved backing-off for M-gram language modeling
inferredcites →https://doi.org/10.1109/icse.2009.5070536openalex-snapshot
Automatically finding patches using genetic programming
inferredcites →https://doi.org/10.1109/icse.2012.6227135openalex-snapshot
On the naturalness of software
inferredcites →https://doi.org/10.1109/tassp.1987.1165125openalex-snapshot
Estimation of probabilities from sparse data for the language model component of a speech recognizer
inferredcites →https://doi.org/10.1109/tnnls.2016.2582924openalex-snapshot
LSTM: A Search Space Odyssey
inferredcites →https://doi.org/10.1109/tse.2019.2944914openalex-snapshot
SOSRepair: Expressive Semantic Search for Real-World Program Repair
inferredcites →https://doi.org/10.1109/tse.2020.2998785openalex-snapshot
Quality of Automated Program Repair on Real-World Defects
inferredcites →https://doi.org/10.1145/1143997.1144315openalex-snapshot
Search-based determination of refactorings for improving the class structure of object-oriented systems
inferredcites →https://doi.org/10.1145/1146238.1146240openalex-snapshot
TimeAware test suite prioritization
inferredcites →https://doi.org/10.1145/1276958.1277171openalex-snapshot
Finding safety errors with ACO
inferredcites →https://doi.org/10.1145/1538788.1538814openalex-snapshot
Formal verification of a realistic compiler
inferredcites →https://doi.org/10.1145/1646353.1646374openalex-snapshot
A few billion lines of code later
inferredcites →https://doi.org/10.1145/2491956.2462178openalex-snapshot
Machine-verified network controllers
inferredcites →https://doi.org/10.1145/2737924.2737958openalex-snapshot
Verdi: a framework for implementing and formally verifying distributed systems
inferredcites →https://doi.org/10.1145/2786805.2786825openalex-snapshot
Is the cure worse than the disease? overfitting in automated program repair
inferredcites →https://doi.org/10.1145/2884781.2884848openalex-snapshot
On the "naturalness" of buggy code
inferredcites →https://doi.org/10.1145/3158116openalex-snapshot
Programming and proving with distributed protocols
inferredcites →https://doi.org/10.1145/3158133openalex-snapshot
Generating good generators for inductive relations
inferredcites →https://doi.org/10.1145/3167094openalex-snapshot
Adapting proof automation to adapt proofs
inferredcites →https://doi.org/10.1162/089976600300015015openalex-snapshot
Learning to Forget: Continual Prediction with LSTM
inferredcites →https://doi.org/10.18429/jacow-icalepcs2017-tudpl02openalex-snapshot
Automatic Formal Verification for EPICS
inferredcites →https://doi.org/10.18653/v1/d13-1170openalex-snapshot
Recursive Deep Models for Semantic Compositionality Over a Sentiment Treebank
inferredcites →https://doi.org/10.18653/v1/n18-1202openalex-snapshot
Deep Contextualized Word Representations
inferredcites →https://doi.org/10.18653/v1/n19-1423openalex-snapshot
BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding
inferredcites →https://doi.org/10.18653/v1/p17-1041openalex-snapshot
A Syntactic Neural Model for General-Purpose Code Generation
inferredcites →https://doi.org/10.21437/interspeech.2012-65openalex-snapshot
LSTM neural networks for language modeling
inferredcites →https://doi.org/10.3115/1075218.1075255openalex-snapshot
An improved error model for noisy channel spelling correction
inferredcites →https://doi.org/10.3115/1610075openalex-snapshot
Proceedings of the 2006 Conference on Empirical Methods in Natural Language Processing - EMNLP '06
inferredcites →https://doi.org/10.3115/v1/d14-1179openalex-snapshot
Learning Phrase Representations using RNN Encoder–Decoder for Statistical Machine Translation
inferredcites →https://doi.org/10.3115/v1/p15-1150openalex-snapshot
Improved Semantic Representations From Tree-Structured Long Short-Term Memory Networks
inferredcites →https://doi.org/10.4204/eptcs.118.2openalex-snapshot
Machine Learning in Proof General: Interfacing Interfaces
inferredcites →https://doi.org/10.4230/lipics.snapl.2017.4openalex-snapshot
Natural Language is a Programming Language: Applying Natural Language Processing to Software Development
inferredcites →https://doi.org/10.5281/zenodo.4088896openalex-snapshot
Replication package for "TacTok: Semantics-aware proof synthesis"
inferredcites →https://doi.org/10.5555/2337223.2337322openalex-snapshot
On the naturalness of software
inferredcites →https://doi.org/10.5555/944919.944966openalex-snapshot
A neural probabilistic language model
inferredcites →https://doi.org/10.7551/mitpress/9153.001.0001openalex-snapshot
Certified Programming with Dependent Types
What points at this work
Incoming claims: where this work appears in other papers’ reference lists and arguments.
inferred← citeshttps://doi.org/10.1007/978-3-031-42753-4_16openalex-snapshot
CoProver: A Recommender System for Proof Construction
inferred← citeshttps://doi.org/10.1007/978-3-031-61716-4_4openalex-snapshot
Learning Guided Automated Reasoning: A Brief Survey
inferred← citeshttps://doi.org/10.1007/978-3-031-66997-2_21openalex-snapshot
HOL4PRS: Proof Recommendation System for the HOL4 Theorem Prover
inferred← citeshttps://doi.org/10.1007/978-981-95-4213-0_3openalex-snapshot
LLM-SYM: Integrating Symbolic Methods and Large Language Models for Automated Theorem Proving
inferred← citeshttps://doi.org/10.1007/s10664-025-10729-8openalex-snapshot
Application of AI to formal methods — an analysis of current trends
inferred← citeshttps://doi.org/10.1109/adacis65663.2025.11436933openalex-snapshot
HOL4PSG: AI-Driven Proof Sequence Generation for the HOL4 Theorem Prover
inferred← citeshttps://doi.org/10.1109/ase63991.2025.00255openalex-snapshot
LLM-Assisted Synthesis of High-Assurance C Programs
inferred← citeshttps://doi.org/10.1109/forge66646.2025.00035openalex-snapshot
Evaluating the Ability of GPT-4o to Generate Verifiable Specifications in VeriFast
inferred← citeshttps://doi.org/10.1109/icpads67057.2025.11323031openalex-snapshot
NL2CSP: Towards Automated CSP Code Generation with Large Language Models
inferred← citeshttps://doi.org/10.1109/icse-companion58688.2023.00018openalex-snapshot
PRoofster: Automated Formal Verification
inferred← citeshttps://doi.org/10.1109/icse-companion58688.2023.00035openalex-snapshot
Seldonian Toolkit: Building Software with Safe and Fair Machine Learning
inferred← citeshttps://doi.org/10.1109/icse48619.2023.00109openalex-snapshot
Better Automatic Program Repair by Using Bug Reports and Tests Together
inferred← citeshttps://doi.org/10.1109/icse55347.2025.00002openalex-snapshot
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
inferred← citeshttps://doi.org/10.1109/icse55347.2025.00033openalex-snapshot
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
inferred← citeshttps://doi.org/10.1109/icse55347.2025.00116openalex-snapshot
Gpass: A Goal-Adaptive Neural Theorem Prover Based on Coq for Automated Formal Verification
inferred← citeshttps://doi.org/10.1109/icse55347.2025.00161openalex-snapshot
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
inferred← citeshttps://doi.org/10.1109/tim.2025.3542861openalex-snapshot
Logic Synthesis Tools’ Testing via Configuration Diversification With Combinatorial Multiarmed Bandit
inferred← citeshttps://doi.org/10.1145/3453483.3454033openalex-snapshot
Proof repair across type equivalences
inferred← citeshttps://doi.org/10.1145/3510003.3510138openalex-snapshot
Diversity-driven automated formal verification
inferred← citeshttps://doi.org/10.1145/3549034.3570200openalex-snapshot
The promise and perils of using machine learning when engineering software (keynote paper)
inferred← citeshttps://doi.org/10.1145/3563306openalex-snapshot
Data-driven lemma synthesis for interactive proofs
inferred← citeshttps://doi.org/10.1145/3571850openalex-snapshot
Blindspots in Python and Java APIs Result in Vulnerable Code
inferred← citeshttps://doi.org/10.1145/3593374openalex-snapshot
Passport: Improving Automated Formal Verification Using Identifiers
inferred← citeshttps://doi.org/10.1145/3597503.3639095openalex-snapshot
Automated Program Repair, What Is It Good For? Not Absolutely Nothing!
inferred← citeshttps://doi.org/10.1145/3611643.3616243openalex-snapshot
Baldur: Whole-Proof Generation and Repair with Large Language Models
inferred← citeshttps://doi.org/10.1145/3626252.3630928openalex-snapshot
Solving Proof Block Problems Using Large Language Models
inferred← citeshttps://doi.org/10.1145/3643763openalex-snapshot
Towards AI-Assisted Synthesis of Verified Dafny Methods
inferred← citeshttps://doi.org/10.1145/3644033openalex-snapshot
Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)
inferred← citeshttps://doi.org/10.1145/3644033.3644374openalex-snapshot
Leveraging Large Language Models to Boost Dafny’s Developers Productivity
inferred← citeshttps://doi.org/10.1145/3663529.3663814openalex-snapshot
CoqPyt: Proof Navigation in Python in the Era of LLMs
inferred← citeshttps://doi.org/10.1145/3691620.3695357openalex-snapshot
CoqPilot, a plugin for LLM-based generation of proofs
inferred← citeshttps://doi.org/10.1145/3691620.3695521openalex-snapshot
Proof Automation with Large Language Models
inferred← citeshttps://doi.org/10.1145/3691621.3694932openalex-snapshot
Vision Paper: Proof-Carrying Code Completions
inferred← citeshttps://doi.org/10.1145/3744916.3787783openalex-snapshot
ProofCoop: Collaborative Automated Formal Verification
inferred← citeshttps://doi.org/10.1145/3759425.3763391openalex-snapshot
A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
inferred← citeshttps://doi.org/10.1145/3763131openalex-snapshot
Synthesizing Implication Lemmas for Interactive Theorem Proving
inferred← citeshttps://doi.org/10.1145/3763174openalex-snapshot
AutoVerus: Automated Proof Generation for Rust Code
inferred← citeshttps://doi.org/10.1145/3797139openalex-snapshot
ProofFusion: Improving Neural Theorem Proving via Adaptive Retrieval-Augmented Reasoning
inferred← citeshttps://doi.org/10.1145/3832783.3834382openalex-snapshot
Adaptive Proof Refinement with LLM-Guided Strategy Selection
inferred← citeshttps://doi.org/10.1145/3832783.3837528openalex-snapshot
Mining Tactics for Automated Theorem Proving
inferred← citeshttps://doi.org/10.48550/arxiv.2108.10821openalex-snapshot
Graph Contrastive Pre-training for Effective Theorem Reasoning
Editorial review for independent work. ICSAC — the Institute for Complexity
Science and Advanced Computing — runs a structured editorial panel for researchers
publishing outside journals, and publishes on CiteStamp rails. Submission is free
and goes through ORCID: icsacinstitute.org/submit.