Travelled to:1 × Denmark
1 × Portugal
1 × Russia
2 × France
2 × Italy
2 × United Kingdom
4 × USA
Collaborated with:M.V.Hermenegildo G.Gange P.Schachte H.Søndergaard P.J.Stuckey J.Jaffar V.Murali A.Gurfinkel T.Kahsai A.E.Santosa M.Méndez-Lojo F.Bueno A.Komuravelli G.Brat N.Shi A.Venet E.Mera P.López-García E.Trias E.S.Ackley S.Forrest J.R.M.Cornish Elazar Gershuni N.Amit N.Narodytska N.Rinetzky L.Ryzhyk M.Sagiv
Talks about:program (7) analysi (6) framework (3) interpol (3) abstract (3) horn (3) constraint (2) transform (2) interpret (2) static (2)
Person: Jorge A. Navas
DBLP: Navas:Jorge_A=
Contributed to:
2015
2015
2015
2014
2014
20132013
2013201320122012200820072007
2006
2019Wrote 16 papers:
- CAV-2015-GurfinkelKKN #framework #verification
- The SeaHorn Verification Framework (AG, TK, AK, JAN), pp. 343–361.
- ICLP-J-2015-GangeNSSS #horn clause #program analysis #program transformation #representation
- Horn clauses as an intermediate representation for program analysis and transformation (GG, JAN, PS, HS, PJS), pp. 526–542.
- TACAS-2015-GurfinkelKN #c #contest #framework #named #source code #verification
- SeaHorn: A Framework for Verifying C Programs (Competition Contribution) (AG, TK, JAN), pp. 447–450.
- LOPSTR-2014-CornishGNSSS #array #program transformation #source code
- Analyzing Array Manipulating Programs by Program Transformation (JRMC, GG, JAN, PS, HS, PJS), pp. 3–20.
- SEFM-2014-BratNSV #abstract interpretation #framework #named #static analysis
- IKOS: A Framework for Static Analysis Based on Abstract Interpretation (GB, JAN, NS, AV), pp. 271–277.
- ESEC-FSE-2013-JaffarMN #testing
- Boosting concolic testing via interpolation (JJ, VM, JAN), pp. 48–58.
- ICLP-J-2013-GangeNSSS #constraints #logic programming
- Failure tabled constraint logic programming by interpolation (GG, JAN, PS, HS, PJS), pp. 593–607.
- SAS-2013-GangeNSSS #abstract domain #abstract interpretation
- Abstract Interpretation over Non-lattice Abstract Domains (GG, JAN, PS, HS, PJS), pp. 6–24.
- TACAS-2013-GangeNSSS #bound #constraints #model checking #regular expression
- Unbounded Model-Checking with Interpolation for Regular Language Constraints (GG, JAN, PJS, HS, PS), pp. 277–291.
- CAV-2012-JaffarMNS #execution #named #symbolic computation #verification
- TRACER: A Symbolic Execution Tool for Verification (JJ, VM, JAN, AES), pp. 758–766.
- SAS-2012-JaffarMNS #slicing
- Path-Sensitive Backward Slicing (JJ, VM, JAN, AES), pp. 231–247.
- ICLP-2008-TriasNAFH
- Negative Ternary Set-Sharing (ET, JAN, ESA, SF, MVH), pp. 301–316.
- ICLP-2007-NavasMLH #analysis #bound #logic programming #source code
- User-Definable Resource Bounds Analysis for Logic Programs (JAN, EM, PLG, MVH), pp. 348–363.
- LOPSTR-2007-Mendez-LojoNH #analysis #approach #flexibility #object-oriented #source code
- A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs (MML, JAN, MVH), pp. 154–168.
- PADL-2006-NavasBH #analysis #clique #performance #top-down #using
- Efficient Top-Down Set-Sharing Analysis Using Cliques (JAN, FB, MVH), pp. 183–198.
- PLDI-2019-GershuniAGNNRRS #kernel #linux #precise #static analysis
- Simple and precise static analysis of untrusted Linux kernel extensions (EG, NA, AG, NN, JAN, NR, LR, MS), pp. 1069–1084.