Navegar

Colección

Datos Estadísticas

Artículo

Mera, S.; Bjørner, N. "DKAL and Z3: A logic embedding experiment" (2010) 35th International Symposium on Mathematical Foundations of Computer Science, MFCS 2010, and 19th EACSL Annual Conference on Computer Science Logic, CSL 2010. 6300 LNCS:504-528
El editor solo permite decargar el artículo en su versión post-print desde el repositorio. Por favor, si usted posee dicha versión, enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

Yuri Gurevich and Itay Neeman proposed the Distributed Knowledge Authorization Language, DKAL, as an expressive, yet very succinct logic for distributed authorization. DKAL uses a combination of modal and intuitionistic propositional logic. Modalities are used for qualifying assertions made by different principals and intuitionistic logic captures very elegantly assertions about basic information. Furthermore, a non-trivial and useful fragment known as the primal infon logic is amenable to efficient linear-time saturation. In this paper we experiment with an embedding of the full DKAL logic into the state-of-the-art Satisfiability Modulo Theories solver Z3 co-developed by the second author. Z3 supports classical first-order semantics of formulas, so it is not possible to directly embed DKAL into Z3. We therefore use an indirect encoding. The one experimented with in this paper uses the instantiation-based support for quantifiers in Z3. Z3 offers the feature to return a potential ground counter-model when the saturation procedure ends up with a satisfiable set of ground assertions. We develop an algorithm that extracts a DKAL model from the propositional model, in order to provide root causes for non-derivability. © 2010 Springer-Verlag Berlin Heidelberg.

Registro:

Documento: Artículo
Título:DKAL and Z3: A logic embedding experiment
Autor:Mera, S.; Bjørner, N.
Ciudad:Brno
Filiación:Computer Science Department, University of Buenos Aires, Ciudad Universitaria, Pabellón 1 (C1428EGA), Buenos Aires, Argentina
Microsoft Research, One Microsoft Way, Redmond, WA 98074, United States
Palabras clave:DKAL; Embedding; Model Extraction; Z3; Authorization languages; Distributed authorization; Distributed knowledge; DKAL; Embedding; First-order; Intuitionistic logic; Model Extraction; Non-trivial; Propositional logic; Root cause; Satisfiability modulo Theories; Z3; Computer science; Technical presentations; Formal logic
Año:2010
Volumen:6300 LNCS
Página de inicio:504
Página de fin:528
DOI: http://dx.doi.org/10.1007/978-3-642-15025-8_25
Título revista:35th International Symposium on Mathematical Foundations of Computer Science, MFCS 2010, and 19th EACSL Annual Conference on Computer Science Logic, CSL 2010
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v6300LNCS_n_p504_Mera

