Jesús Mauricio Chimento

dblp:149/0001 · DBLP profile ↗
← Back
3ranked-venue papers
1as first author
0since 2021 · last 2017
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 2 · 1 first-authorTheory of computation · 2

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Software engineering, system software, and programming languages
1 paper
Program verification · 67% Programming languages and type systems · 33%

Topics — the 3 heaviest of 3, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Program verification › dynamic verification
runtime verification
0.212015
A Specification Language for Static and Runtime Verification of Data and Control Properties · FM 2015
Programming languages and type systems
specification language
0.212015
A Specification Language for Static and Runtime Verification of Data and Control Properties · FM 2015
Program verification
static verification
0.212015
A Specification Language for Static and Runtime Verification of Data and Control Properties · FM 2015
YearPublicationVenuePosition
2017 Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
abstract
Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The analysis is necessarily an over-approximation as the real executions of the program are not available at analysis time. In contrast, runtime verification techniques have been extensively used for control-oriented properties, analysing the current execution path of the program in a fully automatic manner. In this article, we present a novel approach in which data-oriented and control-oriented properties may be stated in a single formalism amenable to both static and dynamic verification techniques. The specification language we present to achieve this that of ppDATEs, which enhances the control-oriented property language of DATEs, with data-oriented pre/postconditions. For runtime verification of ppDATE specifications, the language is translated into a DATE. We give a formal semantics to ppDATEs, which we use to prove the correctness of our translation from ppDATEs to DATEs. We show how ppDATE specifications can be analysed using a combination of the deductive theorem prover KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY first partially proves the data-oriented part of the specification, simplifying the specification which is then passed on to LARVA to check at runtime for the remaining parts of the specification including the control-oriented aspects. We show the applicability of our approach on two case studies.
Wolfgang Ahrendt, Jesús Mauricio Chimento, Gordon J. Pace, Gerardo Schneider
Formal Methods Syst. Des.2
2015 A Specification Language for Static and Runtime Verification of Data and Control Properties
Wolfgang Ahrendt, Jesús Mauricio Chimento, Gordon J. Pace, Gerardo Schneider
FM2
2015 StaRVOOrS: A Tool for Combined Static and Runtime Verification of Java
Jesús Mauricio Chimento, Wolfgang Ahrendt, Gordon J. Pace, Gerardo Schneider
RV1