Hyper Separation Logic extends separation logic and Hyper Hoare Logic with a hyper separating conjunction to support arbitrary quantifier alternation for hyperproperties over heap programs, with a soundness proof in Isabelle/HOL.
super hub Canonical reference
2023.Parallel Programming for Multicore and Cluster Systems(3 ed.)
Canonical reference. 83% of citing Pith papers cite this work as background.
125
Pith papers citing it
Background
83% of classified citations
hub tools
citation-role summary
background 35
method 3
other 2
baseline 1
dataset 1
citation-polarity summary
authors
co-cited works
representative citing papers
2G2T enables constant-size, statistically sound outsourcing of MSM with verification up to 300x faster than local computation and error probability at most 1/q.
A survey of 172 open educational datasets from 204 papers across LAK, EDM, and AIED conferences reveals trends, 143 previously uncatalogued datasets, field gaps, and an 8-item PRACTICE checklist for better data publication.
A dependent linear type theory is constructed by embedding linear logic into dependent type theory, yielding multiplicities that depend on variables, supporting W-types, with semantics in indexed Categories with Families and an Agda implementation.
HDL defines dynamic theories with lifting and combination operations, proves soundness and relative completeness in Isabelle, and demonstrates the approach on a Java controller steering a differential dynamic logic plant model.
The ontological continuum is a new vocabulary based on semantics-pragmatics and properties-affordances distinctions that enables re-engineering of knowledge graphs across the full spectrum of modeling practices.
An O(n^5) exact algorithm for broadcast domination obtained by reducing the path-case to O(n^3) via a single DAG on oriented broadcast balls.
Polyconvexity implies true-stress-true-strain monotonicity in incompressible isotropic hyperelasticity, which is enforced in four PANN architectures that show varying extrapolation behavior on experimental data.
Event-B Agent is an LLM agent that synthesizes, refines, and repairs Event-B formal models from natural language requirements via iterative verification feedback loops.
CDCL SAT solvers compute small proofdoors on linearly scaling BMC families but large non-absorbed ones on exponential families, as shown by empirical measurements on a 76k+ instance benchmark where prior parameters fail to discriminate regimes.
Proves that ℓ_p norm minimization yields p-independent Hausdorff convergence rate O(k^{2/(1-q)}) in convex vector optimization via Euclidean intermediary and norm equivalence.
A compositional algebraic decision diagram algorithm quantifies sensitivity in decision tree ensembles with certified error and confidence bounds, outperforming model counters on benchmarks.
PAFP is FPT by BFS-width plus backward arcs in the union digraph and polynomial-time solvable via 2-SAT for DAGs of exact-length width 2, with matching NP-hardness for width 3.
FLiD is a field-localized forgery detection method for identity documents that outperforms full-document baselines and general detectors with significantly fewer parameters.
LLM2Ltac mines symbolic tactics from 11,725 Coq theorems using LLMs and integrates them into CoqHammer, improving proof rates by 23.87% on 6,199 theorems from four large verification projects.
A source-level interaction concept for interactive program verification, prototyped in KeY, improves user understanding of proof states and defect detection according to a user study.
SCHORTY uses a tilted sensor in a single camera to map pixel position to range via the Scheimpflug principle, demonstrated experimentally with event cameras for passive UAV ranging up to 1.1 km.
Text-guided class-agnostic counting models exhibit significant weaknesses in grounding textual prompts to visual objects, as demonstrated by new negative-label and distractor tests on a multi-category dataset.
BadmintonGRF is a new public multimodal dataset and benchmark that pairs multi-view video with instrumented GRF for markerless load estimation in badminton.
RESTestBench shows that LLM-generated REST API test effectiveness drops when interacting with faulty or mutated code, especially for vague requirements, indicating that high-detail requirements make direct SUT interaction unnecessary.
Hybrid Path-Sums offer a new symbolic framework with rewriting rules and assertions to represent, simplify, and verify properties of hybrid quantum-classical programs.
Agentic Witnessing enables privacy-preserving auditing of semantic properties in private data by running an LLM auditor in a TEE that answers binary queries and produces cryptographic transcripts of its reasoning.
Point&Grasp probabilistically integrates pointing and grasp gestures for out-of-reach object selection in MR, trained on a new ORG dataset, and outperforms single-cue baselines in user studies.
The exact inner vertex-isoperimetric profile I_d(k) on the d-regular tree is determined, with sets optimal precisely when their boundary branching excess satisfies τ(D) ≤ d-2, and all minimizers admit a canonical decomposition into iterated gluings of full domains.
citing papers explorer
-
Hyper Separation Logic (extended version)
Hyper Separation Logic extends separation logic and Hyper Hoare Logic with a hyper separating conjunction to support arbitrary quantifier alternation for hyperproperties over heap programs, with a soundness proof in Isabelle/HOL.
-
2G2T: Constant-Size, Statistically Sound MSM Outsourcing
2G2T enables constant-size, statistically sound outsourcing of MSM with verification up to 300x faster than local computation and error probability at most 1/q.
-
Open Datasets in Learning Analytics: Trends, Challenges, and Best PRACTICE
A survey of 172 open educational datasets from 204 papers across LAK, EDM, and AIED conferences reveals trends, 143 previously uncatalogued datasets, field gaps, and an 8-item PRACTICE checklist for better data publication.
-
Dependent Multiplicities in Dependent Linear Type Theory
A dependent linear type theory is constructed by embedding linear logic into dependent type theory, yielding multiplicities that depend on variables, supporting W-types, with semantics in indexed Categories with Families and an Agda implementation.
-
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
HDL defines dynamic theories with lifting and combination operations, proves soundness and relative completeness in Isabelle, and demonstrates the approach on a Java controller steering a differential dynamic logic plant model.
-
Knowledge Graph Re-engineering Along the Ontological Continuum (extended version)
The ontological continuum is a new vocabulary based on semantics-pragmatics and properties-affordances distinctions that enables re-engineering of knowledge graphs across the full spectrum of modeling practices.
-
An $O(n^5)$-Time Algorithm for Optimal Broadcast Domination
An O(n^5) exact algorithm for broadcast domination obtained by reducing the path-case to O(n^3) via a single DAG on oriented broadcast balls.
-
Concurrent enforcement of polyconvexity and true-stress-true-strain monotonicity in incompressible isotropic hyperelasticity: application to neural network constitutive models
Polyconvexity implies true-stress-true-strain monotonicity in incompressible isotropic hyperelasticity, which is enforced in four PANN architectures that show varying extrapolation behavior on experimental data.
-
Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair
Event-B Agent is an LLM agent that synthesizes, refines, and repairs Event-B formal models from natural language requirements via iterative verification feedback loops.
-
Understanding CDCL Solvers via Scalability Studies and Proofdoors
CDCL SAT solvers compute small proofdoors on linearly scaling BMC families but large non-absorbed ones on exponential families, as shown by empirical measurements on a 76k+ instance benchmark where prior parameters fail to discriminate regimes.
-
Convergence Rates for $\ell_p$ Norm Minimization in Convex Vector Optimization
Proves that ℓ_p norm minimization yields p-independent Hausdorff convergence rate O(k^{2/(1-q)}) in convex vector optimization via Euclidean intermediary and norm equivalence.
-
Quantifying Sensitivity for Tree Ensembles: A symbolic and compositional approach
A compositional algebraic decision diagram algorithm quantifies sensitivity in decision tree ensembles with certified error and confidence bounds, outperforming model counters on benchmarks.
-
Layer-Based Width for PAFP
PAFP is FPT by BFS-width plus backward arcs in the union digraph and polynomial-time solvable via 2-SAT for DAGs of exact-length width 2, with matching NP-hardness for width 3.
-
Field-Localized Forgery Detection for Digital Identity Documents
FLiD is a field-localized forgery detection method for identity documents that outperforms full-document baselines and general detectors with significantly fewer parameters.
-
A Learning Method for Symbolic Systems Using Large Language Models
LLM2Ltac mines symbolic tactics from 11,725 Coq theorems using LLMs and integrates them into CoqHammer, improving proof rates by 23.87% on 6,199 theorems from four large verification projects.
-
A New Interaction Concept for Interactive and Autoactive Program Verification
A source-level interaction concept for interactive program verification, prototyped in KeY, improves user understanding of proof states and defect detection according to a user study.
-
Monocular passive event-based range-finding of airborne objects using the Scheimpflug principle
SCHORTY uses a tilted sensor in a single camera to map pixel position to range via the Scheimpflug principle, demonstrated experimentally with event cameras for passive UAV ranging up to 1.1 km.
-
Does it Really Count? Assessing Semantic Grounding in Text-Guided Class-Agnostic Counting
Text-guided class-agnostic counting models exhibit significant weaknesses in grounding textual prompts to visual objects, as demonstrated by new negative-label and distractor tests on a multi-category dataset.
-
BadmintonGRF: A Multimodal Dataset and Benchmark for Markerless Ground Reaction Force Estimation in Badminton
BadmintonGRF is a new public multimodal dataset and benchmark that pairs multi-view video with instrumented GRF for markerless load estimation in badminton.
-
RESTestBench: A Benchmark for Evaluating the Effectiveness of LLM-Generated REST API Test Cases from NL Requirements
RESTestBench shows that LLM-generated REST API test effectiveness drops when interacting with faulty or mutated code, especially for vague requirements, indicating that high-detail requirements make direct SUT interaction unnecessary.
-
Hybrid Path-Sums for Hybrid Quantum Programs
Hybrid Path-Sums offer a new symbolic framework with rewriting rules and assertions to represent, simplify, and verify properties of hybrid quantum-classical programs.
-
Agentic Witnessing: Pragmatic and Scalable TEE-Enabled Privacy-Preserving Auditing
Agentic Witnessing enables privacy-preserving auditing of semantic properties in private data by running an LLM auditor in a TEE that answers binary queries and produces cryptographic transcripts of its reasoning.
-
Point & Grasp: Flexible Selection of Out-of-Reach Objects Through Probabilistic Cue Integration
Point&Grasp probabilistically integrates pointing and grasp gestures for out-of-reach object selection in MR, trained on a new ORG dataset, and outperforms single-cue baselines in user studies.
-
The Isoperimetric Problem in Regular Trees
The exact inner vertex-isoperimetric profile I_d(k) on the d-regular tree is determined, with sets optimal precisely when their boundary branching excess satisfies τ(D) ≤ d-2, and all minimizers admit a canonical decomposition into iterated gluings of full domains.
-
Network Meta-analysis and Diffusion
Covariance matrix of network meta-analysis treatment effects is the sum of a geometric series of diffusion matrices without inversion.
-
Some results on small ordered and cyclic Ramsey numbers
Authors compute new small two-color ordered and cyclic Ramsey numbers for monotone paths, cycles, stars, complete graphs and nested matchings via SAT solving, determine closed forms for several pairs of graph classes, obtain bounds, apply reinforcement learning for lower bounds, and introduce permut
-
Certified Program Synthesis with a Multi-Modal Verifier
LeetProof achieves higher rates of fully certified program synthesis from natural language by using a multi-modal verifier in Lean to validate specifications via randomized testing and delegate proofs to AI tools, outperforming single-mode baselines on benchmarks while uncovering defects in prior参考.
-
Hardness, Tractability and Density Thresholds of finite Pinwheel Scheduling Variants
2-Visits is strongly NP-complete for multiplicity 2 but in RP for constant distinct deadlines, with a 0.9142 density lower bound for 2-Visits and thresholds approaching 5/6 for large k.
-
GeoAgentBench: A Dynamic Execution Benchmark for Tool-Augmented Agents in Spatial Analysis
GeoAgentBench supplies a live execution environment and Plan-and-React architecture that lets tool-using AI agents handle multi-step GIS tasks more robustly than prior static evaluation methods.
-
A Categorical Basis for Robust Program Analysis
A categorical framework characterizes robustness in program analysis as functors and gives recipes for lifting sound robust analyses from restricted models to general programs.
-
DiV-INR: Extreme Low-Bitrate Diffusion Video Compression with INR Conditioning
DiV-INR integrates implicit neural representations as conditioning signals for diffusion models to achieve better perceptual quality than HEVC, VVC, and prior neural codecs at extremely low bitrates under 0.05 bpp.
-
Appear2Meaning: A Cross-Cultural Benchmark for Structured Cultural Metadata Inference from Images
A new cross-cultural benchmark shows vision-language models infer structured cultural metadata from images inconsistently, with fragmented signals and large performance gaps across regions and metadata types.
-
Entanglement in the open XX chain: R\'enyi oscillations, hard-edge crossover, and symmetry resolution
Closed-form asymptotics for Rényi entropies in the open XX chain give 2k_F oscillations, s^{±1/α} envelopes, and -½ log log ℓ equipartition offset.
-
Dominating Set with Quotas: Balancing Coverage and Constraints
DSQ is W[1]-hard on degeneracy-2 and K_{3,3}-free graphs but FPT parameterized by solution size plus treewidth, FPT on nowhere dense classes, and admits subexponential algorithms on apex-minor-free graphs via bidimensionality.
-
JSON Schema Inclusion through Refutational Normalization: Reconciling Efficiency and Completeness
Refutational normalization reconciles efficiency and completeness for JSON Schema inclusion checking.
-
Grassroots Bonds as a Foundation for Market Liquidity
Grassroots bonds add maturity dates to local cryptocurrencies to enable lending and other instruments via enforceable digital social contracts.
-
The Dual Majorizing Measure Theorem for Canonical Processes
Expected supremum of canonical processes with log-concave tails is equivalent up to universal constants to a functional on parameterized separation trees, with a polynomial-time approximation algorithm for finite cases.
-
State Space Estimation for DPOR-based Model Checkers(Extended Version)
A Monte Carlo estimator converts stateless optimal DPOR into an unbiased poly-time estimator for the number of Mazurkiewicz traces by sampling paths in the exploration tree and using stochastic enumeration to control variance.
-
Backdoor Attacks on Prompt-Driven Video Segmentation Foundation Models
BadVSFM is the first effective backdoor attack on prompt-driven video segmentation foundation models, using a two-stage encoder-decoder strategy to achieve high attack success rates with limited clean performance loss.
-
Fermion Thermal Field Theory for a Rotating Plasma (with Applications to Neutron Stars)
Extends thermal field theory to fermions with angular momentum and shows neutrino production in rotating neutron stars grows indefinitely with angular velocity near the inverse system size.
-
Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts
Semantic typing via coinductively defined interpretations on a typed operational semantics ensures information flow control and non-interference for TinySol contracts that use fallback functions.
-
Omnidirectional type inference for ML: principality any way
Omnidirectional type inference restores principality for ML extensions with fragile constructs via dynamic constraint solving with suspended matches and incremental instantiation of generalized types.
-
Intertwined polar, chiral, and ferro-rotational orders in a rotation-only insulator
Experimental multimodal optical study of Ni3TeO6 demonstrates intertwining of polar, chiral, and ferro-rotational orders that dictates domain states connected by inversion symmetry and produces mixed Néel-Bloch domain walls.
-
Trace Repair for Temporal Behavior Trees
Incremental segmentation and landmark-based heuristic repair enable efficient correction of traces exceeding 25,000 entries against temporal behavior tree specifications.
-
Colorful Minors
Defines colorful minors on q-colored graphs and proves three structural theorems for H-colorful-minor-free graphs, a q-parameterized Erdős-Pósa classification, and FPT results for testing and colorful-minor-monotone parameters.
-
$c$-Birkhoff polytopes
c-Birkhoff polytopes are unimodularly equivalent to the order polytopes of the heap posets of the c-sorting words of the longest permutation.
-
On the structure of higher order quantum maps
Higher order quantum map types are identified with Boolean type functions, with comb types corresponding to chain posets, and type functions decomposed via max/min of basic chains corresponding to affine mixtures and intersections.
-
A $\operatorname{prox}$-Based Semi-Smooth Newton Method for TV-Minimization
A prox-based semi-smooth Newton method for TV-minimization that is globally well-posed and locally superlinearly convergent under finite element discretization, extending to broader convex problems.
-
Evaluation of Pipelines for Data Integration into Knowledge Graphs
KGI-Bench evaluates data integration pipelines into knowledge graphs using coverage, correctness, and consistency metrics on movie domain datasets with 12 pipelines tested.
-
Verification of Configurable SRA Systems
A contract-based deductive verification framework using Dafny to prove correctness of all instantiations of configurable scheduler-restricted asynchronous systems at once.