Formal methods used to validate software designs, like Alloy, OCL, and B, are powerful tools to analyze complex structures (e.g., architectures, object-relational mappings) captured as sets of relational constraints. ...
Formal methods used to validate software designs, like Alloy, OCL, and B, are powerful tools to analyze complex structures (e.g., architectures, object-relational mappings) captured as sets of relational constraints. However, their applicability is limited when software is subject to uncertainty (derived, e.g., from lack of control over third-party components, interaction with physical elements). In contrast, quantitative verification has emerged as a powerful way of providing quantitative guarantees about the performance, cost, and reliability of systems operating under uncertainty. However, quantitative verification methods do not retain thefl exibility of relational modeling in describing structures, forcing engineers to trade structural exploration for analytic capabilities that concern probabilistic and other quantitative guarantees. this paper contributes a method (HaiQ) that enhances structural modeling/synthesis with quantitative guarantees in the style provided by quantitative verification. It includes a language for describing structure and (stochastic) behavior of systems, and a temporal logic that allows checking probability and reward-based properties over sets of feasible design alternatives implicitly described by the relational constraints in a HaiQ model. We report the results of applying a prototype tool in two domains, on which we show the feasibility of synthesizing structural designs that optimize probabilistic and other quantitative guarantees. CCS Concepts • software and its engineering → Formal software verification; software design tradeoffs • theory of computation → Verification by model checking.
Commuting conversions of Linear Logic induce a notion of dependency between rules inside a proof derivation: a rule depends on a previous rule when they cannot be permuted using the conversions. We propose a new inter...
详细信息
ISBN:
(纸本)9783030171278;9783030171261
Commuting conversions of Linear Logic induce a notion of dependency between rules inside a proof derivation: a rule depends on a previous rule when they cannot be permuted using the conversions. We propose a new interpretation of proofs of Linear Logic as causal invariants which captures exactly this dependency. We represent causal invariants using game semantics based on general event structures, carving out, inside the model of [6], a submodel of causal invariants. this submodel supports an interpretation of unit-free Multiplicative Additive Linear Logic with MIX (MALL(-)) which is (1) fully complete: every element of the model is the denotation of a proof and (2) injective: equality in the model characterises exactly commuting conversions of MALL(-). this improves over the standard fully complete game semantics model of MALL(-).
Event structures are fundamental models in concurrency theory, providing a representation of events in computation and of their relations, notably concurrency, conflict and causality. In this paper we present a theory...
详细信息
By developing a hierarchical modeling method, using discrete element analysis software PFC3D, a pile foundation model is built. According to the idea of finite element method, using smaller particles for concerned par...
详细信息
foundations of softwarescience and computationstructures : Second internationalconference, Fossacs '99 Held as Part of the Joint European conferences on theory and Practice of software, Etaps '99, Amsterdam...
详细信息
foundations of softwarescience and computationstructures : Second internationalconference, Fossacs '99 Held as Part of the Joint European conferences on theory and Practice of software, Etaps '99, Amsterdam, the Netherlands, March 22-28, 1999 : Proceedings by Fossacs '99 (1999 : Amsterdam, Netherlands); thomas, Wolfgang, 1947-; international Joint conference on theory; Practice of software Development (9th : 1999 : Amsterdam, Netherlands); published by Berlin ; New York : Springer
the proceedings contain 38 papers. the special focus in this conference is on Semantics of Programming Languages, Categorical Models, Temporal Logics and Timed Systems. the topics include: Synthesis of strategies and ...
ISBN:
(纸本)9783662466773
the proceedings contain 38 papers. the special focus in this conference is on Semantics of Programming Languages, Categorical Models, Temporal Logics and Timed Systems. the topics include: Synthesis of strategies and the Hoare logic of angelic nondeterminism;game semantics and normalization by evaluation;a categorical semantics for linear logical frameworks;coalgebraic trace semantics via forgetful logics;on the total variation distance of semi-Markov chains;decidable and expressive classes of probabilistic automata;compositional metric reasoning with probabilistic process calculi;fragments of ml decidable by nested data class memory automata;step-indexed logical relations for probability;robust multidimensional mean-payoff games are undecidable;three variables suffice for real-time logic;on presburger arithmetic extended with modulo counting quantifiers;programming and reasoning with guarded recursion for coinductive types;the computational contents of ramified corecurrence and on the mints hierarchy in first-order intuitionistic logic.
the proceedings contain 29 papers. the topics discussed include: analysis of probabilistic basic parallel processes;type reconstruction for the linear π-calculus with composite and equi-recursive types;a semantical a...
ISBN:
(纸本)9783642548291
the proceedings contain 29 papers. the topics discussed include: analysis of probabilistic basic parallel processes;type reconstruction for the linear π-calculus with composite and equi-recursive types;a semantical and operational account of call-by-value solvability;network-formation games with regular objectives;playing with probabilities in reconfigurable broadcast networks;unsafe order-2 tree languages are context-sensitive;complexity of model-checking call-by-value programs;resource reachability games on pushdown graphs;the complexity of partial-observation stochastic parity games with finite-memory strategies;on negotiation as concurrency primitive II: deterministic cyclic negotiations;on asymmetric unification and the combination problem in disjoint theories;axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules;generalized Eilenberg theorem I: local varieties of languages;and combining bialgebraic semantics and equations.
Private set intersection (PSI) refers to a special case of secure two-party computation in which the parties each have a set of items and compute the intersection of these sets without revealing any additional informa...
详细信息
ISBN:
(纸本)9783319566207;9783319566191
Private set intersection (PSI) refers to a special case of secure two-party computation in which the parties each have a set of items and compute the intersection of these sets without revealing any additional information. In this paper we present improvements to practical PSI providing security in the presence of malicious adversaries. Our starting point is the protocol of Dong, Chen & Wen (CCS 2013) that is based on Bloom filters. We identify a bug in their malicious-secure variant and show how to fix it using a cut-and-choose approach that has low overhead while simultaneously avoiding one the main computational bottleneck in their original protocol. We also point out some subtleties that arise when using Bloom filters in malicious-secure cryptographic protocols. We have implemented our PSI protocols and report on its performance. Our improvements reduce the cost of Dong et al.'s protocol by a factor of 14 - 110x on a single thread. When compared to the previous fastest protocol of De Cristofaro et al., we improve the running time by 8 - 24x. For instance, our protocol has an online time of 14 s and an overall time of 2.1 min to securely compute the intersection of two sets of 1 million items each.
We present a theory for slicing probabilistic imperative programs-containing random assignment and "observe" statements-represented as control flow graphs whose nodes transform probability distributions. We ...
详细信息
ISBN:
(纸本)9783662496305;9783662496299
We present a theory for slicing probabilistic imperative programs-containing random assignment and "observe" statements-represented as control flow graphs whose nodes transform probability distributions. We show that such a representation allows direct adaptation of standard machinery such as data and control dependence, postdominators, relevant variables, etc. to the probabilistic setting. We separate the specification of slicing from its implementation: first we develop syntactic conditions that a slice must satisfy;next we prove that any such slice is semantically correct;finally we give an algorithm to compute the least slice. A key feature of our syntactic conditions is that they involve two disjoint slices such that the variables of one slice are probabilistically independent of the variables of the other. this leads directly to a proof of correctness of probabilistic slicing.
暂无评论