Search

The Longest-Edge (LE) trisection of a triangle is obtained by joining the two points which divide the longest edge in three with the opposite vertex. If LE-trisection is iteratively applied to an initial triangle, then the maximum diameter of the resulting triangles is between two sharpened decreasing functions. This paper mathematically answers the question of how fast the diameters of a triangle mesh tend to zero as repeated trisection is performed, and completes the previous empirical studies presented in the MASCOT 2010 Meeting (Perdomo et al., 2010).

In this paper, a single phase cascaded H-bridge inverter with s variable dc sources ( s ≥ 2 ), l = 2 s + 1 levels has been considered. A mathematical proof is presented to demonstrate that, under a particular choice of the switching angles, which number corresponds to the number of dc sources i.e. s , and of the dc voltages, all harmonics are eliminated from the output voltage waveform, except those of order n = 4 p ⋅ s ± 1 , p = 1 , 2 , … . With this method, the dc voltage sources vary linearly according to the modulation index m , while the switching angles do not depend on m . The resulting output voltage has low total harmonic distortion, that remains independent on m . Compared to a conventional selective harmonic elimination procedure and to a pulse amplitude method, the proposed procedure reduces distortion in a wide range of modulation index.

Trust in the correctness of an election outcome requires proof of the correctness of vote counting. By formalising particular voting protocols as rules, correctness of vote counting amounts to verifying that all rules have been applied correctly. A proof of the outcome of any particular election then consists of a sequence (or tree) of rule applications and provides an independently checkable certificate of the validity of the result. This reduces the need to trust, or otherwise verify, the correctness of the vote counting software once the certificate has been validated. Using a rule-based formalisation of voting protocols inside a theorem prover, we synthesise vote counting programs that are not only provably correct, but also produce independently verifiable certificates. These programs are generated from a (formal) proof that every initial set of ballots allows to decide the election winner according to a set of given rules.

A new approach of general systems theory is used to study the feasibility of the definition of the theory so‐called the science of science. General scientific theory is studied as a system. The technique, well used by Bertrand Russell in his famous Russell paradox, is applied to show that the theory of science of science cannot exist. A new definition of the theory of science of science is given, so that paradoxes similar to Russell's paradox will not occur in the new theory of science of science developed on the new definition.

Comunicació presentada al AFRICACRYPT 2020: 12th International Conference on Cryptology in Africa, celebrat del 20 al 22 de juliol de 2021 al Caire, Egipte. This paper constructs unbounded simulation sound proofs for boolean circuit satisfiability under standard assumptions with proof size O(n+d) bilinear group elements, where d is the depth and n is the input size of the circuit. Our technical contribution is to add unbounded simulation soundness to a recent NIZK of González and Ràfols (ASIACRYPT’19) with very small overhead. Our new scheme can be used to construct the most efficient Signature-of-Knowledge based on standard assumptions that also can be composed universally with other cryptographic protocols/primitives. Karim Baghery was supported by CyberSecurity Research Flanders with reference number VR20192203.

International audience; In this paper we enhance the EasyCrypt proof assistant to reason about computational complexity of adversaries. The key technical tool is a Hoare logic for reasoning about computational complexity (execution time and oracle calls) of adversarial computations. Our Hoare logic is built on top of the module system used by EasyCrypt for modeling adversaries. We prove that our logic is sound w.r.t. the semantics of EasyCrypt programs-we also provide full semantics for the EasyCrypt module system, which was previously lacking. We showcase (for the first time in EasyCrypt and in other computer-aided cryptographic tools) how our approach can express precise relationships between the probability of adversarial success and their execution time. In particular, we can quantify existentially over adversaries in a complexity class, and express general composition statements in simulation-based frameworks. Moreover, such statements can be composed to derive standard concrete security bounds for cryptographic constructions whose security is proved in a modular way. As a main benefit of our approach, we revisit security proofs of some well-known cryptographic constructions and we present a new formalization of Universal Composability (UC).

