Jorge A. Navas
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
33
Venues
18
Active years
2006–2025
Best venue rank
A*
Where they publish
Papers
33 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2025 | VMCAI | Automatic Inference of Relational Object Invariants. | Yusen Su, Jorge A. Navas, Arie Gurfinkel, Isabel Garcia-Contreras |
| 2024 | ECOOP | Inductive Predicate Synthesis Modulo Programs. | Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wstholz, Arie Gurfinkel |
| 2022 | SAS | Efficient Modular SMT-Based Model Checking of Pointer Programs. | Isabel Garcia-Contreras, Arie Gurfinkel, Jorge A. Navas |
| 2022 | VMCAI | Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE. | Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wstholz, Arie Gurfinkel |
| 2021 | CAV | Automated Safety Verification of Programs Invoking Neural Networks. | Maria Christakis, Hasan Ferit Eniser, Holger Hermanns, Jrg Hoffmann, Yugesh Kothari, Jianlin Li, Jorge A. Navas, Valentin Wstholz |
| 2021 | CAV | Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios. | Muhammad Numair Mansur, Benjamin Mariano, Maria Christakis, Jorge A. Navas, Valentin Wstholz |
| 2021 | SAS | Disjunctive Interval Analysis. | Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sndergaard, Peter J. Stuckey |
| 2021 | SAS | Compositional Verification of Smart Contracts Through Communication Abstraction. | Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wstholz, Arie Gurfinkel |
| 2020 | HPDC | MiDas: Containerizing Data-Intensive Applications with I/O Specialization. | Chaitra Niddodi, Ashish Gehani, Tanu Malik, Jorge A. Navas, Sibin Mohan |
| 2019 | APLAS | Dissecting Widening: Separating Termination from Information. | Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sndergaard, Peter J. Stuckey |
| 2019 | FMCAD | Unification-based Pointer Analysis without Oversharing. | Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel |
| 2019 | PLDI | 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 |
| 2018 | ISoLA | Generating Component Interfaces by Integrating Static and Symbolic Analysis, Learning, and Runtime Monitoring. | Falk Howar, Dimitra Giannakopoulou, Malte Mues, Jorge A. Navas |
| 2017 | SAS | A Context-Sensitive Memory Model for Verification of C/C++ Programs. | Arie Gurfinkel, Jorge A. Navas |
| 2016 | SAS | Exploiting Sparsity in Difference-Bound Matrices. | Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sndergaard, Peter J. Stuckey |
| 2016 | VMCAI | An Abstract Domain of Uninterpreted Functions. | Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sndergaard, Peter J. Stuckey |
| 2015 | CAV | The SeaHorn Verification Framework. | Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, Jorge A. Navas |
| 2015 | LPAR | Finding Inconsistencies in Programs with Loops. | Temesghen Kahsai, Jorge A. Navas, Dejan Jovanovic, Martin Schf |
| 2015 | TACAS | SeaHorn: A Framework for Verifying C Programs (Competition Contribution). | Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas |
| 2014 | LOPSTR | Analyzing Array Manipulating Programs by Program Transformation. | J. Robert M. Cornish, Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sndergaard, Peter J. Stuckey |
| 2014 | SEFM | IKOS: A Framework for Static Analysis Based on Abstract Interpretation. | Guillaume Brat, Jorge A. Navas, Nija Shi, Arnaud Venet |
| 2013 | CP | Modelling Destructive Assignments. | Kathryn Francis, Jorge A. Navas, Peter J. Stuckey |
| 2013 | SAS | Abstract Interpretation over Non-lattice Abstract Domains. | Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sndergaard, Peter J. Stuckey |
| 2013 | TACAS | Unbounded Model-Checking with Interpolation for Regular Language Constraints. | Graeme Gange, Jorge A. Navas, Peter J. Stuckey, Harald Sndergaard, Peter Schachte |
| 2012 | APLAS | Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code. | Jorge A. Navas, Peter Schachte, Harald Sndergaard, Peter J. Stuckey |
| 2012 | CAV | TRACER: A Symbolic Execution Tool for Verification. | Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, Andrew E. Santosa |
| 2012 | SAS | Path-Sensitive Backward Slicing. | Joxan Jaffar, Vijayaraghavan Murali, Jorge A. Navas, Andrew E. Santosa |
| 2011 | RV | Unbounded Symbolic Execution for Program Verification. | Joxan Jaffar, Jorge A. Navas, Andrew E. Santosa |
| 2010 | ATVA | Abstraction Learning. | Joxan Jaffar, Jorge A. Navas, Andrew E. Santosa |
| 2008 | ICLP | Negative Ternary Set-Sharing. | Eric D. Trias, Jorge A. Navas, Elena S. Ackley, Stephanie Forrest, Manuel V. Hermenegildo |
| 2007 | ICLP | User-Definable Resource Bounds Analysis for Logic Programs. | Jorge A. Navas, Edison Mera, Pedro Lpez-Garca, Manuel V. Hermenegildo |
| 2007 | LOPSTR | A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs. | Mario Mndez-Lojo, Jorge A. Navas, Manuel V. Hermenegildo |
| 2006 | PADL | Efficient Top-Down Set-Sharing Analysis Using Cliques. | Jorge A. Navas, Francisco Bueno, Manuel V. Hermenegildo |