On the public citation graph

Horn-ICE learning for synthesizing invariants and contracts

https://doi.org/10.1145/3276501
0 signed · 119 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.
Claim with ORCID
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.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/11691372_33openalex-snapshot
A Practical and Complete Approach to Predicate Refinement
inferredcites →https://doi.org/10.1007/11804192_17openalex-snapshot
Boogie: A Modular Reusable Verifier for Object-Oriented Programs
inferredcites →https://doi.org/10.1007/3-540-45251-6_29openalex-snapshot
Houdini, an Annotation Assistant for ESC/Java
inferredcites →https://doi.org/10.1007/978-3-319-08867-9_5openalex-snapshot
ICE: A Robust Framework for Learning Invariants
inferredcites →https://doi.org/10.1007/978-3-319-08867-9_6openalex-snapshot
From Invariant Checking to Invariant Inference Using Randomized Search
inferredcites →https://doi.org/10.1007/978-3-319-08867-9_7openalex-snapshot
SMACK: Decoupling Source Language Details from Verifier Implementations
inferredcites →https://doi.org/10.1007/978-3-319-21690-4_20openalex-snapshot
The SeaHorn Verification Framework
inferredcites →https://doi.org/10.1007/978-3-319-21690-4_40openalex-snapshot
Property-Directed Inference of Universal Invariants or Proving Their Absence
inferredcites →https://doi.org/10.1007/978-3-319-52234-0_28openalex-snapshot
IC3 - Flipping the E in ICE
inferredcites →https://doi.org/10.1007/978-3-319-66706-5_4openalex-snapshot
Learning Shape Analysis
inferredcites →https://doi.org/10.1007/978-3-319-89960-2_13openalex-snapshot
Invariant Synthesis for Incomplete Verification Engines
inferredcites →https://doi.org/10.1007/978-3-319-89960-2_20openalex-snapshot
ICE-Based Refinement Type Discovery for Higher-Order Functional Programs
inferredcites →https://doi.org/10.1007/978-3-540-45069-6_1openalex-snapshot
Interpolation and SAT-Based Model Checking
inferredcites →https://doi.org/10.1007/978-3-540-45069-6_39openalex-snapshot
Linear Invariant Generation Using Non-linear Constraint Solving
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-02658-4_48openalex-snapshot
InvGen: An Efficient Invariant Generator
inferredcites →https://doi.org/10.1007/978-3-642-18275-4_7openalex-snapshot
SAT-Based Model Checking without Unrolling
inferredcites →https://doi.org/10.1007/978-3-642-31424-7_11openalex-snapshot
Interpolants as Classifiers
inferredcites →https://doi.org/10.1007/978-3-642-31612-8_13openalex-snapshot
Generalized Property Directed Reachability
inferredcites →https://doi.org/10.1007/978-3-642-36742-7_53openalex-snapshot
Ultimate Automizer with SMTInterpol
inferredcites →https://doi.org/10.1007/978-3-642-37036-6_31openalex-snapshot
A Data Driven Approach for Algebraic Loop Invariants
inferredcites →https://doi.org/10.1007/978-3-642-38856-9_21openalex-snapshot
Verification as Learning Geometric Concepts
inferredcites →https://doi.org/10.1007/978-3-642-38856-9_8openalex-snapshot
On Solving Universally Quantified Horn Clauses
inferredcites →https://doi.org/10.1007/978-3-642-39799-8_57openalex-snapshot
Learning Universally Quantified Invariants of Linear Data Structures
inferredcites →https://doi.org/10.1007/978-3-642-39799-8_61openalex-snapshot
Solving Existentially Quantified Horn Clauses
inferredcites →https://doi.org/10.1007/978-3-642-54013-4_3openalex-snapshot
Relational Thread-Modular Static Value Analysis by Abstract Interpretation
inferredcites →https://doi.org/10.1007/978-3-662-54580-5_20openalex-snapshot
Software Verification with Validation of Results
inferredcites →https://doi.org/10.1007/bf00116251openalex-snapshot
Induction of Decision Trees
inferredcites →https://doi.org/10.1007/bf01211617openalex-snapshot
The rely-guarantee method for verifying shared variable concurrent programs
inferredcites →https://doi.org/10.1016/0743-1066(84)90014-1openalex-snapshot
Linear-time algorithms for testing the satisfiability of propositional horn formulae
inferredcites →https://doi.org/10.1145/1375581.1375616openalex-snapshot
Program analysis as constraint solving
inferredcites →https://doi.org/10.1145/1379022.1375616openalex-snapshot
Program analysis as constraint solving
inferredcites →https://doi.org/10.1145/2254064.2254112openalex-snapshot
Synthesizing software verifiers from proof rules
inferredcites →https://doi.org/10.1145/2345156.2254112openalex-snapshot
Synthesizing software verifiers from proof rules
inferredcites →https://doi.org/10.1145/2384616.2384625openalex-snapshot
GPUVerify
inferredcites →https://doi.org/10.1145/2442776.2442783openalex-snapshot
Automatic predicate abstraction of C programs
inferredcites →https://doi.org/10.1145/2509136.2509511openalex-snapshot
Inductive invariant generation via abductive inference
inferredcites →https://doi.org/10.1145/2509136.2509517openalex-snapshot
Barrier invariants
inferredcites →https://doi.org/10.1145/2784731.2784766openalex-snapshot
Learning refinement types
inferredcites →https://doi.org/10.1145/2837614.2837664openalex-snapshot
Learning invariants using decision trees and implication counterexamples
inferredcites →https://doi.org/10.1145/2858949.2784766openalex-snapshot
Learning refinement types
inferredcites →https://doi.org/10.1145/2908080.2908099openalex-snapshot
Data-driven precondition inference with learned features
inferredcites →https://doi.org/10.1145/2908080.2908125openalex-snapshot
Automatically learning shape specifications
inferredcites →https://doi.org/10.1145/2914770.2837664openalex-snapshot
Learning invariants using decision trees and implication counterexamples
inferredcites →https://doi.org/10.1145/2970276.2970305openalex-snapshot
Inferring annotations for device drivers from verification histories
inferredcites →https://doi.org/10.1145/2980983.2908125openalex-snapshot
Automatically learning shape specifications
inferredcites →https://doi.org/10.1145/3192366.3192416openalex-snapshot
A data-driven CHC solver
inferredcites →https://doi.org/10.1145/337180.337240openalex-snapshot
Quickly detecting relevant program invariants
inferredcites →https://doi.org/10.1145/360051.360224openalex-snapshot
Verifying properties of parallel programs
inferredcites →https://doi.org/10.1145/378795.378846openalex-snapshot
Automatic predicate abstraction of C programs
inferredcites →https://doi.org/10.1145/381694.378846openalex-snapshot
Automatic predicate abstraction of C programs
inferredcites →https://doi.org/10.1145/512950.512973openalex-snapshot
Abstract interpretation
inferredcites →https://doi.org/10.1145/69575.69577openalex-snapshot
Tentative steps toward a development method for interfering programs
inferredcites →https://doi.org/10.23919/fmcad.2017.8102247openalex-snapshot
Sampling invariants from frequency distributions
inferredcites →https://doi.org/10.48550/arxiv.1302.2273openalex-snapshot
Learning Universally Quantified Invariants of Linear Data Structures
inferredcites →https://doi.org/10.5555/2337223.2337304openalex-snapshot
Using dynamic analysis to discover polynomial and array invariants

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-030-25540-4_17openalex-snapshot
Overfitting in Synthesis: Theory and Practice
inferred← citeshttps://doi.org/10.1007/978-3-030-32304-2_16openalex-snapshot
Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants
inferred← citeshttps://doi.org/10.1007/978-3-030-53291-8_31openalex-snapshot
Manthan: A Data-Driven Approach for Boolean Function Synthesis
inferred← citeshttps://doi.org/10.1007/978-3-030-81685-8_35openalex-snapshot
Constraint-Based Relational Verification
inferred← citeshttps://doi.org/10.1007/978-3-030-81688-9_4openalex-snapshot
Decision Tree Learning in CEGIS-Based Termination Analysis
inferred← citeshttps://doi.org/10.1007/978-3-030-88806-0_12openalex-snapshot
Toward Neural-Network-Guided Program Synthesis and Verification
inferred← citeshttps://doi.org/10.1007/978-3-030-88806-0_20openalex-snapshot
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
inferred← citeshttps://doi.org/10.1007/978-3-031-13185-1_14openalex-snapshot
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
inferred← citeshttps://doi.org/10.1007/978-3-031-17143-7_23openalex-snapshot
MLFM: Machine Learning Meets Formal Method for Faster Identification of Security Breaches in Network Functions Virtualization (NFV)
inferred← citeshttps://doi.org/10.1007/978-3-031-19135-0_1openalex-snapshot
SAT-Based Invariant Inference and Its Relation to Concept Learning
inferred← citeshttps://doi.org/10.1007/978-3-031-22308-2_10openalex-snapshot
Invariant Inference with Provable Complexity from the Monotone Theory
inferred← citeshttps://doi.org/10.1007/978-3-031-30823-9_12openalex-snapshot
Neural Network-Guided Synthesis of Recursive List Functions
inferred← citeshttps://doi.org/10.1007/978-3-031-38828-6_6openalex-snapshot
Proving Properties of Operation Contracts with Test Scenarios
inferred← citeshttps://doi.org/10.1007/978-3-031-57249-4_9openalex-snapshot
Weakest Precondition Inference for Non-Deterministic Linear Array Programs
inferred← citeshttps://doi.org/10.1007/978-3-031-57267-8openalex-snapshot
Programming Languages and Systems
inferred← citeshttps://doi.org/10.1007/978-3-031-57267-8_10openalex-snapshot
Maximal Quantified Precondition Synthesis for Linear Array Loops
inferred← citeshttps://doi.org/10.1007/978-3-031-74776-2_16openalex-snapshot
ConstraintFlow: A Declarative DSL for Easy Development of DNN Certifiers
inferred← citeshttps://doi.org/10.1007/978-3-031-82700-6_1openalex-snapshot
Discovering Likely Invariants for Distributed Systems Through Runtime Monitoring and Learning
inferred← citeshttps://doi.org/10.1007/978-3-031-98685-7_16openalex-snapshot
Data-Driven Verification of Procedural Programs with Integer Arrays
inferred← citeshttps://doi.org/10.1007/978-3-032-00347-8_2openalex-snapshot
Enhancing Numerical Invariants Learning with Bounded Reachability Analysis
inferred← citeshttps://doi.org/10.1007/978-3-032-00942-5_4openalex-snapshot
AutoSV-Annotator: Integrating Deductive and Automatic Software Verification
inferred← citeshttps://doi.org/10.1007/978-3-032-26204-2_20openalex-snapshot
Generating Rely-Guarantee Conditions with the Conditional-Writes Domain
inferred← citeshttps://doi.org/10.1007/978-3-032-28079-4_10openalex-snapshot
Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving
inferred← citeshttps://doi.org/10.1007/s10009-020-00564-1openalex-snapshot
Verification and refutation of C programs based on k-induction and invariant inference
inferred← citeshttps://doi.org/10.1007/s10703-024-00468-9openalex-snapshot
Towards neural-network-guided program synthesis and verification
inferred← citeshttps://doi.org/10.1007/s10703-025-00484-3openalex-snapshot
Automatic assume-guarantee reasoning for safety and liveness using passive learning
inferred← citeshttps://doi.org/10.1007/s10817-020-09570-zopenalex-snapshot
A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines
inferred← citeshttps://doi.org/10.1109/iccad51958.2021.9643583openalex-snapshot
Engineering an Efficient Boolean Functional Synthesis Engine
inferred← citeshttps://doi.org/10.1109/icse48619.2023.00115openalex-snapshot
Data-driven Recurrent Set Learning For Non-termination Analysis
inferred← citeshttps://doi.org/10.1109/icst53961.2022.00012openalex-snapshot
Machine Learning Based Invariant Generation: A Framework and Reproducibility Study
inferred← citeshttps://doi.org/10.1109/infocom52122.2024.10621366openalex-snapshot
P4Inv: Inferring Packet Invariants for Verification of Stateful P4 Programs
inferred← citeshttps://doi.org/10.1109/qrs51102.2020.00013openalex-snapshot
PBLInv: Postcondition-based Loop Invariant Learning for C Programs
inferred← citeshttps://doi.org/10.1145/3314221.3314641openalex-snapshot
Learning stateful preconditions modulo a test generator
inferred← citeshttps://doi.org/10.1145/3317550.3321451openalex-snapshot
Towards Automatic Inference of Inductive Invariants
inferred← citeshttps://doi.org/10.1145/3365365.3382222openalex-snapshot
Synthesizing barrier certificates using neural networks
inferred← citeshttps://doi.org/10.1145/3368089.3409752openalex-snapshot
Interval counterexamples for loop invariant learning
inferred← citeshttps://doi.org/10.1145/3371073openalex-snapshot
Complexity and information in invariant inference
inferred← citeshttps://doi.org/10.1145/3385412.3385967openalex-snapshot
Data-driven inference of representation invariants
inferred← citeshttps://doi.org/10.1145/3453483.3454104openalex-snapshot
Specification synthesis with constrained Horn clauses
inferred← citeshttps://doi.org/10.1145/3468264.3468621openalex-snapshot
SynGuar: guaranteeing generalization in programming by example
inferred← citeshttps://doi.org/10.1145/3498676openalex-snapshot
Property-directed reachability as abstract interpretation in the monotone theory
inferred← citeshttps://doi.org/10.1145/3517804.3524151openalex-snapshot
On the Parameterized Complexity of Learning First-Order Logic
inferred← citeshttps://doi.org/10.1145/3533767.3534381openalex-snapshot
Almost correct invariants: synthesizing inductive invariants by fuzzing proofs
inferred← citeshttps://doi.org/10.1145/3563306openalex-snapshot
Data-driven lemma synthesis for interactive proofs
inferred← citeshttps://doi.org/10.1145/3597926.3598047openalex-snapshot
Loop Invariant Inference through SMT Solving Enhanced Reinforcement Learning
inferred← citeshttps://doi.org/10.1145/3656433openalex-snapshot
A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata
inferred← citeshttps://doi.org/10.1145/3672608.3707984openalex-snapshot
LLM-guided Predicate Discovery and Data Augmentation for Learning Likely Program Invariants
inferred← citeshttps://doi.org/10.1145/3691620.3695014openalex-snapshot
LLM Meets Bounded Model Checking: Neuro-symbolic Loop Invariant Inference
inferred← citeshttps://doi.org/10.1145/3720505openalex-snapshot
Counterexample-Guided Inference of Modular Specifications
inferred← citeshttps://doi.org/10.1145/3728920openalex-snapshot
Clause2Inv: A Generate-Combine-Check Framework for Loop Invariant Inference
inferred← citeshttps://doi.org/10.1145/3763131openalex-snapshot
Synthesizing Implication Lemmas for Interactive Theorem Proving
inferred← citeshttps://doi.org/10.1145/3798200openalex-snapshot
Learning Symmetric Invariants from Symmetric Samples
inferred← citeshttps://doi.org/10.23919/fmcad.2019.8894254openalex-snapshot
Learning-Based Synthesis of Safety Controllers
inferred← citeshttps://doi.org/10.23919/fmcad.2019.8894267openalex-snapshot
Extending enumerative function synthesis via SMT-driven classification
inferred← citeshttps://doi.org/10.4204/eptcs.344.1openalex-snapshot
An Overview of the HFL Model Checking Project
inferred← citeshttps://doi.org/10.46298/lmcs-21(3:9)2025openalex-snapshot
Learning Concepts Definable in First-Order Logic with Counting
inferred← citeshttps://doi.org/10.48550/arxiv.1904.07146openalex-snapshot
SyGuS-Comp 2018: Results and Analysis
inferred← citeshttps://doi.org/10.48550/arxiv.1905.07457openalex-snapshot
Overfitting in Synthesis: Theory and Practice (Extended Version)
inferred← citeshttps://doi.org/10.48550/arxiv.2006.12638openalex-snapshot
Information-theoretic User Interaction: Significant Inputs for Program Synthesis
inferred← citeshttps://doi.org/10.48550/arxiv.2007.03656openalex-snapshot
Program Verification via Predicate Constraint Satisfiability Modulo Theories
inferred← citeshttps://doi.org/10.48550/arxiv.2108.07642openalex-snapshot
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
inferred← citeshttps://doi.org/10.54337/aau429765826openalex-snapshot
Time For Stubborn Game Reductions
inferred← citeshttps://doi.org/10.70675/529006e9z5197z44eezaa10zb9838ec76479openalex-snapshot
Black-box code analysis for reverse engineering through constraint acquisition and program synthesis
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.