SearcharxivSearch

arXiv subjects

Marek Jankola

Publications and source records attributed to Marek Jankola.

3 recordsLinked to original sources

Minority Takeover in Majority Dynamics: Searching for Rare Initializations via the History Passing Algorithm

We investigate how much bias in the initial configuration is required to drive global agreement in synchronous, deterministic majority dynamics on large random $d$-regular graphs. Nodes take values $\pm 1$ and update their states at each discrete time step to align with the majority of their neighbors. Using the backtracking dynamical cavity method (BDCM), we estimate the minimal fraction of initial $+1$ nodes required to achieve a $+1$ consensus in $p$ time steps. Our analysis predicts that for $d\geq4$ an initial global minority of $+1$ nodes is sufficient to quickly steer the entire system toward consensus on $+1$. We then investigate whether such initial conditions can be determined explicitly for a given large random regular graph. To this end, we introduce a new algorithm, which we name history-passing reinforcement (HPR), designed to find such initial configurations with a minority of $+1$ nodes. We find, as a main result, that the HPR algorithm finds initial configurations where the minority takes over the majority for $d$-regular random graphs with $d\geq4$. The HPR algorithm outperforms standard simulated annealing-based methods, but does not reach the lowest densities predicted by the BDCM. Rather, the lowest density achievable by the algorithm is near the onset of a dynamical one-step replica symmetry breaking (d1RSB) phase, which we estimate using a one-step replica symmetry breaking (1RSB) formulation of the BDCM. While we focus on the majority dynamics and random $d$-regular graphs, the algorithm can be extended to other dynamical rules and classes of sparse graphs.

cond-mat.dis-nn

A Modular Program-Transformation Framework for Reducing Specifications to Reachability

Software verification is a complex problem, and verification tools need significant tuning to achieve high performance. Due to this, many verifiers choose to specialize on reachability properties, or invest the time to implement known transformations from the given specification to reachability on their internal representations. To improve this situation, we provide transformations as stand-alone components, modifying the input program instead of the internal representation, enabling their usage as a preprocessing step by other verifiers. This way, we separate two concerns: improving the performance of reachability analyses and implementing efficient transformations of arbitrary specifications to reachability. We implement the transformations in a framework that is based on instrumentation automata, inspired by the BLAST query language. In our initial study, we support three important concrete specifications for C programs: termination, no-overflow, and memory cleanup. Moreover, we discuss the broader expressiveness of our framework and show how general liveness properties can be transformed to reachability. We demonstrate the effectiveness and efficiency of our transformations by comparing verifiers that support the specifications natively with verifiers for reachability applied on the transformed programs. The results are very promising: Our transformations can extend existing verifiers to be effective on specifications that they do not support natively, and that the efficiency is often similar to verifiers that natively support the considered specifications.

cs.PL

Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)

This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k -induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. It also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php.

cs.SE