Wednesday, October 14, 2015



Soy un nuevo usuario

Olvidé mi contraseña

Entrada usuarios

Lógica Matemáticas Astronomía y Astrofísica Física Química Ciencias de la Vida
Ciencias de la Tierra y Espacio Ciencias Agrarias Ciencias Médicas Ciencias Tecnológicas Antropología Demografía
Ciencias Económicas Geografía Historia Ciencias Jurídicas y Derecho Lingüística Pedagogía
Ciencia Política Psicología Artes y Letras Sociología Ética Filosofía

rss_1.0 Clasificación por Disciplina

Nomenclatura Unesco > (11) Lógica

Mostrando recursos 61 - 80 de 150,310

61. Using Constraint Logic Programming for the Symbolic Animation of Formal Models - Bouquet, Fabrice; Dadeau, Frédéric; Legeard, Bruno
International audience

62. Automatic Composition of Services with Security Policies - Chevalier, Yannick; Mekki, Mohammed Anis; Rusinowitch, Michael
International audience

63. Active Intruders with Caps - Anatharaman, Siva; Lin, Hai; Lynch, Chris; Narendran, Paliath; Rusinowitch, Michael
International audience

64. Combination of Convex Theories: Modularity, Deduction Completeness, and Explanation - Tran, Duc-Khanh; Ringeissen, Christophe; Ranise, Silvio; Kirchner, Hélène
Decision procedures are key components of theorem provers and constraint satisfaction systems. Their modular combination is of prime interest for building efficient systems, but their effective use is often limited by poor interface capabilities, when such procedures only provide a simple ``sat/unsat'' answer. In this paper, we develop a rule-based framework to design cooperation schemas between such procedures while maintaining modularity of their interfaces. First, we use the rule-based framework to specify and prove the correctness of classic combination schemas by Nelson-Oppen and Shostak. Second, we introduce the concept of deduction complete satisfiability procedures, we show how to build them...

65. Towards a Constrained-based Verification of Parameterized Cryptographic Protocols - Chridi, Najah; Turuani, Mathieu; Rusinowitch, Michael
International audience

66. Inductive Proof Search Modulo - Nahon, Fabrice; Kirchner, Claude; Kirchner, Hélène; Brauner, Paul
International audience

67. Automatic Methods for Analyzing Non-repudiation Protocole with an Active Intruder - Klay, Francis; Vigneron, Laurent
International audience

68. Satisfiability Procedures for Combination of Theories Sharing Integer Offsets - Nicolini, Enrica; Ringeissen, Christophe; Rusinowitch, Michael
We present a novel technique to combine satisfiability procedures for theories that model some data-structures and that share the integer offsets. This procedure extends the Nelson-Oppen approach to a family of non-disjoint theories that have practical interest in verification. The result is derived by showing that the considered theories satisfy the hypotheses of a general result on non-disjoint combination. In particular, the capability of computing logical consequences over the shared signature is ensured in a non trivial way by devising a suitable complete superposition calculus.

69. Combinable Extensions of Abelian Groups - Nicolini, Enrica; Ringeissen, Christophe; Rusinowitch, Michael
The design of decision procedures for combinations of theories sharing some arithmetic fragment is a challenging problem in verification. One possible solution is to apply a combination method à la Nelson-Oppen, like the one developed by Ghilardi for unions of non-disjoint theories. We show how to apply this non-disjoint combination method with the theory of abelian groups as shared theory. We consider the completeness and the effectiveness of this non-disjoint combination method. For the completeness, we show that the theory of abelian groups can be embedded into a theory admitting quantifier elimination. For achieving effectiveness, we rely on a superposition...

70. Modular Security Policy Design based on Extended Petri Nets - Huang, Hejiao; Kirchner, Helene
Security policies are one of the most fundamental elements of computer security. Their design has to cope with composition of components in security systems and interactions between them. Consequently, a modular approach for specification and verification of security policies is necessary and the composition of modules must consistently ensure fundamental properties of security policies, in a rigorous and systematic way. This paper shows how to use extended Petri net process (EPNP) to specify and verify security policies in a modular way. It defines a few fundamental policy properties, namely completeness, termination, consistency and confluence, in Petri net terminology and relates...

71. Secure Interoperation in Heterogeneous Systems based on Colored Petri Nets - Huang, Hejiao; Kirchner, Helene
In a multi-domains application environment, where distributed multiple organizations interoperate with each other, the local access control policies should correspondingly be integrated in order to allow users of one organization to interact with other domains. One of the key challenges of integrating policies is conflict detection and resolution while preserving policy consistency. This paper addresses several types of potential conflicts and consistency properties with a systematic and rigorous approach. In the approach, graph theory, network flow technology and colored Petri nets are applied for specifying and verifying a secure interoperation design. The component-based integration of policies is applicable for both...

72. Data Structures with Arithmetic Constraints: a Non-Disjoint Combination - Nicolini, Enrica; Ringeissen, Christophe; Rusinowitch, Michael
We apply an extension of the Nelson-Oppen combination method to develop a decision procedure for the non-disjoint union of theories modeling data structures with a counting operator and fragments of arithmetic. We present some data structures and some fragments of arithmetic for which the combination method is complete and effective. To achieve effectiveness, the combination method relies on particular procedures to compute sets that are representative of all the consequences over the shared theory. We show how to compute these sets by using a superposition calculus for the theories of the considered data structures and various solving and reduction techniques...

73. On the relation between sized-types based termination and semantic labelling - Blanqui, Frédéric; Roux, Cody
Full version

74. Automating Theories in Intuitionistic Logic - Burel, Guillaume
International audience

75. A Port Graph Calculus for Autonomic Computing and Invariant Verification - Andrei, Oana; Kirchner, Helene
International audience

76. Quantitative Notions of Leakage for One-try Attacks - Braun, Christelle; Chatzikokolakis, Konstantinos; Palamidessi, Catuscia
International audience

77. Epistemic Strategies and Games on Concurrent Processes - Chatzikokolakis, Konstantinos; Knight, Sophia; Panangaden, Prakash
International audience

78. Probabilistic and nondeterministic aspects of anonymity - Beauxis, Romain; Palamidessi, Catuscia
International audience

79. Model checking probabilistic and stochastic extensions of the $\pi$-calculus - Norman, Gethin; Palamidessi, Catuscia; Parker, David; Wu, Peng
International audience

80. Design and Verification of a Non-repudiation Protocol Based on Receiver-Side Smart Card - Jing, Liu; Vigneron, Laurent
International audience

Página de resultados:

Busque un recurso