{rfName}
A

Indexed in

License and use

Icono OpenAccess

Citations

3

Altmetrics

Analysis of institutional authors

Escobar, SAuthorRomero, DAuthor

Share

Publications
>
Article

A Tool for Automated Certification of Java Source Code in Maude

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

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

Affiliations

Univ Politecn Valencia, Dept Sistemas Informat & Computac - Author

Abstract

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.

Keywords

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

Quality index

Bibliometric impact. Analysis of the contribution and dissemination channel

The work has been published in the journal Electronic Notes In Theoretical Computer Science due to its progression and the good impact it has achieved in recent years, according to the agency Scopus (SJR), it has become a reference in its field. In the year of publication of the work, 2009, it was in position , thus managing to position itself as a Q2 (Segundo Cuartil), in the category Computer Science (Miscellaneous).

Independientemente del impacto esperado determinado por el canal de difusión, es importante destacar el impacto real observado de la propia aportación.

Según las diferentes agencias de indexación, el número de citas acumuladas por esta publicación hasta la fecha 2025-06-26:

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

Impact and social visibility

From the perspective of influence or social adoption, and based on metrics associated with mentions and interactions provided by agencies specializing in calculating the so-called "Alternative or Social Metrics," we can highlight as of 2025-06-26:

  • The use of this contribution in bookmarks, code forks, additions to favorite lists for recurrent reading, as well as general views, indicates that someone is using the publication as a basis for their current work. This may be a notable indicator of future more formal and academic citations. This claim is supported by the result of the "Capture" indicator, which yields a total of: 8 (PlumX).

It is essential to present evidence supporting full alignment with institutional principles and guidelines on Open Science and the Conservation and Dissemination of Intellectual Heritage. A clear example of this is:

  • The work has been submitted to a journal whose editorial policy allows open Open Access publication.

Leadership analysis of institutional authors

There is a significant leadership presence as some of the institution’s authors appear as the first or last signer, detailed as follows: First Author (Alba-Castro, M) and Last Author (Romero Alvarado, Daniel).

the author responsible for correspondence tasks has been Alba-Castro, M.