Password-based authenticated key exchange (PAKE) protocol allows protocol participants to establish a high entropy session key by pre-sharing a low-entropy password. Katz and Vaikuntanathan (ASIACRYPT'09) used a one-round smooth projective hash function (SPHF) over lattices to design a three-round PAKE protocol. Zhang and Yu (AISACRYPT'17) improved Katz-Vaikuntanatha's scheme by proposing a two-round PAKE with NIZK proofs, but how to construct a lattice-based simulation-sound NIZK remains an open research question. Benhamouda et al. followed the framework of Katz and Vaikuntananthan (TCC'11) and proposed a one-round PAKE via trapdoor-SPHF, but their scheme was based on conventional DDH assumption. In other words, how to design a one-round PAKE via an efficient lattice-based SPHF still remains a challenge. In this paper, we attempt to fill this gap by first proposing a new IND-CCA-secure lattice-based SPHF based on the work of Benhamouda et al. (PKC'18), and then using the proposed SPHF to construct a one-round PAKE protocol. We then prove the security of the proposed protocol. We also explore the possibilities of constructing two-round PAKE, three-round PAKE and universal composable security from our SPHF, and show the potential application of our PAKE in the Internet of Things where communication cost is the main consideration.

The expensive cost and intermittent availability of renewable energy bring great challenges to its efficient utilization in green data centers. In this paper, we propose a new way to achieve an explicit trade-off between operational cost and carbon emission by dynamic storing off-site renewable energy in distributed data centers. We first formulate a constrained stochastic optimization problem for cost minimization of data centers. Then, by leveraging Lyapunov optimization theory, we design an online Carbon Capped Cost Minimization algorithm (CCCM) to achieve a near-optimal cost with rigorous mathematical proof. Specially, the decisions at each time slot are determined with an efficient iterative algorithm based on the Generalized Benders Decomposition (GBD) technique. Finally, extensive simulations are conducted to show the effectiveness of our algorithm. The results show that our algorithm can save about 6% total costs compared with the algorithm without offsite energy storage.

Model management is a central activity in Software Engineering. The most challenging aspect of model management is to keep inter-related models consistent with each other while they evolve. As a consequence, there is a lot of scientific activity in this area, which has produced an extensive body of knowledge, methods, results and tools. The majority of these approaches, however, are limited to binary inter-model relations; i.e. the synchronisation of exactly two models. Yet, not every multi-ary relation can be factored into a family of binary relations. In this paper, we propose and investigate a novel comprehensive system construction, which is able to represent multi-ary relations among multiple models in an integrated manner and thus serves as a formal foundation for artefacts used in consistency management activities involving multiple models. The construction is based on the definition of partial commonalities among a set of models using the same language, which is used to denote the (local) models. The main theoretical results of this paper are proofs of the facts that comprehensive systems are an admissible environment for (i) applying formal means of consistency verification (diagrammatic predicate framework), (ii) performing algebraic graph transformation (weak adhesive HLR category), and (iii) that they generalise the underlying setting of graph diagrams and triple graph grammars.

We construct a 1-round delegation scheme (i.e., argument-system) for every language computable in time t = t ( n ), where the running time of the prover is poly ( t ) and the running time of the verifier is n · polylog ( t ). In particular, for every language in P we obtain a delegation scheme with almost linear time verification. Our construction relies on the existence of a computational sub-exponentially secure private information retrieval ( PIR ) scheme. The proof exploits a curious connection between the problem of computation delegation and the model of multi-prover interactive proofs that are sound against no-signaling (cheating) strategies , a model that was studied in the context of multi-prover interactive proofs with provers that share quantum entanglement, and is motivated by the physical principle that information cannot travel faster than light. For any language computable in time t = t ( n ), we construct a multi-prover interactive proof ( MIP ), that is, sound against no-signaling strategies, where the running time of the provers is poly ( t ), the number of provers is polylog ( t ), and the running time of the verifier is n · polylog ( t ). In particular, this shows that the class of languages that have polynomial-time MIP s that are sound against no-signaling strategies, is exactly EXP . Previously, this class was only known to contain PSPACE . To convert our MIP into a 1-round delegation scheme, we use the method suggested by Aiello et al. (ICALP, 2000), which makes use of a PIR scheme. This method lacked a proof of security. We prove that this method is secure assuming the underlying MIP is secure against no-signaling provers.

Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this paper, we will survey the use of structural proof theory as an alternative foundation. Researchers have been using this foundation for the past 35 years to elevate logic programming from its roots in first-order classical logic into higher-order versions of intuitionistic and linear logic. These more expressive logic programming languages allow for capturing stateful computations and rich forms of abstractions, including higher-order programming, modularity, and abstract data types. Term-level bindings are another kind of abstraction, and these are given an elegant and direct treatment within both proof theory and these extended logic programming languages. Logic programming has also inspired new results in proof theory, such as those involving polarity and focused proofs. These recent results provide a high-level means for presenting the differences between forward-chaining and backward-chaining style inferences. Anchoring logic programming in proof theory has also helped identify its connections and differences with functional programming, deductive databases, and model checking., To appear in Theory and Practice of Logic Programming (TPLP)

Fuzzy extractor can be used to convert the reading of a noisy non-uniform source into a reliably reproducible and almost uniform string, while reusable fuzzy extractor allows multiple extractions of the same source. In this paper, we propose multi-party fuzzy extractor, called threshold reusable fuzzy extractor, whose execution requires a threshold number of members. New definition and efficient construction are given with security proofs and experimental implementations. It preserves the inherent properties of fuzzy extractor with expanded use in multi-party scenarios. Based on the proposed threshold reusable fuzzy extractor, an application in privacy protection is given to store and share sensitive data by smart contract on blockchain , achieving joint access control via biometric information.

Note from the Research Highlights Co-Chairs: A Research Highlights paper appearing in Communications is usually peer-reviewed prior to publication. The following paper is unusual in that it is still under review. However, the result has generated enormous excitement in the research community, and came strongly nominated by SIGACT, a nomination seconded by external reviewers. The complexity class NP characterizes the collection of computational problems that have efficiently verifiable solutions. With the goal of classifying computational problems that seem to lie beyond NP, starting in the 1980s complexity theorists have considered extensions of the notion of efficient verification that allow for the use of randomness (the class MA), interaction (the class IP), and the possibility to interact with multiple proofs, or provers (the class MIP). The study of these extensions led to the celebrated PCP theorem and its applications to hardness of approximation and the design of cryptographic protocols. In this work, we study a fourth modification to the notion of efficient verification that originates in the study of quantum entanglement. We prove the surprising result that every problem that is recursively enumerable, including the Halting problem, can be efficiently verified by a classical probabilistic polynomial-time verifier interacting with two all-powerful but noncommunicating provers sharing entanglement. The result resolves long-standing open problems in the foundations of quantum mechanics (Tsirelson's problem) and operator algebras (Connes' embedding problem).

Privacy-preserving federated learning is distributed machine learning where multiple collaborators train a model through protected gradients. To achieve robustness to users dropping out, existing practical privacy-preserving federated learning schemes are based on ( t, N)-threshold secret sharing. Such schemes rely on a strong assumption to guarantee security: the threshold t must be greater than half of the number of users. The assumption is so rigorous that in some scenarios the schemes may not be appropriate. Motivated by the issue, we first introduce membership proof for federated learning, which leverages cryptographic accumulators to generate membership proofs by accumulating user IDs. The proofs are issued in a public blockchain for users to verify. With membership proof, we propose a privacy-preserving federated learning scheme called PFLM. PFLM releases the assumption of threshold while maintaining the security guarantees. Additionally, we design a result verification algorithm based on a variant of ElGamal encryption to verify the correctness of aggregated results from the cloud server. The verification algorithm is integrated into PFLM as a part. Security analysis in a random oracle model shows that PFLM guarantees privacy against active adversaries. The implementation of PFLM and experiments demonstrate the performance of PFLM in terms of computation and communication.

We give a transport proof of a discrete version of the displacement convexity of entropy on integers (Z), and get, as a consequence, two discrete forms of the Prekopa-Leindler Inequality : the Four Functions Theorem of Ahlswede and Daykin on the discrete hypercube [1] and a recent result on Z due to Klartag and Lehec [16].

This article is motivated by seeking lower bounds on OBDD(∧, w, r) refutations, namely, OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1 - NBP ∧ refutations based on read-once nondeterministic branching programs. These generalize OBDD(∧, r) refutations. There are polynomial size 1 - NBP(∧) refutations of the pigeonhole principle, hence 1-NBP(∧) is strictly stronger than OBDD}(∧, r). There are also formulas that have polynomial size tree-like resolution refutations but require exponential size 1-NBP(∧) refutations. As a corollary, OBDD}(∧, r) does not simulate tree-like resolution, answering a previously open question. The system 1-NBP(∧, ∃) uses projection inferences instead of weakening. 1-NBP(∧, ∃ k is the system restricted to projection on at most k distinct variables. We construct explicit constant degree graphs G n on n vertices and an ε > 0, such that 1-NBP(∧, ∃ ε n ) refutations of the Tseitin formula for G n require exponential size. Second, we study the proof system OBDD}(∧, w, r ℓ ), which allows ℓ different variable orders in a refutation. We prove an exponential lower bound on the complexity of tree-like OBDD(∧, w, r ℓ ) refutations for ℓ = ε log n , where n is the number of variables and ε > 0 is a constant. The lower bound is based on multiparty communication complexity.

Memory allocation and deallocation are the fundamental operations of embedded operating systems, which have been extensively used in many safety critical systems. The correctness of the operations is of paramount importance because their failure could incur severe consequences. While the system is running, the memory state can easily grow to a gigantic amount, which means that it is impossible to verify the huge memory states one by one. Therefore, it is a challenge how to verify the correctness of running memory state of the system. In this article, we propose a novel memory state verification method based on inductive and deductive reasoning. First, we abstract the memory state as a list of memory blocks, which will transform in memory operations. Second, we construct the generic model based on the transition function of the memory management and summarize the invariant properties of the memory state. Third, we use the inductive method to calculate the changes between the memory states, and verify that the memory state of the system always satisfy the global properties. All the proofs are implemented in the interactive theorem prover Coq. On the basis of our proposed model, we verify the correctness of a two-level segregated fit (TLSF) algorithm through some extensions, and we also apply this method to verify the correctness of the memory state of the embedded system at runtime.

The calculus of Dependent Object Types (DOT) has enabled a more principled and robust implementation of Scala, but its support for type-level computation has proven insufficient. As a remedy, we propose F ·· ω , a rigorous theoretical foundation for Scala’s higher-kinded types. F ·· ω extends F ω with interval kinds , which afford a unified treatment of important type- and kind-level abstraction mechanisms found in Scala, such as bounded quantification, bounded operator abstractions, translucent type definitions and first-class subtyping constraints. The result is a flexible and general theory of higher-order subtyping. We prove type and kind safety of F ·· ω , as well as weak normalization of types and undecidability of subtyping. All our proofs are mechanized in Agda using a fully syntactic approach based on hereditary substitution.

