@inproceedings{22006, abstract = {Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support. We provide the first robustness-based quantitative semantics for SFO, enabling the expression and evaluation of rich real-time properties beyond the scope of existing formalisms such as Signal Temporal Logic. To enable online monitoring, we identify a past-time fragment of SFO and give a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment. We then develop an efficient runtime monitoring algorithm for this past-time fragment and evaluate its performance on a set of benchmarks, demonstrating the practicality and effectiveness of our approach. To the best of our knowledge, this is the first publicly available prototype for online quantitative monitoring of full SFO.}, author = {Chalupa, Marek and Henzinger, Thomas A and Sarac, Naci E and Yu, Zhengqi}, booktitle = {27th International Symposium on Formal Methods}, isbn = {9783032262196}, issn = {1611-3349}, keywords = {Signal first-order logic, Robustness-based quantitative semantics, Online runtime monitoring}, location = {Tokyo, Japan}, pages = {214--233}, publisher = {Springer Nature}, title = {{Quantitative monitoring of Signal First-Order logic}}, doi = {10.1007/978-3-032-26220-2_11}, volume = {16557}, year = {2026}, } @inproceedings{21042, abstract = {Many blockchains such as Ethereum execute all incoming transactions sequentially significantly limiting the potential throughput. A common approach to scale execution is parallel execution engines that fully utilize modern multi-core architectures. Parallel execution is then either done optimistically, by executing transactions in parallel and detecting conflicts on the fly, or guided, by requiring exhaustive client transaction hints and scheduling transactions accordingly. However, recent studies have shown that the performance of parallel execution engines depends on the nature of the underlying workload. In fact, in some cases, only a 60% speed-up compared to sequential execution could be obtained. This is the case, as transactions that access the same resources must be executed sequentially. For example, if 10% of the transactions in a block access the same resource, the execution cannot meaningfully scale beyond 10 cores. Therefore, a single popular application can bottleneck the execution and limit the potential throughput. In this paper, we introduce Anthemius, a block construction algorithm that optimizes parallel transaction execution throughput. We evaluate Anthemius exhaustively under a range of workloads, and show that Anthemius enables the underlying parallel execution engine to process over twice as many transactions.}, author = {Neiheiser, Ray and Kokoris Kogias, Eleftherios}, booktitle = {29th International Conference on Financial Cryptography and Data Security}, isbn = {9783032070234}, issn = {1611-3349}, location = {Miyakojima, Japan}, pages = {307--323}, publisher = {Springer Nature}, title = {{Anthemius: Efficient and modular block assembly for concurrent execution}}, doi = {10.1007/978-3-032-07024-1_18}, volume = {15751}, year = {2026}, } @inproceedings{21044, abstract = {Scalability is a crucial requirement for modern large-scale systems, enabling elasticity and ensuring responsiveness under varying load. While cloud systems have achieved scalable architectures, blockchain systems remain constrained by the need to over-provision validator machines to handle peak load. This leads to resource inefficiency, poor cost scaling, and limits on performance. To address these challenges, we introduce Pilotfish, the first scale-out transaction execution engine for blockchains. Pilotfish enables validators to scale horizontally by distributing transaction execution across multiple worker machines, allowing elasticity without compromising consistency or determinism. It integrates seamlessly with the lazy blockchain architecture, completing the missing piece of execution elasticity. To achieve this, Pilotfish tackles several key challenges: ensuring scalable and strongly consistent distributed transactions, handling partial crash recovery with lightweight replication, and maintaining concurrency with a novel versioned-queue scheduling algorithm. Our evaluation shows that Pilotfish scales linearly up to at least eight workers per validator for compute-bound workloads, while maintaining low latency. By solving scalable execution, Pilotfish brings blockchains closer to achieving end-to-end elasticity, unlocking new possibilities for efficient and adaptable blockchain systems.}, author = {Kniep, Quentin and Kokoris Kogias, Eleftherios and Sonnino, Alberto and Zablotchi, Igor and Zhang, Nuda}, booktitle = {29th International Conference on Financial Cryptography and Data Security}, isbn = {9783032070234}, issn = {1611-3349}, location = {Miyakojima, Japan}, pages = {287--306}, publisher = {Springer Nature}, title = {{Pilotfish: Distributed execution for scalable blockchains}}, doi = {10.1007/978-3-032-07024-1_17}, volume = {15751}, year = {2026}, } @inproceedings{21134, abstract = {The Nakamoto consensus protocol underlying the Bitcoin blockchain uses proof of work as a voting mechanism. Honest miners who contribute hashing power towards securing the chain try to extend the longest chain they are aware of. Despite its simplicity, Nakamoto consensus achieves meaningful security guarantees assuming that at any point in time, a majority of the hashing power is controlled by honest parties. This also holds under “resource variability”, i.e., if the total hashing power varies greatly over time. Proofs of space (PoSpace) have been suggested as a more sustainable replacement for proofs of work. Unfortunately, no construction of a “longest-chain” blockchain based on PoSpace, that is secure under dynamic availability, is known. In this work, we prove that without additional assumptions no such protocol exists. We exactly quantify this impossibility result by proving a bound on the length of the fork required for double spending as a function of the adversarial capabilities. This bound holds for any chain selection rule, and we also show a chain selection rule (albeit a very strange one) that almost matches this bound. The Nakamoto consensus protocol underlying the Bitcoin blockchain uses proof of work as a voting mechanism. Honest miners who contribute hashing power towards securing the chain try to extend the longest chain they are aware of. Despite its simplicity, Nakamoto consensus achieves meaningful security guarantees assuming that at any point in time, a majority of the hashing power is controlled by honest parties. This also holds under “resource variability”, i.e., if the total hashing power varies greatly over time. Proofs of space (PoSpace) have been suggested as a more sustainable replacement for proofs of work. Unfortunately, no construction of a “longest-chain” blockchain based on PoSpace, that is secure under dynamic availability, is known. In this work, we prove that without additional assumptions no such protocol exists. We exactly quantify this impossibility result by proving a bound on the length of the fork required for double spending as a function of the adversarial capabilities. This bound holds for any chain selection rule, and we also show a chain selection rule (albeit a very strange one) that almost matches this bound. Concretely, we consider a security game in which the honest parties at any point control 0 > 1 times more space than the adversary. The adversary can change the honest space by a factor 1+- E with every block (dynamic availability), and “replotting” the space (which allows answering two challenges using the same space) takes as much time as p blocks. We prove that no matter what chain selection rule is used, in this game the adversary can create a fork of length o^2 . p/E that will be picked as the winner by the chain selection rule. We also provide an upper bound that matches the lower bound up to a factor o. There exists a chain selection rule (albeit a very strange one) which in the above game requires forks of length at least o . p/E Our results show the necessity of additional assumptions to create a secure PoSpace based longest-chain blockchain. The Chia network in addition to PoSpace uses a verifiable delay function. Our bounds show that an additional primitive like that is necessary.}, author = {Baig, Mirza Ahad and Pietrzak, Krzysztof Z}, booktitle = {29th International Conference on Financial Cryptography and Data Security}, isbn = {9783032070340}, issn = {1611-3349}, location = {Miyakojima, Japan}, pages = {127--142}, publisher = {Springer Nature}, title = {{On the (in)security of Proofs-of-space based longest-chain blockchains}}, doi = {10.1007/978-3-032-07035-7_8}, volume = {15752}, year = {2026}, } @inproceedings{21135, abstract = {Three-dimensional (3D) microscopy data is often anisotropic with significantly lower resolution (up to 8x) along the z axis than along the xy axes. Computationally generating plausible isotropic resolution from anisotropic imaging data would benefit the visual analysis of large-scale volumes. This paper proposes niiv, a self-supervised method for isotropic reconstruction of 3D microscopy data that can quickly produce images at arbitrary output resolutions. The representation embeds a learned latent code within a neural field that describes the implicit higher-resolution isotropic image region. We use an attention-guided latent interpolation approach, which allows flexible information exchange over a local latent neighborhood. Under isotropic volume assumptions, we self-supervise this representation on low-/high-resolution lateral image pairs to reconstruct an isotropic volume from low-resolution axial images. We evaluate our method on simulated and real anisotropic electron (EM) and light microscopy (LM) data. Compared to diffusion-based baselines, niiv shows improved reconstruction quality (+1 dB PSNR) and is over three orders of magnitude faster (1,000x) to infer. Specifically, niiv reconstructs a 128^3 voxel volume in 2/10th of a second, renderable at varying (continuous) high resolutions for display. Our code is available at https://github.com/jakobtroidl/niiv-miccai.}, author = {Troidl, Jakob and Liang, Yiqing and Beyer, Johanna and Tavakoli, Mojtaba and Danzl, Johann G and Hadwiger, Markus and Pfister, Hanspeter and Tompkin, James}, booktitle = {1st International Workshop on Efficient Medical Artificial Intelligence}, isbn = {9783032139603}, issn = {1611-3349}, location = {Daejeon, South Korea}, pages = {257--267}, publisher = {Springer Nature}, title = {{niiv: Interactive Self-supervised Neural Implicit Isotropic Volume Reconstruction}}, doi = {10.1007/978-3-032-13961-0_26}, volume = {16318}, year = {2026}, } @inproceedings{21374, abstract = {Let . S be a set of distinct points in general position in the Euclidean plane. A plane Hamiltonian path on . S is a crossing-free geometric path such that every point of .S is a vertex of the path. It is known that, if. S is sufficiently large, there exist three edge-disjoint plane Hamiltonian paths on . S. In this paper we study an edge-constrained version of the problem of finding Hamiltonian paths on a point set. We first consider the problem of finding a single plane Hamiltonian path . π with endpoints .s, t ∈ S and constraints given by a segment . ab, where .a, b ∈ S. We consider the following scenarios: (i) .ab ∈ π; (ii) .ab π. We characterize those quintuples . S, a, b, s, t for which . π exists. Secondly, we consider the problem of finding two plane Hamiltonian paths . π1, π2 on a set . S with constraints given by a segment . ab, where .a, b ∈ S. We consider the following scenarios: (i) .π1 and .π2 share no edges and .ab is an edge of . π1; (ii) .π1 and .π2 share no edges and none of them includes .ab as an edge; (iii) both .π1 and .π2 include .ab as an edge and share no other edges. In all cases, we characterize those triples . S, a, b for which .π1 and .π2 exist.}, author = {Antić, Todor and Džuklevski, Aleksa and Fiala, Jiří and Kratochvíl, Jan and Liotta, Giuseppe and Saghafian, Morteza and Saumell, Maria and Zink, Johannes}, booktitle = {51st International Conference on Current Trends in Theory and Practice of Computer Science}, isbn = {9783032178008}, issn = {1611-3349}, location = {Krakow, Poland}, pages = {532--546}, publisher = {Springer Nature}, title = {{Edge-constrained Hamiltonian paths on a point set}}, doi = {10.1007/978-3-032-17801-5_39}, volume = {16448}, year = {2026}, } @inproceedings{21410, abstract = {Given a finite set of red and blue points in R^d, the MST-ratio is defined as the total length of the Euclidean minimum spanning trees of the red points and the blue points, divided by the length of the Euclidean minimum spanning tree of their union. The MST-ratio has recently gained attention due to its direct interpretation in topological models for studying point sets with applications in spatial biology. The maximum MST-ratio of a point set is the maximum MST-ratio over all proper colorings of its points by red and blue. We prove that finding the maximum MST-ratio of a given point set is NP-hard when the dimension is part of the input. Moreover, we present a quadratic-time 3-approximation algorithm for this problem. As part of the proof, we show that in any metric space, the maximum MST-ratio is smaller than 3. Furthermore, we study the average MST-ratio over all colorings of a set of n points. We show that this average is always at least n-2/n-1, and for n random points uniformly distributed in a d-dimensional unit cube, the average tends to (math formular) in expectation as n approaches infinity.}, author = {Jabal Ameli, Afrouz and Motiei, Faezeh and Saghafian, Morteza}, booktitle = {20th International Conference and Workshops on Algorithms and Computation}, isbn = {9789819571260}, issn = {1611-3349}, location = {Perugia, Italy}, pages = {386--401}, publisher = {Springer Nature}, title = {{On the MST-ratio: Theoretical bounds and complexity of finding the maximum}}, doi = {10.1007/978-981-95-7127-7_26}, volume = {16444}, year = {2026}, } @inproceedings{22717, abstract = {We study concurrent graph games where n players cooperate against an opponent to reach a set of target states. Unlike traditional settings, we study distributed randomisation: team players do not share a source of randomness, and their private random sources are hidden from the opponent and from each other. We show that memoryless strategies are sufficient for the threshold problem (deciding whether there is a strategy for the team that ensures winning with probability that exceeds a threshold), a result that not only places the problem in the Existential Theory of the Reals (ER) but also enables the construction of value iteration algorithms. We additionally show that the threshold problem is NP-hard. For the almost-sure reachability problem, we prove NP-completeness. We introduce Individually Randomised Alternating-time Temporal Logic (IRATL). This logic extends the standard ATL framework to reason about probability thresholds, with semantics explicitly designed for coalitions that lack a shared source of randomness. On the practical side, we implement and evaluate a solver for the threshold and almost-sure problem based on the algorithms that we develop.}, author = {Brice, Leonard J and Henzinger, Thomas A and Montaseri, Alipasha and Shafiee, Ali and Thejaswini, K. S.}, booktitle = {38th International Conference on Computer Aided Verification}, isbn = {9783032325181}, issn = {1611-3349}, location = {Lisbon, Portugal}, pages = {215--236}, publisher = {Springer Nature}, title = {{Randomise alone, reach as a team}}, doi = {10.1007/978-3-032-32519-8_12}, volume = {16682}, year = {2026}, } @inproceedings{22719, abstract = {We study the problem of generating paths on a graph that satisfy a collection of w-regular objectives. We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler—oblivious to the graph and objective—dynamically composes these policies into a single path. We ask when such a composition satisfies all objectives, assuming their conjunction is realizable. The framework enables modular policy design but raises fundamental compositional challenges. We show that even extremely fair deterministic schedulers do not ensure correctness, and that stochastic schedulers, while necessary, are insufficient without coordination. For safety objectives, we demonstrate that fully decentralized implementations are impossible, and we introduce a protocol for synchronizing on maximal safe actions. For non-safety objectives, we introduce conventions—simple, a priori restrictions agreed upon before the graph or objectives are revealed—that guarantee satisfaction of all objectives when followed by all agents. We characterize minimally restrictive conventions for major subclasses of w-regular objectives. In particular, Büchi objectives admit universal composition of finite-memory policies without scheduler communication; co-Büchi objectives require only knowledge of whether the agent was scheduled; and parity objectives additionally require knowledge of which agent was scheduled.}, author = {Avni, Guy and Henzinger, Thomas A and Mallik, Kaushik and Sadhukhan, Suman and Thejaswini, K. S.}, booktitle = {38th International Conference on Computer Aided Verification}, isbn = {9783032325181}, issn = {1611-3349}, location = {Lisbon, Portugal}, pages = {237--257}, publisher = {Springer Nature}, title = {{Decoupled planning for multiple omega-regular objectives}}, doi = {10.1007/978-3-032-32519-8_13}, volume = {16682}, year = {2026}, } @inproceedings{22754, abstract = {Quantitative automata (QAs) extend finite-state automata on infinite words with weighted transitions to specify quantitative system properties. However, their finite weight sets rule out properties like average response time, where response times can be arbitrarily large. Nested quantitative automata (NQAs) overcome this limitation: a parent automaton spawns child automata to compute unbounded values over finite infixes and aggregates them into a final result. Despite this expressiveness, NQAs have lacked practical tool support to date. We close this gap by extending the Quantitative Automata Kit (QuAK), a software tool for QA analysis, to support NQAs. Our core contribution is implementing a suite of flattening procedures that reduce NQAs to QAs, leveraging QuAK’s existing decision procedures. These reductions preserve the answers to threshold decision problems, while allowing users to specify properties in the more expressive NQA formalism. The tool handles all combinations of parent aggregators (including limits and averages) and child functions (extrema and monotonic or bounded summations) for which emptiness and universality are known to be decidable. Experiments on response-time and resource-consumption benchmarks demonstrate QuAK’s effectiveness.}, author = {Henzinger, Thomas A and Mazzocchi, Nicolas Adrien and Sarac, Naci E and Yılmaz, Harun}, booktitle = {38th International Conference on Computer Aided Verification}, isbn = {9783032325259}, issn = {1611-3349}, location = {Lisbon, Portugal}, pages = {418--432}, publisher = {Springer Nature}, title = {{Extending QuAK with nested quantitative automata}}, doi = {10.1007/978-3-032-32526-6_20}, volume = {16683}, year = {2026}, } @inproceedings{22820, abstract = {We introduce a new primitive, called beholder signatures (Full version [14] of the paper is available at https://eprint.iacr.org/2025/1900), which, in some sense, are the opposite of blind signatures. In a beholder signature, one signs a commitment to a (potentially very long) message, and the signature attests that the parties participating in the signing process, who know the secret key, jointly also know the entire committed message. This guarantee holds even against distributed adversaries that use secure multi-party computation (MPC) to produce the signature. We work in the distributed adversarial model (Dziembowski, Faust, and Lizurej, Crypto’23), where one assumes that it is infeasible to evaluate a large number of hash queries without any of the participating parties learning the input. We propose a construction of beholder signatures in the random oracle model. The starting point of our construction is proofs of complete knowledge, recently proposed by (Kelkar et al. CCS’24), which build on Fischlin’s transformation of a sigma protocol to a non-interactive, straight-line extractable zero-knowledge proof of knowledge. Our scheme is concretely efficient and comes with a proof-of-concept implementation using Schnorr as the underlying sigma protocol. The primary applications of beholder signatures can be found within the blockchain space. In particular, we describe how to use them to construct proofs of custody (Feist, 2021) that do not require ephemeral keys and are non-interactive. We also outline applications to data dissemination, data availability, and proofs of replication.}, author = {Dziembowski, Stefan and Faust, Sebastian and Kedzior, Paweł and Mielniczuk, Marcin and Mohanty, Susil Kumar and Pietrzak, Krzysztof Z}, booktitle = {46th Annual International Cryptology Conference}, isbn = {9783032353733}, issn = {1611-3349}, location = {Santa Barbara, CA, United States}, pages = {134--165}, publisher = {Springer}, title = {{Beholder signatures}}, doi = {10.1007/978-3-032-35374-0_5}, volume = {16801}, year = {2026}, } @inproceedings{20845, abstract = {We develop new attacks against the Evasive LWE family of assumptions, in both the public and private-coin regime. To the best of our knowledge, ours are the first attacks against Evasive LWE in the public-coin regime, for any instantiation from the family. Our attacks are summarized below. Public-Coin Attacks. 1.The recent work by Hseih, Lin and Luo [17] constructed the first Attribute Based Encryption (ABE) for unbounded depth circuits by relying on the “circular” evasive LWE assumption. This assumption has been popularly considered as a safe, public-coin instance of Evasive LWE in contrast to its “private-coin” cousins (for instance, see [10, 11]). We provide the first attack against this assumption, challenging the widely held belief that this is a public-coin assumption. 2. We demonstrate a counter-example against vanilla public-coin evasive LWE by Wee [26] in an unnatural parameter regime. Our attack crucially relies on the error in the pre-condition being larger than the error in the post-condition, necessitating a refinement of the assumption. Private-Coin Attacks. 1. The recent work by Agrawal, Kumari and Yamada [2] constructed the first functional encryption scheme for pseudorandom functionalities (PRFE) and extended this to obfuscation for pseudorandom functionalities (PRIO) [4] by relying on private-coin evasive LWE. We provide a new attack against the assumption stated in the first posting of their work (subsequently refined to avoid these attacks). 2. The recent work by Branco et al. [8] (concurrently to [4]) provides a construction of obfuscation for pseudorandom functionalities by relying on private-coin evasive LWE. We provide a new attack against their stated assumption. 3. Branco et al. [8] showed that there exist contrived, “self-referential” classes of pseudorandom functionalities for which pseudorandom obfuscation cannot exist. We extend their techniques to develop an analogous result for pseudorandom functional encryption. While Evasive LWE was developed to specifically avoid “zeroizing attacks”, our work shows that in certain settings, such attacks can still apply.}, author = {Agrawal, Shweta and Modi, Anuja and Yadav, Anshu and Yamada, Shota}, booktitle = {23rd International Conference on Theory of Cryptography}, isbn = {9783032122926}, issn = {1611-3349}, location = {Aarhus, Denmark}, pages = {259--290}, publisher = {Springer Nature}, title = {{Zeroizing attacks against evasive and circular evasive LWE}}, doi = {10.1007/978-3-032-12293-3_9}, volume = {16269}, year = {2025}, } @inproceedings{20846, abstract = {CVRFs are PRFs that unify the properties of verifiable and constrained PRFs. Since they were introduced concurrently by Fuchsbauer and Chandran-Raghuraman-Vinayagamurthy in 2014, it has been an open problem to construct CVRFs without using heavy machinery such as multilinear maps, obfuscation or functional encryption. We solve this problem by constructing a prefix-constrained verifiable PRF that does not rely on the aforementioned assumptions. Essentially, our construction is a verifiable version of the Goldreich-Goldwasser-Micali PRF. To achieve verifiability we leverage degree-2 algebraic PRGs and bilinear groups. In short, proofs consist of intermediate values of the Goldreich-Goldwasser-Micali PRF raised to the exponents of group elements. These outputs can be verified using pairings since the underlying PRG is of degree 2. We prove the selective security of our construction under the Decisional Square Diffie-Hellman (DSDH) assumption and a new assumption, which we dub recursive Decisional Diffie-Hellman (recursive DDH). We prove the soundness of recursive DDH in the generic group model assuming the hardness of the Multivariate Quadratic (MQ) problem and a new variant thereof, which we call MQ+. Last, in terms of applications, we observe that our CVRF is also an exponent (C)VRF in the plain model. Exponent VRFs were recently introduced by Boneh et al. (Eurocrypt’25) with various applications to threshold cryptography in mind. In addition to that, we give further applications for prefix-CVRFs in the blockchain setting, namely, stake-pooling and compressible randomness beacons.}, author = {Brandt, Nicholas and Cueto Noval, Miguel and Günther, Christoph Ullrich and Ünal, Akin and Wohnig, Stella}, booktitle = {23rd International Conference on Theory of Cryptography}, isbn = {9783032122896}, issn = {1611-3349}, location = {Aarhus, Denmark}, pages = {478--511}, publisher = {Springer Nature}, title = {{Constrained verifiable random functions without obfuscation and friends}}, doi = {10.1007/978-3-032-12290-2_16}, volume = {16271}, year = {2025}, } @inproceedings{21091, abstract = {Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates.}, author = {Henzinger, Thomas A and Kueffner, Konstantin and Yu, Zhengqi}, booktitle = {25th International Conference on Runtime Verification}, issn = {1611-3349}, location = {Graz, Austria}, pages = {54--72}, publisher = {Springer Nature}, title = {{Formal verification of neural certificates done dynamically}}, doi = {10.1007/978-3-032-05435-7_4}, volume = {16087}, year = {2025}, } @inproceedings{21092, abstract = {Formal verification provides assurances that a probabilistic system satisfies its specification—conditioned on the system model being aligned with reality. We propose alignment monitoring to watch that this assumption is justified. We consider a probabilistic model well aligned if it accurately predicts the behaviour of an uncertain system in advance. An alignment score measures this by quantifying the similarity between the model’s predicted and the system’s (unknown) actual distributions. An alignment monitor observes the system at runtime; at each point in time it uses the current state and the model to predict the next state. After the next state is observed, the monitor updates the verdict, which is a high-probability interval estimate for the true alignment score. We utilize tools from sequential forecasting to construct our alignment monitors. Besides a monitor for measuring the expected alignment score, we introduce a differential alignment monitor, designed for comparing two models, and a weighted alignment monitor, which permits task-specific alignment monitoring. We evaluate our monitors experimentally on the PRISM benchmark suite. They are fast, memory-efficient, and detect misalignment early.}, author = {Henzinger, Thomas A and Kueffner, Konstantin and Singh, Vasu and Sun, I}, booktitle = {25th International Conference on Runtime Verification}, issn = {1611-3349}, location = {Graz, Austria}, pages = {140--159}, publisher = {Springer Nature}, title = {{Alignment monitoring}}, doi = {10.1007/978-3-032-05435-7_9}, volume = {16087}, year = {2025}, } @inproceedings{21093, abstract = {We propose a monitoring approach for hyperproperties where the system’s observations range over infinite domains. The specifications are given as formulas of symbolic hypernode logic, an extension of earlier versions of hypernode logic that supports events with data. We demonstrate how to translate terms of symbolic hypernode logic into multi-tape symbolic transducers and we present a monitoring algorithm for universally quantified formulas that is based on this translation. We evaluate our approach against the previous approach for monitoring hypernode logic, and we also compare it to other monitors for hyperproperties.}, author = {Chalupa, Marek and Henzinger, Thomas A and Oliveira da Costa, Ana A}, booktitle = {25th International Conference on Runtime Verification}, issn = {1611-3349}, location = {Graz, Austria}, pages = {417--437}, publisher = {Springer Nature}, title = {{Monitoring hypernode logic over infinite domains}}, doi = {10.1007/978-3-032-05435-7_23}, volume = {16087}, year = {2025}, } @inproceedings{21323, abstract = {We present a unifying framework for proving the knowledge-soundness of KZG-like polynomial commitment schemes, encompassing both univariate and multivariate variants. By conceptualizing the proof technique of Lipmaa, Parisella, and Siim for the univariate KZG scheme (EUROCRYPT 2024), we present tools and falsifiable hardness assumptions that permit black-box extraction of the multivariate KZG scheme. Central to our approach is the notion of a canonical Proof-of-Knowledge of a Polynomial (PoKoP) of a polynomial commitment scheme, which we use to capture the extractability notion required in constructions of practical zk-SNARKs. We further present an explicit polynomial decomposition lemma for multivariate polynomials, enabling a more direct analysis of interpolating extractors and bridging the gap between univariate and multivariate commitments. Our results provide the first standard-model proofs of extractability for the multivariate KZG scheme and many of its variants under falsifiable assumptions.}, author = {Belohorec, Juraj and Dvořák, Pavel and Hoffmann, Charlotte and Hubáček, Pavel and Mašková, Kristýna and Pastyřík, Martin}, booktitle = {45th Annual International Cryptology Conference}, isbn = {9783032018861}, issn = {1611-3349}, location = {Santa Barbara, CA, United States}, pages = {584--616}, publisher = {Springer Nature}, title = {{On extractability of the KZG family of polynomial commitment schemes}}, doi = {10.1007/978-3-032-01887-8_19}, volume = {16005}, year = {2025}, } @inproceedings{19375, abstract = {Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such huge MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs. The idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools.}, author = {Azeem, Muqsit and Chakraborty, Debraj and Kanav, Sudeep and Kretinsky, Jan and Mohagheghi, Mohammadsadegh and Mohr, Stefanie and Weininger, Maximilian}, booktitle = {26th International Conference on Verification, Model Checking, and Abstract Interpretation}, isbn = {9783031827020}, issn = {1611-3349}, location = {Denver, CO, United States}, pages = {97--120}, publisher = {Springer Nature}, title = {{1–2–3–Go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization}}, doi = {10.1007/978-3-031-82703-7_5}, volume = {15530}, year = {2025}, } @inproceedings{19445, abstract = {In reconfiguration, we are given two solutions to a graph problem, such as Vertex Cover or Dominating Set, with each solution represented by a placement of tokens on vertices of the graph. Our task is to reconfigure one into the other using small steps while ensuring the intermediate configurations of tokens are also valid solutions. The two commonly studied settings are Token Jumping and Token Sliding, which allows moving a single token to an arbitrary or an adjacent vertex, respectively. We introduce new rules that generalize Token Jumping, parameterized by the number of tokens allowed to move at once and by the maximum distance of each move. Our main contribution is identifying minimal rules that allow reconfiguring any possible given solution into any other for Independent Set, Vertex Cover, and Dominating Set. For each minimal rule, we also provide an efficient algorithm that finds a corresponding reconfiguration sequence. We further focus on the rule that allows each token to move to an adjacent vertex in a single step. This natural variant turns out to be the minimal rule that guarantees reconfigurability for Vertex Cover. We determine the computational complexity of deciding whether a (shortest) reconfiguration sequence exists under this rule for the three studied problems. While reachability for Vertex Cover is shown to be in P, finding a shortest sequence is shown to be NP-complete. For Independent Set and Dominating Set, even reachability is shown to be PSPACE-complete.}, author = {Křišťan, Jan Matyáš and Svoboda, Jakub}, booktitle = {19th International Conference and Workshops on Algorithms and Computation}, isbn = {9789819628445}, issn = {1611-3349}, location = {Chengdu, China}, pages = {244--265}, publisher = {Springer Nature}, title = {{Reconfiguration using generalized token jumping}}, doi = {10.1007/978-981-96-2845-2_16}, volume = {15411}, year = {2025}, } @inproceedings{19600, abstract = {In this work, we explore route discovery in private payment channel networks. We first determine what “ideal" privacy for a routing protocol means in this setting. We observe that protocols achieving this strong privacy definition exist by leveraging Multi-Party Computation but they are inherently inefficient as they must involve the entire network. We then present protocols with weaker privacy guarantees but much better efficiency (involving only a small fraction of the nodes). The core idea is that both sender and receiver gossip a message which propagates through the network, and the moment any node in the network receives both messages, a path is found. In our first protocol the message is always sent to all neighbouring nodes with a delay proportional to the fees of that edge. In our second protocol the message is only sent to one neighbour chosen randomly with a probability proportional to its degree. We additionally propose a more realistic notion of privacy in order to measure the privacy leakage of our protocols in practice. Our realistic notion of privacy challenges an adversary that join the network with a fixed budget to create channels to guess the sender and receiver of a transaction upon receiving messages from our protocols. Simulations of our protocols on the Lightning network topology (for random transactions and uniform fees) show that 1) forming edges with high degree nodes is a more effective attack strategy for the adversary, 2) there is a tradeoff between the number of nodes involved in our protocols (privacy) and the optimality of the discovered path, and 3) our protocols involve a very small fraction of the network on average.}, author = {Avarikioti, Zeta and Bastankhah, Mahsa and Maddah-Ali, Mohammad Ali and Pietrzak, Krzysztof Z and Svoboda, Jakub and Yeo, Michelle X}, booktitle = {Computer Security. ESORICS 2024 International Workshops}, isbn = {9783031823480}, issn = {1611-3349}, location = {Bydgoszcz, Poland}, pages = {207--223}, publisher = {Springer Nature}, title = {{Route discovery in private payment channel networks}}, doi = {10.1007/978-3-031-82349-7_15}, volume = {15263}, year = {2025}, }