Jorge A. Navas

According to our database, Jorge A. Navas authored at least 57 papers between 2005 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Inductive Predicate Synthesis Modulo Programs (Extended).

Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel

CoRR, 2024

Inductive Predicate Synthesis Modulo Programs.

Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel

Proceedings of the 38th European Conference on Object-Oriented Programming, 2024

2023

OCCAM-v2: Combining Static and Dynamic Analysis for Effective and Efficient Whole-Program Specialization.

Jorge A. Navas, Ashish Gehani

Commun. ACM, 2023

2022

OCCAM-v2: Combining Static and Dynamic Analysis for Effective and Efficient Whole-program Specialization: Leveraging scalable pointer analysis, value analysis, and dynamic analysis.

Jorge A. Navas, Ashish Gehani

ACM Queue, 2022

Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE.

Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2022

Efficient Modular SMT-Based Model Checking of Pointer Programs.

Isabel Garcia-Contreras, Arie Gurfinkel, Jorge A. Navas

Proceedings of the Static Analysis - 29th International Symposium, 2022

2021

A Fresh Look at Zones and Octagons.

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

ACM Trans. Program. Lang. Syst., 2021

Compositional Verification of Smart Contracts Through Communication Abstraction (Extended).

Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel

CoRR, 2021

Abstract Interpretation of LLVM with a Region-Based Memory Model.

Arie Gurfinkel, Jorge A. Navas

Proceedings of the Software Verification - 13th International Conference, 2021

Compositional Verification of Smart Contracts Through Communication Abstraction.

Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel

Proceedings of the Static Analysis - 28th International Symposium, 2021

Disjunctive Interval Analysis.

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

Proceedings of the Static Analysis - 28th International Symposium, 2021

Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios.

Muhammad Numair Mansur, Benjamin Mariano, Maria Christakis, Jorge A. Navas, Valentin Wüstholz

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Automated Safety Verification of Programs Invoking Neural Networks.

Maria Christakis, Hasan Ferit Eniser, Holger Hermanns, Jörg Hoffmann, Yugesh Kothari, Jianlin Li, Jorge A. Navas, Valentin Wüstholz

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Automatically Tailoring Static Analysis to Custom Usage Scenarios.

Muhammad Numair Mansur, Benjamin Mariano, Maria Christakis, Jorge A. Navas, Valentin Wüstholz

CoRR, 2020

Verification of an Optimized NTT Algorithm.

Jorge A. Navas, Bruno Dutertre, Ian A. Mason

Proceedings of the Software Verification - 12th International Conference, 2020

MiDas: Containerizing Data-Intensive Applications with I/O Specialization.

Chaitra Niddodi, Ashish Gehani, Tanu Malik, Jorge A. Navas, Sibin Mohan

Proceedings of the 3rd International Workshop on Practical Reproducible Evaluation of Computer Systems, 2020

2019

Simple and precise static analysis of untrusted Linux kernel extensions.

Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, Mooly Sagiv

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Unification-based Pointer Analysis without Oversharing.

Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel

Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

Dissecting Widening: Separating Termination from Information.

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

Proceedings of the Programming Languages and Systems - 17th Asian Symposium, 2019

2018

Executable Counterexamples in Software Model Checking.

Jeffrey Gennari, Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas, Edward J. Schwartz

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Verification of Fault-Tolerant Protocols with Sally.

Bruno Dutertre, Dejan Jovanovic, Jorge A. Navas

Proceedings of the NASA Formal Methods - 10th International Symposium, 2018

Generating Component Interfaces by Integrating Static and Symbolic Analysis, Learning, and Runtime Monitoring.

Falk Howar, Dimitra Giannakopoulou, Malte Mues, Jorge A. Navas

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification, 2018

2017

A Context-Sensitive Memory Model for Verification of C/C++ Programs.

Arie Gurfinkel, Jorge A. Navas

Proceedings of the Static Analysis - 24th International Symposium, 2017

2016

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

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

Theor. Comput. Sci., 2016

An Abstract Domain of Uninterpreted Functions.

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

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Exploiting Sparsity in Difference-Bound Matrices.

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

Proceedings of the Static Analysis - 23rd International Symposium, 2016

2015

Horn clauses as an intermediate representation for program analysis and transformation.

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

Theory Pract. Log. Program., 2015

