Jorge A. Navas

Publication Activity (10 Years)

Years Active: 2005-2024
Publications (10 Years): 26

Top Topics

Intermediate Representation

Static Analysis

Top Venues

Publications

Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
Inductive Predicate Synthesis Modulo Programs (Extended). CoRR (2024)
Jorge A. Navas, Ashish Gehani
OCCAM-v2: Combining Static and Dynamic Analysis for Effective and Efficient Whole-Program Specialization. Commun. ACM 66 (4) (2023)
Jorge A. Navas, Ashish Gehani
OCCAM-v2: Combining Static and Dynamic Analysis for Effective and Efficient Whole-program Specialization: Leveraging scalable pointer analysis, value analysis, and dynamic analysis. ACM Queue 20 (5) (2022)
Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE. VMCAI (2022)
Isabel Garcia-Contreras, Arie Gurfinkel, Jorge A. Navas
Efficient Modular SMT-Based Model Checking of Pointer Programs. SAS (2022)
Maria Christakis, Hasan Ferit Eniser, Holger Hermanns, Jörg Hoffmann, Yugesh Kothari, Jianlin Li, Jorge A. Navas, Valentin Wüstholz
Automated Safety Verification of Programs Invoking Neural Networks. CAV (1) (2021)
Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
Compositional Verification of Smart Contracts Through Communication Abstraction. SAS (2021)
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
Disjunctive Interval Analysis. SAS (2021)
Graeme Gange, Zequn Ma, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
A Fresh Look at Zones and Octagons. ACM Trans. Program. Lang. Syst. 43 (3) (2021)
Muhammad Numair Mansur, Benjamin Mariano, Maria Christakis, Jorge A. Navas, Valentin Wüstholz
Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios. CAV (2) (2021)
Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
Compositional Verification of Smart Contracts Through Communication Abstraction (Extended). CoRR (2021)
Arie Gurfinkel, Jorge A. Navas
Abstract Interpretation of LLVM with a Region-Based Memory Model. VSTTE (2021)
Jorge A. Navas, Bruno Dutertre, Ian A. Mason
Verification of an Optimized NTT Algorithm. VSTTE (2020)
Muhammad Numair Mansur, Benjamin Mariano, Maria Christakis, Jorge A. Navas, Valentin Wüstholz
Automatically Tailoring Static Analysis to Custom Usage Scenarios. CoRR (2020)
Chaitra Niddodi, Ashish Gehani, Tanu Malik, Jorge A. Navas, Sibin Mohan
MiDas: Containerizing Data-Intensive Applications with I/O Specialization. P-RECS@HPDC (2020)
Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel
Unification-based Pointer Analysis without Oversharing. CoRR (2019)
Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel
Unification-based Pointer Analysis without Oversharing. FMCAD (2019)
Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, Mooly Sagiv
Simple and precise static analysis of untrusted Linux kernel extensions. PLDI (2019)
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
Dissecting Widening: Separating Termination from Information. APLAS (2019)
Falk Howar, Dimitra Giannakopoulou, Malte Mues, Jorge A. Navas
Generating Component Interfaces by Integrating Static and Symbolic Analysis, Learning, and Runtime Monitoring. ISoLA (2) (2018)
Jeffrey Gennari, Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas, Edward J. Schwartz
Executable Counterexamples in Software Model Checking. VSTTE (2018)
Bruno Dutertre, Dejan Jovanovic, Jorge A. Navas
Verification of Fault-Tolerant Protocols with Sally. NFM (2018)
Arie Gurfinkel, Jorge A. Navas
A Context-Sensitive Memory Model for Verification of C/C++ Programs. SAS (2017)
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
A complete refinement procedure for regular separability of context-free languages. Theor. Comput. Sci. 625 (2016)
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
An Abstract Domain of Uninterpreted Functions. VMCAI (2016)
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
Exploiting Sparsity in Difference-Bound Matrices. SAS (2016)
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
A Tool for Intersecting Context-Free Grammars and Its Applications. NFM (2015)
Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas
Algorithmic logic-based verification. ACM SIGLOG News 2 (2) (2015)
Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas
SeaHorn: A Framework for Verifying C Programs (Competition Contribution). TACAS (2015)
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
Horn Clauses as an Intermediate Representation for Program Analysis and Transformation. CoRR (2015)
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
Horn clauses as an intermediate representation for program analysis and transformation. Theory Pract. Log. Program. 15 (4-5) (2015)
Temesghen Kahsai, Jorge A. Navas, Dejan Jovanovic, Martin Schäf
Finding Inconsistencies in Programs with Loops. LPAR (2015)
Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, Jorge A. Navas
The SeaHorn Verification Framework. CAV (1) (2015)
Emanuele De Angelis, Fabio Fioravanti, Jorge A. Navas, Maurizio Proietti
Verification of Programs by Combining Iterated Specialization with Interpolation. HCVS (2014)
Guillaume Brat, Jorge A. Navas, Nija Shi, Arnaud Venet
IKOS: A Framework for Static Analysis Based on Abstract Interpretation. SEFM (2014)
J. Robert M. Cornish, Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
Analyzing Array Manipulating Programs by Program Transformation. LOPSTR (2014)
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
Interval Analysis and Machine Arithmetic: Why Signedness Ignorance Is Bliss. ACM Trans. Program. Lang. Syst. 37 (1) (2014)
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
A Complete Refinement Procedure for Regular Separability of Context-Free Languages. CoRR (2014)
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
A Partial-Order Approach to Array Content Analysis. CoRR (2014)
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
Failure tabled constraint logic programming by interpolation. Theory Pract. Log. Program. 13 (4-5) (2013)
Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas
Boosting concolic testing via interpolation. ESEC/SIGSOFT FSE (2013)
Graeme Gange, Jorge A. Navas, Peter J. Stuckey, Harald Søndergaard, Peter Schachte
Unbounded Model-Checking with Interpolation for Regular Language Constraints. TACAS (2013)
Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
Abstract Interpretation over Non-lattice Abstract Domains. SAS (2013)
Kathryn Francis, Jorge A. Navas, Peter J. Stuckey
Modelling Destructive Assignments. CP (2013)
Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, Andrew E. Santosa
Path-Sensitive Backward Slicing. SAS (2012)
Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, Andrew E. Santosa
TRACER: A Symbolic Execution Tool for Verification. CAV (2012)
Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey
Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code. APLAS (2012)
Joxan Jaffar, Jorge A. Navas, Andrew E. Santosa
Unbounded Symbolic Execution for Program Verification. RV (2011)
Joxan Jaffar, Jorge A. Navas, Andrew E. Santosa
Symbolic Execution for Verification. CoRR (2011)
Francisco Bueno, Jorge A. Navas, Manuel V. Hermenegildo
Towards Parameterized Regular Type Inference Using Set Constraints CoRR (2010)
Joxan Jaffar, Jorge A. Navas, Andrew E. Santosa
Abstraction Learning. ATVA (2010)
Jorge A. Navas, Mario Méndez-Lojo, Manuel V. Hermenegildo
User-Definable Resource Usage Bounds Analysis for Java Bytecode. Electron. Notes Theor. Comput. Sci. 253 (5) (2009)
Eric D. Trias, Jorge A. Navas, Elena S. Ackley, Stephanie Forrest, Manuel V. Hermenegildo
Negative Ternary Set-Sharing. ICLP (2008)
Jorge A. Navas, Edison Mera, Pedro López-García, Manuel V. Hermenegildo
User-Definable Resource Bounds Analysis for Logic Programs. ICLP (2007)
Mario Méndez-Lojo, Jorge A. Navas, Manuel V. Hermenegildo
An Efficient, Parametric Fixpoint Algorithm for Analysis of Java Bytecode. Electron. Notes Theor. Comput. Sci. 190 (1) (2007)
Mario Méndez-Lojo, Jorge A. Navas, Manuel V. Hermenegildo
A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs. LOPSTR (2007)
Jorge A. Navas, Francisco Bueno, Manuel V. Hermenegildo
Efficient Top-Down Set-Sharing Analysis Using Cliques. PADL (2006)
Jorge A. Navas, Francisco Bueno, Manuel V. Hermenegildo
A study of set-sharing analysis via cliques. CoRR (2005)
Jorge A. Navas, Francisco Bueno, Manuel V. Hermenegildo
A Study of Set-Sharing Analysis via Clique. WLPE (2005)