A Study of Set-Sharing Analysis via Clique. - Jorge A. Navas; Francisco Bueno; Manuel V. Hermenegildo (WLPE, 2005)

A study of set-sharing analysis via cliques. - Jorge A. Navas; Francisco Bueno; Manuel V. Hermenegildo (CoRR, 2005)

Efficient Top-Down Set-Sharing Analysis Using Cliques. - Jorge A. Navas; Francisco Bueno; Manuel V. Hermenegildo (PADL, 2006)

User-Definable Resource Bounds Analysis for Logic Programs. - Jorge A. Navas; Edison Mera; Pedro López-García 001; Manuel V. Hermenegildo (ICLP, 2007)

A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs. - Mario Méndez-Lojo; Jorge A. Navas; Manuel V. Hermenegildo (LOPSTR, 2007)

An Efficient, Parametric Fixpoint Algorithm for Analysis of Java Bytecode. - Mario Méndez-Lojo; Jorge A. Navas; Manuel V. Hermenegildo (Bytecode@ETAPS, 2007)

Negative Ternary Set-Sharing. - Eric D. Trias; Jorge A. Navas; Elena S. Ackley; Stephanie Forrest; Manuel V. Hermenegildo (ICLP, 2008)

User-Definable Resource Usage Bounds Analysis for Java Bytecode. - Jorge A. Navas; Mario Méndez-Lojo; Manuel V. Hermenegildo (BYTECODE@ETAPS, 2009)

Abstraction Learning. - Joxan Jaffar; Jorge A. Navas; Andrew E. Santosa (ATVA, 2010)

Towards Parameterized Regular Type Inference Using Set Constraints - Francisco Bueno; Jorge A. Navas; Manuel V. Hermenegildo (CoRR, 2010)

Unbounded Symbolic Execution for Program Verification. - Joxan Jaffar; Jorge A. Navas; Andrew E. Santosa (RV, 2011)

Symbolic Execution for Verification. - Joxan Jaffar; Jorge A. Navas; Andrew E. Santosa (CoRR, 2011)

Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code. - Jorge A. Navas; Peter Schachte; Harald Søndergaard; Peter J. Stuckey (APLAS, 2012)

TRACER: A Symbolic Execution Tool for Verification. - Joxan Jaffar; Vijayaraghavan Murali; Jorge A. Navas; Andrew E. Santosa (CAV, 2012)

Path-Sensitive Backward Slicing. - Joxan Jaffar; Vijayaraghavan Murali; Jorge A. Navas; Andrew E. Santosa (SAS, 2012)

Modelling Destructive Assignments. - Kathryn Francis; Jorge A. Navas; Peter J. Stuckey (CP, 2013)

Abstract Interpretation over Non-lattice Abstract Domains. - Graeme Gange; Jorge A. Navas; Peter Schachte; Harald Søndergaard; Peter J. Stuckey (SAS, 2013)

Boosting concolic testing via interpolation. - Joxan Jaffar; Vijayaraghavan Murali; Jorge A. Navas (ESEC/SIGSOFT FSE, 2013)

Unbounded Model-Checking with Interpolation for Regular Language Constraints. - Graeme Gange; Jorge A. Navas; Peter J. Stuckey; Harald Søndergaard; Peter Schachte (TACAS, 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)

Analyzing Array Manipulating Programs by Program Transformation. - J. Robert M. Cornish; Graeme Gange; Jorge A. Navas; Peter Schachte; Harald Søndergaard; Peter J. Stuckey (LOPSTR, 2014)

IKOS: A Framework for Static Analysis Based on Abstract Interpretation. - Guillaume Brat; Jorge A. Navas; Nija Shi; Arnaud Venet (SEFM, 2014)

Verification of Programs by Combining Iterated Specialization with Interpolation. - Emanuele De Angelis; Fabio Fioravanti; Jorge A. Navas; Maurizio Proietti (HCVS, 2014)

A Partial-Order Approach to Array Content Analysis. - Graeme Gange; Jorge A. Navas; Peter Schachte; Harald Søndergaard; Peter J. Stuckey (CoRR, 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)

The SeaHorn Verification Framework. - Arie Gurfinkel; Temesghen Kahsai; Anvesh Komuravelli; Jorge A. Navas (CAV (1), 2015)

Finding Inconsistencies in Programs with Loops. - Temesghen Kahsai; Jorge A. Navas; Dejan Jovanovic; Martin Schäf (LPAR, 2015)

A Tool for Intersecting Context-Free Grammars and Its Applications. - Graeme Gange; Jorge A. Navas; Peter Schachte; Harald Søndergaard; Peter J. Stuckey (NFM, 2015)

