Jorge A. Navas

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