Algorithmic logic-based verification.

Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas

ACM SIGLOG News, 2015

SeaHorn: A Framework for Verifying C Programs (Competition Contribution).

Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

A Tool for Intersecting Context-Free Grammars and Its Applications.

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

Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

Finding Inconsistencies in Programs with Loops.

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

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

The SeaHorn Verification Framework.

Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, Jorge A. Navas

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Interval Analysis and Machine Arithmetic: Why Signedness Ignorance Is Bliss.

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

ACM Trans. Program. Lang. Syst., 2014

A Partial-Order Approach to Array Content Analysis.

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

CoRR, 2014

Verification of Programs by Combining Iterated Specialization with Interpolation.

Emanuele De Angelis, Fabio Fioravanti, Jorge A. Navas, Maurizio Proietti

Proceedings of the Proceedings First Workshop on Horn Clauses for Verification and Synthesis, 2014

IKOS: A Framework for Static Analysis Based on Abstract Interpretation.

Guillaume Brat, Jorge A. Navas, Nija Shi, Arnaud Venet

Proceedings of the Software Engineering and Formal Methods - 12th International Conference, 2014

Analyzing Array Manipulating Programs by Program Transformation.

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

Proceedings of the Logic-Based Program Synthesis and Transformation, 2014

2013

Failure tabled constraint logic programming by interpolation.

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

Theory Pract. Log. Program., 2013

Unbounded Model-Checking with Interpolation for Regular Language Constraints.

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

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Boosting concolic testing via interpolation.

Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas

Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2013

Abstract Interpretation over Non-lattice Abstract Domains.

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

Proceedings of the Static Analysis - 20th International Symposium, 2013

Modelling Destructive Assignments.

Kathryn Francis, Jorge A. Navas, Peter J. Stuckey

Proceedings of the Principles and Practice of Constraint Programming, 2013

2012

Path-Sensitive Backward Slicing.

Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, Andrew E. Santosa

Proceedings of the Static Analysis - 19th International Symposium, 2012

TRACER: A Symbolic Execution Tool for Verification.

Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, Andrew E. Santosa

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code.

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

Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

2011

Symbolic Execution for Verification.

Joxan Jaffar, Jorge A. Navas, Andrew E. Santosa

CoRR, 2011

Unbounded Symbolic Execution for Program Verification.

Joxan Jaffar, Jorge A. Navas, Andrew E. Santosa

Proceedings of the Runtime Verification - Second International Conference, 2011

2010

Towards Parameterized Regular Type Inference Using Set Constraints

Francisco Bueno, Jorge A. Navas, Manuel V. Hermenegildo

CoRR, 2010

Abstraction Learning.

Joxan Jaffar, Jorge A. Navas, Andrew E. Santosa

Proceedings of the Automated Technology for Verification and Analysis, 2010

2009

User-Definable Resource Usage Bounds Analysis for Java Bytecode.

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

Proceedings of the Fourth Workshop on Bytecode Semantics, 2009

2008

Negative Ternary Set-Sharing.

Eric D. Trias, Jorge A. Navas, Elena S. Ackley, Stephanie Forrest, Manuel V. Hermenegildo

Proceedings of the Logic Programming, 24th International Conference, 2008

2007

An Efficient, Parametric Fixpoint Algorithm for Analysis of Java Bytecode.

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

Proceedings of the Second Workshop on Bytecode Semantics, 2007

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

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

Proceedings of the Logic-Based Program Synthesis and Transformation, 2007

User-Definable Resource Bounds Analysis for Logic Programs.

Jorge A. Navas, Edison Mera, Pedro López-García, Manuel V. Hermenegildo

Proceedings of the Logic Programming, 23rd International Conference, 2007

2006

Efficient Top-Down Set-Sharing Analysis Using Cliques.

Jorge A. Navas, Francisco Bueno, Manuel V. Hermenegildo

Proceedings of the Practical Aspects of Declarative Languages, 8th International Symposium, 2006

2005

A study of set-sharing analysis via cliques.

Jorge A. Navas, Francisco Bueno, Manuel V. Hermenegildo

CoRR, 2005

A Study of Set-Sharing Analysis via Clique.

Jorge A. Navas, Francisco Bueno, Manuel V. Hermenegildo

Proceedings of the 15th International Workshop on Logic Programming Environments, 2005