SeaHorn: A Framework for Verifying C Programs (Competition Contribution). - Arie Gurfinkel; Temesghen Kahsai; Jorge A. Navas (TACAS, 2015)

Algorithmic logic-based verification. - Arie Gurfinkel; Temesghen Kahsai; Jorge A. Navas (ACM SIGLOG News, 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)

Exploiting Sparsity in Difference-Bound Matrices. - Graeme Gange; Jorge A. Navas; Peter Schachte; Harald Søndergaard; Peter J. Stuckey (SAS, 2016)

An Abstract Domain of Uninterpreted Functions. - Graeme Gange; Jorge A. Navas; Peter Schachte; Harald Søndergaard; Peter J. Stuckey (VMCAI, 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)

A Context-Sensitive Memory Model for Verification of C/C++ Programs. - Arie Gurfinkel; Jorge A. Navas (SAS, 2017)

Generating Component Interfaces by Integrating Static and Symbolic Analysis, Learning, and Runtime Monitoring. - Falk Howar; Dimitra Giannakopoulou; Malte Mues; Jorge A. Navas (ISoLA (2), 2018)

Verification of Fault-Tolerant Protocols with Sally. - Bruno Dutertre; Dejan Jovanovic; Jorge A. Navas (NFM, 2018)

Executable Counterexamples in Software Model Checking. - Jeffrey Gennari; Arie Gurfinkel; Temesghen Kahsai; Jorge A. Navas; Edward J. Schwartz (VSTTE, 2018)

Dissecting Widening: Separating Termination from Information. - Graeme Gange; Jorge A. Navas; Peter Schachte; Harald Søndergaard; Peter J. Stuckey (APLAS, 2019)

Unification-based Pointer Analysis without Oversharing. - Jakub Kuderski; Jorge A. Navas; Arie Gurfinkel (FMCAD, 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 (PLDI, 2019)

MiDas: Containerizing Data-Intensive Applications with I/O Specialization. - Chaitra Niddodi; Ashish Gehani; Tanu Malik; Jorge A. Navas; Sibin Mohan (P-RECS@HPDC, 2020)

Verification of an Optimized NTT Algorithm. - Jorge A. Navas; Bruno Dutertre; Ian A. Mason (VSTTE, 2020)

Automatically Tailoring Static Analysis to Custom Usage Scenarios. - Muhammad Numair Mansur; Benjamin Mariano; Maria Christakis; Jorge A. Navas; Valentin Wüstholz (CoRR, 2020)

Automated Safety Verification of Programs Invoking Neural Networks. - Maria Christakis; Hasan Ferit Eniser; Holger Hermanns; Jörg Hoffmann 001; Yugesh Kothari; Jianlin Li; Jorge A. Navas; Valentin Wüstholz (CAV (1), 2021)

Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios. - Muhammad Numair Mansur; Benjamin Mariano; Maria Christakis; Jorge A. Navas; Valentin Wüstholz (CAV (2), 2021)

Disjunctive Interval Analysis. - Graeme Gange; Jorge A. Navas; Peter Schachte; Harald Søndergaard; Peter J. Stuckey (SAS, 2021)

Compositional Verification of Smart Contracts Through Communication Abstraction. - Scott Wesley; Maria Christakis; Jorge A. Navas; Richard J. Trefler; Valentin Wüstholz; Arie Gurfinkel (SAS, 2021)

Abstract Interpretation of LLVM with a Region-Based Memory Model. - Arie Gurfinkel; Jorge A. Navas (VSTTE, 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)

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)

Efficient Modular SMT-Based Model Checking of Pointer Programs. - Isabel Garcia-Contreras; Arie Gurfinkel; Jorge A. Navas (SAS, 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 (VMCAI, 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)

OCCAM-v2: Combining Static and Dynamic Analysis for Effective and Efficient Whole-Program Specialization. - Jorge A. Navas; Ashish Gehani (Commun. ACM, 2023)

Inductive Predicate Synthesis Modulo Programs. - Scott Wesley; Maria Christakis; Jorge A. Navas; Richard J. Trefler; Valentin Wüstholz; Arie Gurfinkel (ECOOP, 2024)

Inductive Predicate Synthesis Modulo Programs (Extended). - Scott Wesley; Maria Christakis; Jorge A. Navas; Richard J. Trefler; Valentin Wüstholz; Arie Gurfinkel (CoRR, 2024)

Automatic Inference of Relational Object Invariants. - Yusen Su; Jorge A. Navas; Arie Gurfinkel; Isabel Garcia-Contreras (VMCAI (1), 2025)