An Efficient VCGen-based Modular Verification of Relational Properties

• URL: http://arxiv.org/abs/2401.08385v1
• Date: Tue, 16 Jan 2024 14:19:04 GMT
• Title: An Efficient VCGen-based Modular Verification of Relational Properties
• Abstract summary: Deductive verification typically relies on function contracts that specify the behavior of each function for a single function call. Recent work proposed a new technique for relational property verification that relies on a verification condition generator.
• Score: 1.567576360103422
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Deductive verification typically relies on function contracts that specify the behavior of each function for a single function call. Relational properties link several function calls together within a single specification. They can express more advanced properties of a given function, such as non-interference, continuity, or monotonicity, or relate calls to different functions, possibly run in parallel, for instance, to show the equivalence of two implementations. However, relational properties cannot be expressed and verified directly in the traditional setting of modular deductive verification. Recent work proposed a new technique for relational property verification that relies on a verification condition generator to produce logical formulas that must be verified to ensure a given relational property. This paper presents an overview of this approach and proposes important enhancements. We integrate an optimized verification condition generator and extend the underlying theory to show how relational properties can be proved in a modular way, where one relational property can be used to prove another one, like in modular verification of function contracts. Our results have been fully formalized and proved sound in the Coq proof assistant.

Related papers

• Lifted Model Construction under Approximate Commutativity [5.629677133940586]
  We show how -commutativity can be exploited for lifted model construction, downstream probabilistic inference, and prove strict bounds on the induced approximation error.<n>These theoretical guarantees are confirmed empirically, demonstrating comparable query accuracy at lower runtime.
  arXiv  Detail & Related papers  (2026-08-25T15:32:47Z)
• Concept Modulation Models: A Unified Framework for Identifiability and Extrapolation [19.425749551382093]
  We introduce concept modulation models (CMMs), an attribute-indexed class of conditional generative models with structure $Ato to Cto X$.<n>We show that CMMs lift identifiability to conditional settings by showing that feature agreement on observed attributes induces a latent concept transition constrained by the CMM class.
  arXiv  Detail & Related papers  (2026-06-16T21:53:01Z)
• COMBINER: Composed Image Retrieval Guided by Attribute-based Neighbor Relations [73.40758654107724]
  We introduce a COMposed image retrieval network guided by By attrIbute-based NEighbor Relations (COMBINER)<n>Specifically, we first design an Adaptive Semantic Disentanglement module, which is capable of disentangling attribute features.<n> Secondly, we propose a Unified Prototype-based Composition module, which can construct cross-modal unified prototypes.<n>Finally, we introduce a Dual Relations Modeling module, which can mine pairwise and neighbor relations based on attribute similarity.
  arXiv  Detail & Related papers  (2026-06-03T08:43:51Z)
• Geometric Factual Recall in Transformers [57.48371649045765]
  A common view casts internal weight matrices as associative memories over pairs of embeddings, requiring memorization counts that scale linearly with the number of facts.<n>We develop a theoretical and empirical account of an alternative, emphgeometric form of memorization in which learned embeddings encode structure directly.<n>In a controlled setting where a single-layer transformer must memorize random vectors from subjects to a shared attribute set, we prove that a logarithmic embedding dimension suffices.<n>We extend these results to the multi-hop setting, providing constructions with and without chain-of-thought that exhibit a provable
  arXiv  Detail & Related papers  (2026-05-12T17:22:22Z)
• Unifying Formal Explanations: A Complexity-Theoretic Perspective [9.350838775251075]
  We show that complexity of computations is influenced by three key properties of the value function.<n>We show that even highly simplified versions of these explanations become NP-hard to compute in the corresponding local explainability setting.
  arXiv  Detail & Related papers  (2026-02-20T11:52:26Z)
• Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem [0.2599882743586163]
  We present a formalization of the sigmoid function, proving its monotonicity, smoothness, and higher-order derivatives.<n>We provide a constructive proof of the Universal Approximation Theorem, demonstrating that neural networks with sigmoidal activation functions can approximate any continuous function on a compact interval.<n>Our work enhances trust in neural networks and contributes to the broader goal of verified and trustworthy machine learning.
  arXiv  Detail & Related papers  (2025-12-03T10:16:02Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Loss-Complexity Landscape and Model Structure Functions [56.01537787608726]
  We develop a framework for dualizing the Kolmogorov structure function $h_x(alpha)$.<n>We establish a mathematical analogy between information-theoretic constructs and statistical mechanics.<n>We explicitly prove the Legendre-Fenchel duality between the structure function and free energy.
  arXiv  Detail & Related papers  (2025-07-17T21:31:45Z)
• Emergence of Quantised Representations Isolated to Anisotropic Functions [0.0]
  This paper builds upon the existing Spotlight Resonance method to determine representational alignment.<n>A new tool is used to gain insight into how discrete representations can emerge and organise in autoencoder models.
  arXiv  Detail & Related papers  (2025-07-16T09:27:54Z)
• A Refreshed Similarity-based Upsampler for Direct High-Ratio Feature Upsampling [54.05517338122698]
  We propose an explicitly controllable query-key feature alignment from both semantic-aware and detail-aware perspectives. We also develop a fine-grained neighbor selection strategy on HR features, which is simple yet effective for alleviating mosaic artifacts. Our proposed ReSFU framework consistently achieves satisfactory performance on different segmentation applications.
  arXiv  Detail & Related papers  (2024-07-02T14:12:21Z)
• Nonparametric Partial Disentanglement via Mechanism Sparsity: Sparse Actions, Interventions and Sparse Temporal Dependencies [58.179981892921056]
  This work introduces a novel principle for disentanglement we call mechanism sparsity regularization. We propose a representation learning method that induces disentanglement by simultaneously learning the latent factors. We show that the latent factors can be recovered by regularizing the learned causal graph to be sparse.
  arXiv  Detail & Related papers  (2024-01-10T02:38:21Z)
• Flow Factorized Representation Learning [109.51947536586677]
  We introduce a generative model which specifies a distinct set of latent probability paths that define different input transformations. We show that our model achieves higher likelihoods on standard representation learning benchmarks while simultaneously being closer to approximately equivariant models.
  arXiv  Detail & Related papers  (2023-09-22T20:15:37Z)
• Refining and relating fundamentals of functional theory [0.0]
  We explain why there exist six equivalent universal functionals, prove concise relations among them and conclude that the important notion of $v$-representability is relative to the scope and choice of variable. For systems with time-reversal symmetry, we explain why there exist six equivalent universal functionals, prove concise relations among them and conclude that the important notion of $v$-representability is relative to the scope and choice of variable.
  arXiv  Detail & Related papers  (2023-01-24T18:09:47Z)
• Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version) [67.99023219822564]
  We introduce the general framework of relational action bases (RABs) RABs generalize existing models by lifting both restrictions. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes.
  arXiv  Detail & Related papers  (2022-08-12T17:03:50Z)
• On Neural Architecture Inductive Biases for Relational Tasks [76.18938462270503]
  We introduce a simple architecture based on similarity-distribution scores which we name Compositional Network generalization (CoRelNet) We find that simple architectural choices can outperform existing models in out-of-distribution generalizations.
  arXiv  Detail & Related papers  (2022-06-09T16:24:01Z)
• Adaptive n-ary Activation Functions for Probabilistic Boolean Logic [2.294014185517203]
  We show that we can learn arbitrary logic in a single layer using an activation function of matching or greater arity. We represent belief tables using a basis that directly associates the number of nonzero parameters to the effective arity of the belief function. This opens optimization approaches to reduce logical complexity by inducing parameter sparsity.
  arXiv  Detail & Related papers  (2022-03-16T22:47:53Z)
• Using Partial Monotonicity in Submodular Maximization [13.23676270963484]
  We show that for many standard submodular algorithms one can prove new approximation guarantees that depend on the monotonicity ratio. This leads to improved approximation ratios for the common machine learning applications of movie recommendation, quadratic programming and image summarization.
  arXiv  Detail & Related papers  (2022-02-07T10:35:40Z)
• First Power Linear Unit with Sign [0.0]
  It is enlightened by common inverse operation while endowed with an intuitive meaning of bionics. We extend the function presented to a more generalized type called PFPLUS with two parameters that can be fixed or learnable.
  arXiv  Detail & Related papers  (2021-11-29T06:47:58Z)
• A New Representation of Successor Features for Transfer across Dissimilar Environments [60.813074750879615]
  Many real-world RL problems require transfer among environments with different dynamics. We propose an approach based on successor features in which we model successor feature functions with Gaussian Processes. Our theoretical analysis proves the convergence of this approach as well as the bounded error on modelling successor feature functions.
  arXiv  Detail & Related papers  (2021-07-18T12:37:05Z)
• Concave Aspects of Submodular Functions [0.0]
  Submodular functions generalize several information-theoretic quantities such as entropy and mutual information. Submodular functions also show signs of concavity. We characterize the super-differentials and polyhedra associated with upper bounds and provide optimality conditions for submodular using the differentials.
  arXiv  Detail & Related papers  (2020-06-27T17:06:24Z)
• From Sets to Multisets: Provable Variational Inference for Probabilistic Integer Submodular Models [82.95892656532696]
  Submodular functions have been studied extensively in machine learning and data mining. In this work, we propose a continuous DR-submodular extension for integer submodular functions. We formulate a new probabilistic model which is defined through integer submodular functions.
  arXiv  Detail & Related papers  (2020-06-01T22:20:45Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.