Author name cluster

Jorge A. Navas

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

2 author rows

TCS Journal 2016 Journal Article

A complete refinement procedure for regular separability of context-free languages

Graeme Gange
Jorge A. Navas
Peter Schachte
Harald Søndergaard
Peter J. Stuckey

Often, when analyzing the behaviour of systems modelled as context-free languages, we wish to know if two languages overlap. To this end, we present a class of semi-decision procedures for regular separability of context-free languages, based on counter-example guided abstraction refinement. We propose two effective instances of this approach, one that is complete but relatively expensive, and one that is inexpensive and sound, but for which we do not have a completeness proof. The complete method will prove disjointness whenever the input languages are regularly separable. Both methods will terminate whenever the input languages overlap. We provide an experimental evaluation of these procedures, and demonstrate their practicality on a range of verification and language-theoretic instances.

Details DOI

LPAR Conference 2015 Conference Paper

Finding Inconsistencies in Programs with Loops

Temesghen Kahsai
Jorge A. Navas
Dejan Jovanovic
Martin Schäf

Abstract Inconsistent code is an important class of program abnormalities that appears in real-world code bases and often reveals serious bugs. A piece of code is inconsistent if it is not part of any safely terminating execution. Existing approaches to inconsistent code detection scale to programs with millions of lines of code, and have lead to patches in applications like the web-server Tomcat or the Linux kernel. However, the ability of existing tools to detect inconsistencies is limited by gross over-approximation of looping control-flow. We present a novel approach to inconsistent code detection that can reason about programs with loops without compromising precision. To that end, by leveraging recent advances in software model checking and Horn clause solving, we demonstrate how to encode the problem as a sequence of Horn clauses queries enabling us to detect inconsistencies that were previously unattainable.

Details

LOPSTR Conference 2014 Conference Paper

Analyzing Array Manipulating Programs by Program Transformation

J. Robert M. Cornish
Graeme Gange
Jorge A. Navas
Peter Schachte
Harald Søndergaard
Peter J. Stuckey

Abstract We explore a transformational approach to the problem of verifying simple array-manipulating programs. Traditionally, verification of such programs requires intricate analysis machinery to reason with universally quantified statements about symbolic array segments, such as “every data item stored in the segment A[i] to A[j] is equal to the corresponding item stored in the segment B[i] to B[j]. ” We define a simple abstract machine which allows for set-valued variables and we show how to translate programs with array operations to array-free code for this machine. For the purpose of program analysis, the translated program remains faithful to the semantics of array manipulation. Based on our implementation in LLVM, we evaluate the approach with respect to its ability to extract useful invariants and the cost in terms of code size.

Details

LOPSTR Conference 2007 Conference Paper

A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs

Mario Méndez-Lojo
Jorge A. Navas
Manuel V. Hermenegildo

Abstract Static analyses of object-oriented programs usually rely on intermediate representations that respect the original semantics while having a more uniform and basic syntax. Most of the work involving object-oriented languages and abstract interpretation usually omits the description of that language or just refers to the Control Flow Graph (CFG) it represents. However, this lack of formalization on one hand results in an absence of assurances regarding the correctness of the transformation and on the other it typically strongly couples the analysis to the source language. In this work we present a framework for analysis of object-oriented languages in which in a first phase we transform the input program into a representation based on Horn clauses. This facilitates on one hand proving the correctness of the transformation attending to a simple condition and on the other allows applying existing analyzers for (constraint) logic programming to automatically derive a safe approximation of the semantics of the original program. The approach is flexible in the sense that the first phase decouples the analyzer from most language-dependent features, and correct because the set of Horn clauses returned by the transformation phase safely approximates the standard semantics of the input program. The resulting analysis is also reasonably scalable due to the use of mature, modular (C)LP-based analyzers. This allows us to report good results for medium-sized programs.

Details