Referencias:

  • Ball, T., Rajamani, S.K., The SLAM project: Debugging system software via static analysis (2002) SIGPLAN Not., 37 (1), pp. 1-3
  • Barnett, M., Leino, K.R.M., Schulte, W., The spec# programming system: An overview (2005) LNCS, 3362, pp. 49-69. , Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. Springer, Heidelberg
  • Biere, A., Cimatti, A., Clarke, E., Zhu, Y., Symbolic model checking without BDDs (1999) LNCS, 1579, pp. 193-207. , Cleaveland, W.R. (ed.) TACAS 1999. Springer, Heidelberg
  • Bjørner, N., Hendrix, J., Linear functional fixed-points (2009) LNCS, 5643, pp. 124-139. , Bouajjani, A., Maler, O. (eds.) CAV 2009. Springer, Heidelberg
  • Cohen, E., Moskal, M., Schulte, W., Tobies, S., A precise yet efficient memory model for C (2009) Proceedings of Systems Software Verification Workshop (SSV 2009), , to appear
  • Costa, M., Crowcroft, J., Castro, M., Rowstron, A.I.T., Zhou, L., Zhang, L., Barham, P., Vigilante: End-to-end containment of internet worms (2005) SOSP, pp. 133-147. , Herbert, A., Birman, K.P. (eds.) ACM, New York
  • De Moura, L., Bjørner, N., Efficient E-matching for SMT solvers (2007) LNCS (LNAI), 4603, pp. 183-198. , Pfenning F. (ed.) CADE 2007. Springer, Heidelberg
  • De Moura, L., Bjørner, N., Z3: An efficient SMT solver (2008) LNCS, 4963, pp. 337-340. , Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. Springer, Heidelberg
  • Degtyarev, A., Gurevich, Y., Narendran, P., Veanes, M., Voronkov, A., Decidability and complexity of simultaneous rigid E-unification with one variable and related results (2000) Theoretical Computer Science, 243, pp. 167-184
  • Deline, R., Leino, K.R.M., BoogiePL: A typed procedural language for checking object-oriented programs (2005) Technical Report 2005-70, , Microsoft Research
  • Godefroid, P., Levin, M., Molnar, D., Automatedwhitebox fuzz testing (2007) Technical Report 2007-58, , Microsoft Research
  • Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K., Synergy: A new algorithm for property checking (2006) SIGSOFT FSE, pp. 117-127. , Young M., Devanbu, P.T. (eds.) . ACM, New York
  • Gurevich, Y., Neeman, I., Dkal: Distributed-knowledge authorization language (2008) CSF, pp. 149-162. , IEEE Computer Society, Los Alamitos
  • Gurevich, Y., Neeman, I., DKAL 2 - A simplified and improved authorization language (2009) Technical Report 2009-11, , Microsoft Research
  • Gurevich, Y., Neeman, I., The infon logic (2009) Bulletin of European Association for Theoretical Computer Science
  • Jackson, E.K., Schulte, W., Model generation for horn logic with stratified negation (2008) LNCS, 5048, pp. 1-20. , Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. Springer, Heidelberg
  • Lahiri, S.K., Qadeer, S., Back to the future: Revisiting precise program verification using SMT solvers (2008) POPL 2008
  • Mints, G., Grigori (2000) A Short Introduction to Intuitionistic Logic, , Kluwer Academic, New York
  • Moy, Y., Bjørner, N., Sielaff, D., Modular bug-finding for integer overflows in the large: Sound, efficient, bit-precise static analysis (2009) Technical Report MSR-TR-2009-2057, , Microsoft Research
  • Ohlbach, H.J., Nonnengart, A., De Rijke, M., Gabbay, D.M., Encoding two-valued nonclassical logics in classical logic (2001) Handbook of Automated Reasoning, pp. 1403-1486. , Robinson, J.A., Voronkov, A. (eds.) Elsevier, MIT Press
  • Tillmann, N., Schulte, W., Unit tests reloaded: Parameterized unit testing with symbolic execution (2006) IEEE Software, 23, pp. 38-47

Citas:

---------- APA ----------
Mera, S. & Bjørner, N. (2010) . DKAL and Z3: A logic embedding experiment. 35th International Symposium on Mathematical Foundations of Computer Science, MFCS 2010, and 19th EACSL Annual Conference on Computer Science Logic, CSL 2010, 6300 LNCS, 504-528.
http://dx.doi.org/10.1007/978-3-642-15025-8_25
---------- CHICAGO ----------
Mera, S., Bjørner, N. "DKAL and Z3: A logic embedding experiment" . 35th International Symposium on Mathematical Foundations of Computer Science, MFCS 2010, and 19th EACSL Annual Conference on Computer Science Logic, CSL 2010 6300 LNCS (2010) : 504-528.
http://dx.doi.org/10.1007/978-3-642-15025-8_25
---------- MLA ----------
Mera, S., Bjørner, N. "DKAL and Z3: A logic embedding experiment" . 35th International Symposium on Mathematical Foundations of Computer Science, MFCS 2010, and 19th EACSL Annual Conference on Computer Science Logic, CSL 2010, vol. 6300 LNCS, 2010, pp. 504-528.
http://dx.doi.org/10.1007/978-3-642-15025-8_25
---------- VANCOUVER ----------
Mera, S., Bjørner, N. DKAL and Z3: A logic embedding experiment. Lect. Notes Comput. Sci. 2010;6300 LNCS:504-528.
http://dx.doi.org/10.1007/978-3-642-15025-8_25