{rfName}
A

Indexat a

Llicència i ús

Icono OpenAccess

Citacions

3

Altmetrics

Anàlisi d'autories institucional

Escobar, SAutor o coautorRomero, DAutor o coautor

Compartir

Publicacions
>
Article

A Tool for Automated Certification of Java Source Code in Maude

Publicat a:Electronic Notes In Theoretical Computer Science. 248 19-29 - 2009-08-04 248(), DOI: 10.1016/j.entcs.2009.07.056

Autors: Alba-Castro, M; Alpuente, M; Escobar, S; Ojeda, P; Romero, D

Afiliacions

Univ Politecn Valencia, Dept Sistemas Informat & Computac - Autor o coautor

Resum

In previous work, an abstract certification technique for Java source code was proposed based on rewriting logic, which is a semantic framework that has been efficiently implemented in the rule-based programming language Maude. Starting from a specification of a (generic) Java abstract semantics written in Maude, we develop an abstract verification technique that essentially consists of a reachability analysis using the Java abstract semantics. We provide facilities to associate abstract domains to the variables of the considered Java program so that the resulting state-space is finite. As a by-product of the abstract verification, a safety certificate is delivered that contains a set of (abstract) rewriting proofs that can be checked by the code consumer using a standard rewriting logic engine. The main advantage is that the amount of code that must be explicitly trusted is very small. This paper presents a Web tool that implements the abstract certification technique by providing appropriate abstract domains for different safety properties while hiding the technical details of the method from the user. The tool has been devised to be easily extendable to other properties and domains. It currently supports the certification of two kinds of safety properties that are not handled by standard Java compilers: secure integer arithmetic rules and non-interference policies.

Paraules clau

Abstract domainsAbstract semanticsAbstractingAutomated certificationAutomationComputer programmingComputer softwareInteger arithmeticJava compilersJava programJava programming languageJava source codesMaudeNon interferenceReachability analysisRewriting logicRule-based programmingSafety propertySemantic frameworkSemanticsState-spaceTechnical detailsVerification techniquesWeb toolWeb toolsWireless telecommunication systems

Indicis de qualitat

Impacte bibliomètric. Anàlisi de la contribució i canal de difusió

El treball ha estat publicat a la revista Electronic Notes In Theoretical Computer Science a causa de la seva progressió i el bon impacte que ha aconseguit en els últims anys, segons l'agència Scopus (SJR), s'ha convertit en una referència en el seu camp. A l'any de publicació del treball, 2009, es trobava a la posició , aconseguint així situar-se com a revista Q2 (Segundo Cuartil), en la categoria Computer Science (Miscellaneous).

Independentment de l'impacte esperat determinat pel canal de difusió, és important destacar l'impacte real observat de la pròpia aportació.

Segons les diferents agències d'indexació, el nombre de citacions acumulades per aquesta publicació fins a la data 2025-06-26:

  • WoS: 2
  • Scopus: 1
  • OpenCitations: 1

Impacte i visibilitat social

Des de la dimensió d'influència o adopció social, i prenent com a base les mètriques associades a les mencions i interaccions proporcionades per agències especialitzades en el càlcul de les denominades "Mètriques Alternatives o Socials", podem destacar a data 2025-06-26:

  • L'ús d'aquesta aportació en marcadors, bifurcacions de codi, afegits a llistes de favorits per a una lectura recurrent, així com visualitzacions generals, indica que algú està fent servir la publicació com a base del seu treball actual. Això pot ser un indicador destacat de futures cites més formals i acadèmiques. Aquesta afirmació està avalada pel resultat de l'indicador "Capture", que aporta un total de: 8 (PlumX).

És fonamental presentar evidències que recolzin l'alineació plena amb els principis i directrius institucionals sobre Ciència Oberta i la Conservació i Difusió del Patrimoni Intel·lectual. Un clar exemple d'això és:

  • El treball s'ha enviat a una revista la política editorial de la qual permet la publicació en obert Open Access.

Anàlisi del lideratge dels autors institucionals

Hi ha un lideratge significatiu, ja que alguns dels autors pertanyents a la institució apareixen com a primer o últim signant, es pot apreciar en el detall: Primer Autor (Alba-Castro, M) i Últim Autor (Romero Alvarado, Daniel).

l'autor responsable d'establir les tasques de correspondència ha estat Alba-Castro, M.