Class imbalance is one of the most popular and important issues in the domain of classification. The AdaBoost algorithm is an effective solution for classification, but it still needs improvement in the imbalanced data problem. This paper proposes a method to improve the AdaBoost algorithm using the new weighted vote parameters for the weak classifiers. Our proposed weighted vote parameters are determined not only by the global error rate but also by the classification accuracy rate of the positive class, which is our primary interest. The imbalanced index of the data is also a factor in constructing our algorithms. Our proposed algorithms outperform the traditional ones, especially regarding the evaluation criterion of F - 1 Measure . Theoretic proofs of the advantages of our proposed algorithms are presented. Two kinds of simulated datasets and four real datasets are applied in the experiment as the specific support to our proposed algorithms.

We develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mechanism with a counterexample-guided abstraction refinement scheme for the theory of arrays. Our framework can thus, in many cases, reduce inductive reasoning with quantifiers and arrays to quantifier-free and array-free reasoning. We evaluate the approach on a wide set of benchmarks from the literature. The results show that our implementation often outperforms state-of-the-art tools, demonstrating its practical potential.

A nonzero integral flow f is conformally decomposable if $$f=f_1+f_2$$ , where $$f_1,f_2$$ are nonzero integral flows, both are nonnegative or both are nonpositive. Conformally indecomposable flows on ordinary graphs are simply graph circuit flows. However, on signed graphs without outer-edges (compact case), conformally indecomposable flows, classified by Chen and Wang (arXiv:1112.0642, 2013) and by Chen et al. (Discret Math 340:1271–1286, 2017), are signed-graph circuit flows plus an extra class of characteristic flows of so-called Eulerian circle-trees. This paper is to classify indecomposable conformal integral flows on signed graphs with outer-edges (non-compact case). A notable feature is that with outer-edges the treatment is natural and results become stronger but proofs are simpler than that without outer-edges.

Axiom selection is a task that selects the most likely useful axioms from a large-scale axiom set for proving a given conjecture. Existing axiom selection methods either solely take shallow symbols into account or strongly dependent on previous successful proofs from homologous problems. To address these problems, we introduce a new metric to evaluate the dissimilarity between formulae and utilize it as an evaluator in the selection task. Firstly, we propose a substitution-based metric to compute the dissimilarity between terms. It is a pseudo-metric and can capture the in-depth syntactic difference trigged by both functional and variable subterms. We then extend it to atoms and prove the atom metric also to be a pseudo-metric. Treating formulae as atom sets, we define three kinds of dissimilarity metrics between formulae. Finally, we design and implement conjecture-oriented axiom selection methods based on newly proposed formula metrics. The experimental evaluation is conducted on the MPTP2078 benchmark and demonstrates dissimilarity-based axiom selection improves E prover’s performance. In the best case, it increases the ratio of successful proofs from 30.90% to 42.25%.

In this work, we show negative results on the tamper-resilience of a wide class of cryptographic primitives with uniqueness properties, such as unique signatures, verifiable random functions, signatures with unique keys, injective one-way functions, and encryption schemes with a property we call unique-message property. Concretely, we prove that for these primitives, it is impossible to derive their (even extremely weak) tamper-resilience from any common assumption, via black-box reductions. Our proofs exploit the simulatable attack paradigm proposed by Wichs (ITCS ’13), and the tampering model we treat is the plain model, where there is no trusted setup.

We show that every connected graph can be approximated by a normal tree, up to some arbitrarily small error phrased in terms of neighbourhoods around its ends. The existence of such approximate normal trees has consequences of both combinatorial and topological nature. On the combinatorial side, we show that a graph has a normal spanning tree as soon as it has normal spanning trees locally at each end; i.e., the only obstruction for a graph to having a normal spanning tree is an end for which none of its neighbourhoods has a normal spanning tree. On the topological side, we show that the end space $\Omega(G)$, as well as the spaces $|G| = G \cup \Omega(G)$ naturally associated with a graph $G$, are always paracompact. This gives unified and short proofs for a number of results by Diestel, Spr\"ussel and Polat, and answers an open question about metrizability of end spaces by Polat., Comment: 9 pages

Separation logic (SL) is a logical formalism for reasoning about programs that use pointers to mutate data structures. It is successful for program verification as an assertion language to state properties about memory heaps using Hoare triples. Most of the proof systems and verification tools for ${\textrm{SL}}$ focus on the decidable but rather restricted symbolic heaps fragment. Moreover, recent proof systems that go beyond symbolic heaps are purely syntactic or labelled systems dedicated to some fragments of ${\textrm{SL}}$ and they mainly allow either the full set of connectives, or the definition of arbitrary inductive predicates, but not both. In this work, we present a labelled proof system, called ${\textrm{G}_{\textrm{SL}}}$, that allows both the definition of cyclic proofs with arbitrary inductive predicates and the full set of SL connectives. We prove its soundness and show that we can derive in ${\textrm{G}_{\textrm{SL}}}$ the built-in rules for data structures of another non-cyclic labelled proof system and also that ${\textrm{G}_{\textrm{SL}}}$ is strictly more powerful than that system.

The classical NP-hard feedback arc set problem (FASP) and feedback vertex set problem (FVSP) ask for a minimum set of arcs $\varepsilon \subseteq E$ or vertices $\nu \subseteq V$ whose removal $G\setminus \varepsilon$, $G\setminus \nu$ makes a given multi-digraph $G=(V,E)$ acyclic, respectively. Though both problems are known to be APX-hard, approximation algorithms or proofs of inapproximability are unknown. We propose a new $\mathcal{O}(|V||E|^4)$-heuristic for the directed FASP. While a ratio of $r \approx 1.3606$ is known to be a lower bound for the APX-hardness, at least by empirical validation we achieve an approximation of $r \leq 2$. The most relevant applications, such as circuit testing, ask for solving the FASP on large sparse graphs, which can be done efficiently within tight error bounds due to our approach., Comment: manuscript submitted to ACM

Representation predicates enable data abstraction in separation logic, but when the same concrete implementation may need to be abstracted in different ways, one needs a notion of subsumption. We demonstrate function-specification subtyping, analogous to subtyping, with a subsumption rule: if \(\phi \) is a Open image in new window of \(\psi \), that is \(\phi

UNITY is a model for concurrent specifications with a complete logic for proving progress properties of the form “ P leads to Q ”. UNITY is generalized to U-specifications by giving more freedom to specify the steps that are to be taken infinitely often. In particular, these steps can correspond to non-total relations. The generalization keeps the logic sound and complete. The paper exploits the generalization in two ways. Firstly, the logic remains sound when the specification is extended with hypotheses of the form “ F leads to G ”. As the paper shows, this can make the logic incomplete. The generalization is used to show that the logic remains complete, if the added hypotheses “ F leads to G ” satisfy “ F unless G ”. The main result extends the applicability and completeness of UNITY logic to proofs that a given concurrent program satisfies any given formula of LTL, linear temporal logic, without the next-operator which is omitted because it is sensitive to stuttering. For this purpose, the program, written as a UNITY program, is extended with a number of boolean variables. The proof method relies on implementing the LTL formula, i.e., restricting the specification in such a way that only those runs remain that satisfy the formula. This result is a variation of the classical construction of a Büchi automatonfor a given LTL formula that accepts precisely those runs that satisfy the formula.

Grotzsch proved that every triangle-free planar graph is 3-colorable. Thomassen proved that every planar graph of girth at least five is 3-choosable. As for other surfaces, Thomassen proved that there are only finitely many 4-critical graphs of girth at least five embeddable in any fixed surface. This implies a linear-time algorithm for deciding 3-colorablity for graphs of girth at least five on any fixed surface. Dvořak, Kral' and Thomas strengthened Thomassen's result by proving that the number of vertices in a 4-critical graph of girth at least five is linear in its genus. They used this result to prove Havel's conjecture that a planar graph whose triangles are pairwise far enough apart is 3-colorable. As for list-coloring, Dvořak proved that a planar graph whose cycles of size at most four are pairwise far enough part is 3-choosable. In this article, we generalize these results. First we prove a linear isoperimetric bound for 3-list-coloring graphs of girth at least five. Many new results then follow from the theory of hyperbolic families of graphs developed by Postle and Thomas. In particular, it follows that there are only finitely many 4-list-critical graphs of girth at least five on any fixed surface, and that in fact the number of vertices of a 4-list-critical graph is linear in its genus. This provides independent proofs of the above results while generalizing Dvořak's result to graphs on surfaces that have large edge-width and yields a similar result showing that a graph of girth at least five with crossings pairwise far apart is 3-choosable. Finally, we generalize to surfaces Thomassen's result that every planar graph of girth at least five has exponentially many distinct 3-list-colorings. Specifically, we show that every graph of girth at least five that has a 3-list-coloring has 2 Ω ( n ) − O ( g ) distinct 3-list-colorings.

Symbolic model checkers can construct proofs of properties over highly complex models. However, the results reported by the tool when a proof succeeds do not generally provide much insight to the user. It is often useful for users to have traceability information related to the proof: which portions of the model were necessary to construct it. This traceability information can be used to diagnose a variety of modeling problems such as overconstrained axioms and underconstrained properties, measure completeness of a set of requirements over a model, and assist with design optimization given a set of requirements for an existing or synthesized implementation. In this paper, we present a comprehensive treatment of a suite of algorithms to compute inductive validity cores (IVCs), minimal sets of model elements necessary to construct inductive proofs of safety properties for sequential systems. The algorithms are based on the UNSAT core support built into current SMT solvers and novel encodings of the inductive problem to generate approximate and guaranteed minimal inductive validity cores as well as all inductive validity cores. We demonstrate that our algorithms are correct, describe their implementation in the JKind model checker for Lustre models, and present several use cases for the algorithms. We then present a substantial experiment in which we benchmark the efficiency and efficacy of the algorithms.

In this paper we consider Levin's notion of mutual information in infinite 0-1-sequences, as defined in [Leonid Levin. Laws of Information Conservation (Nongrowth) and Aspects of the Foundation of Probability Theory. Problems of information transmission, vol. 10 (1974), pp. 206--211]. The respective information conservation inequalities were stated in that paper without proofs. Later some proofs appeared in the literature, however no proof of the probabilistic conservation inequality has been published yet. In this paper we prove that inequality and for the sake of completeness we present also short proofs of other properties of the said notion.

Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without having to unroll their loops, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks., Comment: Extended version of FM'19 conference paper (https://doi.org/10.1007/978-3-030-30942-8_10), to appear in FMSD

Differential privacy is a mathematical framework for developing statistical computations with provable guarantees of privacy and accuracy. In contrast to the privacy component of differential privacy, which has a clear mathematical and intuitive meaning, the accuracy component of differential privacy does not have a generally accepted definition; accuracy claims of differential privacy algorithms vary from algorithm to algorithm and are not instantiations of a general definition. We identify program discontinuity as a common theme in existing ad hoc definitions and introduce an alternative notion of accuracy parametrized by, what we call, — the of an input x w.r.t. a deterministic computation f and a distance d , is the minimal distance d ( x , y ) over all y such that f ( y )≠ f ( x ). We show that our notion of accuracy subsumes the definition used in theoretical computer science, and captures known accuracy claims for differential privacy algorithms. In fact, our general notion of accuracy helps us prove better claims in some cases. Next, we study the decidability of accuracy. We first show that accuracy is in general undecidable. Then, we define a non-trivial class of probabilistic computations for which accuracy is decidable (unconditionally, or assuming Schanuel’s conjecture). We implement our decision procedure and experimentally evaluate the effectiveness of our approach for generating proofs or counterexamples of accuracy for common algorithms from the literature.

We give upper and lower bounds on the power of subsystems of the Ideal Proof System (IPS), the algebraic proof system recently proposed by Grochow and Pitassi [26], where the circuits comprising the proof come from various restricted algebraic circuit classes. This mimics an established research direction in the boolean setting for subsystems of Extended Frege proofs whose lines are circuits from restricted boolean circuit classes. Essentially all of the subsystems considered in this paper can simulate the well-studied Nullstellensatz proof system, and prior to this work there were no known lower bounds when measuring proof size by the algebraic complexity of the polynomials (except with respect to degree, or to sparsity). Our main contributions are two general methods of converting certain algebraic lower bounds into proof complexity ones. Both require stronger arithmetic lower bounds than common, which should hold not for a specific polynomial but for a whole family defined by it. These may be likened to some of the methods by which Boolean circuit lower bounds are turned into related proof-complexity ones, especially the "feasible interpolation" technique. We establish algebraic lower bounds of these forms for several explicit polynomials, against a variety of classes, and infer the relevant proof complexity bounds. These yield separations between IPS subsystems, which we complement by simulations to create a partial structure theory for IPS systems. Our first method is a functional lower bound, a notion of Grigoriev and Razborov [25], which is a function [EQUATION] {0, 1}n → F such that any polynomial f agreeing with [EQUATION] on the boolean cube requires large algebraic circuit complexity. We develop functional lower bounds for a variety of circuit classes (sparse polynomials, depth-3 powering formulas, read-once algebraic branching programs and multilinear formulas) where [EQUATION] equals [EQUATION] for a constant-degree polynomial p depending on the relevant circuit class. We believe these lower bounds are of independent interest in algebraic complexity, and show that they also imply lower bounds for the size of the corresponding IPS refutations for proving that the relevant polynomial p is non-zero over the boolean cube. In particular, we show super-polynomial lower bounds for refuting variants of the subset-sum axioms in these IPS subsystems. Our second method is to give lower bounds for multiples, that is, to give explicit polynomials whose all (non-zero) multiples require large algebraic circuit complexity. By extending known techniques, we give lower bounds for multiples for various restricted circuit classes such sparse polynomials, sums of powers of low-degree polynomials, and roABPs. These results are of independent interest, as we argue that lower bounds for multiples is the correct notion for instantiating the algebraic hardness versus randomness paradigm of Kabanets and Impagliazzo [31]. Further, we show how such lower bounds for multiples extend to lower bounds for refutations in the corresponding IPS subsystem.

Interactive consistency is the problem in which n distinct nodes, each having its own private value, where up to t may be Byzantine, run an algorithm that allows all non-faulty nodes to infer the values of each other node. This problem is relevant to critical applications that rely on the combination of the opinions of multiple peers to provide a service. Examples include monitoring a content source to prevent equivocation or to track variability in the content provided, and resolving divergent state amongst the nodes of a distributed system. Previous works assume a fully synchronous system, where one can make strong assumptions such as negligible message delivery delays and/or detection of absent messages. However, practical, real-world systems are mostly asynchronous, i.e., they exhibit only some periods of synchrony during which message delivery is timely, thus requiring a different approach. In this paper, we present a thorough study of practical interactive consistency. We leverage the vast prior work on broadcast and Byzantine consensus algorithms to design, implement and evaluate a set of randomized algorithms, with only a single synchronization barrier and varying message complexities, that can be used to achieve interactive consistency in real-world distributed systems. We present formal proofs of correctness and message complexity of our proposed algorithms. We provide a complete, open-source implementation of each proposed interactive consistency algorithm by building a multi-layered software stack of algorithms that includes several broadcast algorithms, as well as a binary and a multi-valued consensus algorithm. Most of these algorithms have never been implemented and evaluated in a real system before. Finally, we analyze the performance of our suite of algorithms experimentally by testing both single instance and multiple parallel instances of each alternative and present a case study of achieving interactive consistency in a real-world distributed e-voting system.

For some classes of analytic functions f, g, h and k in the open unit disk U, we consider the general integral operator Tn, that was introduced in a recent work [1] and we obtain new conditions of univalence for this integral operator. The key tools in the proofs of our results are the Pascu’s and the Pescar’s univalence criteria, as well as the Mocanu’s and erb’s Lemma. Some corollaries of the main results are also considered. Relevant connections of the results presented here with various other known results are briefly indicated.

The area of property testing is concerned with designing methods to decide whether an input object possesses a certain property or not. Usually the problem is described as a promise problem: either the input object has the property or the input object is far from possessing the property. Here, the meaning of object being far from possessing the property is based on a specified and meaningful notion of distance. The main objective of property testing is accomplishing this decision making by developing a super efficient tester. A tester that reads through the entire object can easily determine whether the property is satisfied or not. However, one wishes the tester to probe the input at very few random locations and determine whether the property is satisfied. As such, randomness is a necessary ingredient for testing and having the tester erring on few instances is a necessary price to pay for designing highly efficient methodologies. Much of the literature on property testing has focused on two types of objects: functions and graphs. Naturally they form the major portion of the book: functions are discussed from Chapters 2 to 6 and graph properties are discussed from Chapters 8 to 10. The final three chapters focus on distribution testing, probabilistically checkable proofs (PCPs) and locally testable codes, and ramifications of property testing on other related topics in Computer Science and Statistics. A separate chapter is devoted to query lower bound techniques.

To enhance the user’s privacy in electronic ID, anonymous credential systems have been researched. In the anonymous credential system, a trusted issuing organization first issues a certificate certifying the user’s attributes to a user. Then, in addition to the possession of the certificate, the user can anonymously prove only the necessary attributes. Previously, an anonymous credential system was proposed, where CNF (Conjunctive Normal Form) formulas on attributes can be proved. The advantage is that the attribute proof in the authentication has the constant size for the number of attributes that the user owns and the size of the proved formula. Thus, various expressive logical relations on attributes can be efficiently verified. However, the previous system has a limitation: the proved CNF formulas cannot include any negation. Therefore, in this paper, we propose an anonymous credential system with constant-size attribute proofs such that the user can prove CNF formulas with negations. For the proposed system, we extend the previous accumulator for the limited CNF formulas to verify CNF formulas with negations.

The fact that equalizers in the context of strongly Hausdorff locales (similarly like those in classical spaces) are closed is a special case of a standard categorical fact connecting diagonals with general equalizers. In this paper we analyze this and related phenomena in the category of locales. Here the mechanism of pullbacks connecting equalizers is based on natural preimages that preserve a number of properties (closedness, openness, fittedness, complementedness, etc.). Also, we have a new simple and transparent formula for equalizers in this category providing very easy proofs for some facts (including the general behavior of diagonals). In particular we discuss some aspects of the closed case (strong Hausdorff property), and the open and clopen one.

Automated verification for program safety is reduced to the discovery safe inductive invariants, i.e., formulas that over-approximate the sets of reachable program states, but precise enough to prove unreachability of the error state. We present a framework, called FreqHorn, that follows the Syntax-Guided Synthesis paradigm to iteratively sample candidate invariants from a formal grammar and check them with an SMT solver. FreqHorn automatically constructs grammars based on either source code or bounded proofs. After each (un-)successful candidate, FreqHorn adjusts the grammars to ensure the candidate is not sampled again. The process continues either until the conjunction of successful candidates (called lemmas) is sufficient, or the search space is exhausted. Additionally, FreqHorn keeps a history of counterexamples-to-induction (CTI) which block learning a lemma. With some periodicity, it checks if there is a CTI which is invalidated by the currently learned lemmas and rechecks the failed lemma if needed. FreqHorn is able to check several candidates at the same time to filter them effectively using the well known Houdini algorithm.

There is growing interest in termination reasoning for non-linear programs and, meanwhile, recent dynamic strategies have shown they are able to infer invariants for such challenging programs. These advances led us to hypothesize that perhaps such dynamic strategies for non-linear invariants could be adapted to learn recurrent sets (for non-termination) and/or ranking functions (for termination). In this paper, we exploit dynamic analysis and draw termination and non-termination as well as static and dynamic strategies closer together in order to tackle non-linear programs. For termination, our algorithm infers ranking functions from concrete transitive closures, and, for non-termination, the algorithm iteratively collects executions and dynamically learns conditions to refine recurrent sets. Finally, we describe an integrated algorithm that allows these algorithms to mutually inform each other, taking counterexamples from a failed validation in one endeavor and crossing both the static/dynamic and termination/non-termination lines, to create new execution samples for the other one., Comment: To appear at OOPSLA 2020

Following Newman (2010), we initiate a study of testing properties of graphs that are presented as subgraphs of a fixed (or an explicitly given) graph. The tester is given free access to a base graph G = ([ n ], E ) and oracle access to a function f : E → {0, 1} that represents a subgraph of G . The tester is required to distinguish between subgraphs that possess a predetermined property and subgraphs that are far from possessing this property. We focus on bounded-degree base graphs and on the relation between testing graph properties in the subgraph model and testing the same properties in the bounded-degree graph model. We identify cases in which testing is significantly easier in one model than in the other as well as cases in which testing has approximately the same complexity in both models. Our proofs are based on the design and analysis of efficient testers and on the establishment of query-complexity lower bounds.

The verification of the Cloud composite services’ correctness is challenging. In fact, multiple component services, derived from different Cloud providers with different service description languages and communication protocols, are involved in the composition which may raise incompatibility issues that in turn lead to a non-consistent composition. In this work, we propose a formal approach to model and verify Cloud composite services. Four verification levels are considered in this article; the structural, semantic, behavioral, and resource allocation levels. Therefore, we opted for the Event-B formal method that enables complex problems decomposition thanks to its refinement capabilities. The proposed approach has proven its efficiency for the modelling and verification of Cloud composite services. The proposed model comprises four abstract levels with respect to the four verification axes. A proof-based approach is applied to the model’s verification. We also succeeded in the validation of the model thanks to the model animation provided by the PROB tool. The use of formal methods provides a rigorous reasoning and mathematical proofs on the correction of the model which ensures the elaboration of correct-by-construction composite services.

Camera pose estimation is key to the proper functioning of robotic systems, supporting critical tasks such as robot navigation, target tracking, camera calibration, etc.Whilemultiple algorithms solving this problem have been proposed, their correctness has rarely been validated using formal techniques. This is true despite the fact that the adoption of formal verification is essential for the reliability of safety-critical systems, and for their certification to high assurance levels. In this article, we present an effort in formally verifying an algorithm for camera pose estimation in an interactive theorem prover. The algorithm leverages the power of Rodrigues formula to solve the pose estimation problem under conditions for which existing solutions cannot be applied. The technical ingredients include (but are not limited to) mechanized proofs of the Rodrigues formula (along with its Cayley decomposition form) and the least squares method for fitting data. Based on the formalization of the algorithm, we formally derive and verify its general solution and unique solution.

Group role assignment &#x0028 GRA &#x0029 is originally a complex problem in role-based collaboration &#x0028 RBC &#x0029 . The solution to GRA provides modelling techniques for more complex problems. GRA with constraints &#x0028 GRA &#x002B &#x0029 is categorized as a class of complex assignment problems. At present, there are few generally efficient solutions to this category of problems. Each special problem case requires a specific solution. Group multi-role assignment &#x0028 GMRA &#x0029 and GRA with conflicting agents on roles &#x0028 GRACAR &#x0029 are two problem cases in GRA &#x002B . The contributions of this paper include: 1 &#x0029 The formalization of a new problem of GRA &#x002B , called group multi-role assignment with conflicting roles and agents &#x0028 GMAC &#x0029 , which is an extension to the combination of GMRA and GRACAR; 2 &#x0029 A practical solution based on an optimization platform; 3 &#x0029 A sufficient condition, used in planning, for solving GMAC problems; and 4 &#x0029 A clear presentation of the benefits in avoiding conflicts when dealing with GMAC. The proposed methods are verified by experiments, simulations, proofs and analysis.

As all computational programs, derivation sequences of functional dependences are twice partially ordered sets: by following the instructions in the program and by their execution in time. Order consistency is achieved by the theoretical multiple embedding of one into another. Hereinafter, such sets are referred to as cascade ordered, and there is no need to resort to the terminology of the relational database theory for them. It is possible to represent the derivation sequence in the form of a special union of almost disjoint simple subsequences referred to as pointed sets here. It is achieved by applying a gluing operation $$\ae $$ to them. The process of forming a cascade-ordered set of pointed sets is reflected in the title by the term Synthesis. This paper is aimed at studying this process. The final section of the paper sets forth the principles of Analysis, i.e., decomposition of a specified cascade-ordered set into so-called AR cones. This issue will be completely resolved in subsequent papers. Here, logic schemes that are designed to calculate predicates from the given ones are applied for proofs. Flowcharts that are common to algorithmization are less frequently used. Their combined application serves the purposes of automating mathematical proofs. The logical toolkit of the paper is a prerequisite for constructing a mathematical model of artificial intelligence.