- -

Datalog-Based program analysis with BES and RWL

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Datalog-Based program analysis with BES and RWL

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: Alpuente-Feliu-Jo ...
Tamaño: 313.8Kb
Formato: PDF
Descripción: Versión del Autor.
Abrir
[Cerrado]
Nombre: Datalog-Based Program ...
Tamaño: 329.9Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor
dc.contributor.author Alpuente Frasnedo, María es_ES
dc.contributor.author Feliú Gabaldón, Marco Antonio es_ES
dc.contributor.author Joubert, Christophe es_ES
dc.contributor.author Villanueva García, Alicia es_ES
dc.date.accessioned 2014-05-21T10:44:25Z
dc.date.issued 2011
dc.identifier.isbn 978-3-642-24205-2
dc.identifier.issn 0302-9743
dc.identifier.uri http://hdl.handle.net/10251/37650
dc.description.abstract This paper describes two techniques for Datalog query evaluation and their application to object-oriented program analysis. The first technique transforms Datalog programs into an implicit Boolean Equation System (Bes) that can then be solved by using linear-time complexity algorithms that are available in existing, general purpose verification toolboxes such as Cadp. In order to improve scalability and to enable analyses involving advanced meta-programming features, we develop a second methodology that transforms Datalog programs into rewriting logic (Rwl) theories. This method takes advantage of the preeminent features and facilities that are available within the high-performance system Maude, which provides a very efficient implementation of Rwl. We provide evidence of the practicality of both approaches by reporting on some experiments with a number of real-world Datalog-based analyses. © 2011 Springer-Verlag. es_ES
dc.description.sponsorship This work has been partially supported by the eu(feder), the Spanish mec/micinn under grants tin2007-68093-C02 and tin2010-21062-C02-02, and the Generalitat Valenciana under grant Emergentes gv/2009/024. M.A.Feliu was partially supported by the Spanish mec fpu grant AP2008-00608. es_ES
dc.format.extent 20 es_ES
dc.language Inglés es_ES
dc.publisher Springer Verlag (Germany) es_ES
dc.relation.ispartof Datalog Reloaded es_ES
dc.relation.ispartofseries Lecture Notes in Computer Science;6702
dc.rights Reserva de todos los derechos es_ES
dc.subject Boolean equation system es_ES
dc.subject Model checking es_ES
dc.subject Query evaluation es_ES
dc.subject Rewriting logic es_ES
dc.subject.classification CIENCIAS DE LA COMPUTACION E INTELIGENCIA ARTIFICIAL es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Datalog-Based program analysis with BES and RWL es_ES
dc.type Capítulo de libro es_ES
dc.embargo.lift 10000-01-01
dc.embargo.terms forever es_ES
dc.identifier.doi 10.1007/978-3-642-24206-9_1
dc.relation.projectID info:eu-repo/grantAgreement/MEC//TIN2007-68093-C02-02/ES/TECHNOLOGICS-UPV/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/MICINN//TIN2010-21062-C02-02/ES/SWEETLOGICS-UPV/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//GV%2F2009%2F024/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/MECD//AP2008-00608/ES/AP2008-00608/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Alpuente Frasnedo, M.; Feliú Gabaldón, MA.; Joubert, C.; Villanueva García, A. (2011). Datalog-Based program analysis with BES and RWL. En Datalog Reloaded. Springer Verlag (Germany). 6702:1-20. https://doi.org/10.1007/978-3-642-24206-9_1 es_ES
dc.description.accrualMethod S es_ES
dc.relation.conferencename First International Workshop, Datalog 2010 es_ES
dc.relation.conferencedate March 16-19, 2010 es_ES
dc.relation.conferenceplace Oxford, UK es_ES
dc.relation.publisherversion http://link.springer.com/chapter/10.1007/978-3-642-24206-9_1 es_ES
dc.description.upvformatpinicio 1 es_ES
dc.description.upvformatpfin 20 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 6702 es_ES
dc.relation.senia 210345
dc.contributor.funder Ministerio de Ciencia e Innovación es_ES
dc.contributor.funder European Regional Development Fund es_ES
dc.contributor.funder Generalitat Valenciana es_ES
dc.contributor.funder Ministerio de Educación y Ciencia es_ES
dc.contributor.funder Ministerio de Educación, Cultura y Deporte es_ES
dc.description.references Afrati, F.N., Ullman, J.D.: Optimizing joins in a map-reduce environment. In: Manolescu, I., Spaccapietra, S., Teubner, J., Kitsuregawa, M., Léger, A., Naumann, F., Ailamaki, A., Özcan, F. (eds.) EDBT. ACM International Conference Proceeding Series, vol. 426, pp. 99–110. ACM, New York (2010) es_ES
dc.description.references Alpuente, M., Feliú, M., Joubert, C., Villanueva, A.: Defining Datalog in Rewriting Logic. Technical Report DSIC-II/07/09, DSIC, Universidad Politécnica de Valencia (2009) es_ES
dc.description.references Alpuente, M., Feliú, M., Joubert, C., Villanueva, A.: Using Datalog and Boolean Equation Systems for Program Analysis. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 215–231. Springer, Heidelberg (2009) es_ES
dc.description.references Alpuente, M., Feliú, M.A., Joubert, C., Villanueva, A.: Defining datalog in rewriting logic. In: De Schreye, D. (ed.) LOPSTR 2009. LNCS, vol. 6037, pp. 188–204. Springer, Heidelberg (2010) es_ES
dc.description.references Andersen, H.R.: Model checking and boolean graphs. Theoretical Computer Science 126(1), 3–30 (1994) es_ES
dc.description.references Bancilhon, F., Maier, D., Sagiv, Y., Ullman, J.D.: Magic Sets and Other Strange Ways to Implement Logic Programs. In: Proc. 5th ACM SIGACT-SIGMOD Symp. on Principles of Database Systems, PODS 1986, pp. 1–15. ACM Press, New York (1986) es_ES
dc.description.references Ceri, S., Gottlob, G., Tanca, L.: Logic Programming and Databases. Springer, Heidelberg (1990) es_ES
dc.description.references Chen, T., Ploeger, B., van de Pol, J., Willemse, T.A.C.: Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 120–135. Springer, Heidelberg (2007) es_ES
dc.description.references Clavel, M., Durán, F., Ejer, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007) es_ES
dc.description.references Dam, A., Ploeger, B., Willemse, T.: Instantiation for Parameterised Boolean Equation Systems. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 440–454. Springer, Heidelberg (2008) es_ES
dc.description.references de Moor, O., Sereni, D., Verbaere, M., Hajiyev, E., Avgustinov, P., Ekman, T., Ongkingco, N., Tibble, J.: QL: Object-oriented queries made easy. In: Lämmel, R., Visser, J., Saraiva, J. (eds.) GTTSE 2008. LNCS, vol. 5235, pp. 78–133. Springer, Heidelberg (2008) es_ES
dc.description.references Feliú, M., Joubert, C., Tarín, F.: Efficient BES-based Bottom-Up Evaluation of Datalog Programs. In: Gulías, V., Silva, J., Villanueva, A. (eds.) Proc. X Jornadas sobre Programación y Lenguajes (PROLE 2010), Garceta, pp. 165–176 (2010) es_ES
dc.description.references Feliú, M., Joubert, C., Tarín, F.: Evaluation strategies for datalog-based points-to analysis. In: Bendisposto, J., Leuschel, M., Roggenbach, M. (eds.) Proc. 10th Workshop on Automated Verification of Critical Systems (AVoCS 2010), pp. 88–103. Technical Report of Düsseldorf University (2010) es_ES
dc.description.references Garavel, H., Mateescu, R., Lang, F., Serwe, W.: CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007) es_ES
dc.description.references Hajiyev, E., Verbaere, M., de Moor, O.: CodeQuest: Scalable Source Code Queries with Datalog. In: Hu, Q. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 2–27. Springer, Heidelberg (2006) es_ES
dc.description.references Hanus, M.: The Integration of Functions into Logic Programming: From Theory to Practice. Journal on Logic Programming 19 & 20, 583–628 (1994) es_ES
dc.description.references Joubert, C., Mateescu, R.: Distributed On-the-Fly Model Checking and Test Case Generation. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 126–145. Springer, Heidelberg (2006) es_ES
dc.description.references Leeuwen, J. (ed.): Formal Models and Semantics, vol. B. Elsevier, The MIT Press (1990) es_ES
dc.description.references Liu, X., Smolka, S.A.: Simple Linear-Time Algorithms for Minimal Fixed Points. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 53–66. Springer, Heidelberg (1998) es_ES
dc.description.references Liu, Y.A., Stoller, S.D.: From datalog rules to efficient programs with time and space guarantees. ACM Trans. Program. Lang. Syst. 31(6) (2009) es_ES
dc.description.references Livshits, B., Whaley, J., Lam, M.: Reflection Analysis for Java. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 139–160. Springer, Heidelberg (2005) es_ES
dc.description.references Marchiori, M.: Logic Programs as Term Rewriting Systems. In: Rodríguez-Artalejo, M., Levi, G. (eds.) ALP 1994. LNCS, vol. 850, pp. 223–241. Springer, Heidelberg (1994) es_ES
dc.description.references Mateescu, R.: Local Model-Checking of an Alternation-Free Value-Based Modal Mu-Calculus. In: Proc. 2nd Int’l Workshop on Verication, Model Checking and Abstract Interpretation, VMCAI 1998 (1998) es_ES
dc.description.references Mateescu, R., Thivolle, D.: A Model Checking Language for Concurrent Value-Passing Systems. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008) es_ES
dc.description.references Meseguer, J.: Conditional Rewriting Logic as a Unified Model of Concurrency. Theoretical Computer Science 96(1), 73–155 (1992) es_ES
dc.description.references Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998) es_ES
dc.description.references Reddy, U.: Transformation of Logic Programs into Functional Programs. In: Proc. Symposium on Logic Programming (SLP 1984), pp. 187–197. IEEE Computer Society Press, Los Alamitos (1984) es_ES
dc.description.references Reps, T.W.: Solving Demand Versions of Interprocedural Analysis Problems. In: Adsul, B. (ed.) CC 1994. LNCS, vol. 786, pp. 389–403. Springer, Heidelberg (1994) es_ES
dc.description.references Rosu, G., Havelund, K.: Rewriting-Based Techniques for Runtime Verification. Autom. Softw. Eng. 12(2), 151–197 (2005) es_ES
dc.description.references Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated Termination Analysis for Logic Programs by Term Rewriting. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 177–193. Springer, Heidelberg (2007) es_ES
dc.description.references Ullman, J.D.: Principles of Database and Knowledge-Base Systems, Volume I and II, The New Technologies. Computer Science Press, Rockville (1989) es_ES
dc.description.references Vieille, L.: Recursive Axioms in Deductive Databases: The Query/Subquery Approach. In: Proc. 1st Int’l Conf. on Expert Database Systems, EDS 1986, pp. 253–267 (1986) es_ES
dc.description.references Whaley, J.: Joeq: a Virtual Machine and Compiler Infrastructure. In: Proc. Workshop on Interpreters, Virtual Machines and Emulators, IVME 2003, pp. 58–66. ACM Press, New York (2003) es_ES
dc.description.references Whaley, J., Avots, D., Carbin, M., Lam, M.S.: Using Datalog with Binary Decision Diagrams for Program Analysis. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 97–118. Springer, Heidelberg (2005) es_ES
dc.description.references Zheng, X., Rugina, R.: Demand-driven alias analysis for C. In: Proc. 35th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2008, pp. 197–208. ACM Press, New York (2008) es_ES


Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem