Travelled to:1 × Austria
1 × Canada
1 × China
1 × Croatia
1 × Czech Republic
1 × Denmark
1 × Germany
1 × Ireland
1 × Korea
1 × Spain
1 × Sweden
1 × The Netherlands
16 × USA
2 × France
2 × Portugal
6 × Italy
6 × United Kingdom
Collaborated with:R.Majumdar T.A.Henzinger P.M.Rondon K.L.McMillan M.Kawaguchi S.Lerner N.Vazou D.Beyer A.Bakst R.Chugh E.L.Seidel ∅ B.Cosman A.Chlipala P.Vekris R.Xu J.W.Voung W.Weimer M.Emmi C.Tucker D.Shuffelton K.v.Gleissenthall Rami Gökhan Kici G.Sutre C.E.Killian R.Braud J.W.Anderson D.Herman A.Rybalchenko J.Fischer Marc Andrysco D.Stefan J.A.Meister E.Kohler J.S.Fischer S.Qadeer D.Vytiniotis S.L.P.Jones Z.Tatlock A.Vahdat M.Endres G.Sakkas Huma Sibghat K.Chaudhuri W.T.Hallahan A.Xue Maxwell Troy Bland R.Piskac A.Leung M.Gupta Y.Agarwal R.Gupta K.Nagaraj S.Pervez G.C.Necula J.Coburn A.M.Caulfield A.Akel L.M.Grupp R.K.Gupta S.Swanson Anish Tondwalkar V.Choudhury R.G.Scott R.R.Newton P.Wadler Zheng Guo M.James David Justo Jiaxiao Zhou Ziteng Wang N.Polikarpova Sunjay Cauligi Gary Soeller Brian Johannesmeyer Fraser Brown Riad S. Wahby John Renner B.Grégoire G.Barthe
Talks about:type (21) verif (10) refin (10) abstract (7) program (7) liquid (7) verifi (6) softwar (5) languag (5) check (4)
Person: Ranjit Jhala
DBLP: Jhala:Ranjit
Facilitated 2 volumes:
Ed
EdContributed to:
2015
2015
201520142013
2012
2012
2012
20122012
201120112010
201020102009
2009200820082007
2007
20072007200720072006
2006200620052005
200520052004
2004
200420042004
200420042003
2003200220022001
2019
20142017201620162018201920192020Wrote 61 papers:
- ECOOP-2015-VekrisCJ #trust #type system #verification
- Trust, but Verify: Two-Phase Typing for Dynamic Languages (PV, BC, RJ), pp. 52–75.
- ESOP-2015-SeidelVJ #testing
- Type Targeted Testing (ELS, NV, RJ), pp. 812–836.
- ICFP-2015-VazouBJ #bound #refinement
- Bounded refinement types (NV, AB, RJ), pp. 48–61.
- ICFP-2014-VazouSJVJ #haskell #refinement
- Refinement types for Haskell (NV, ELS, RJ, DV, SLPJ), pp. 269–282.
- ESOP-2013-VazouRJ #refinement
- Abstract Refinement Types (NV, PMR, RJ), pp. 209–228.
- CAV-2012-RondonBKJ #c #named #verification
- CSolve: Verifying C with Liquid Types (PMR, AB, MK, RJ), pp. 744–750.
- OOPSLA-2012-ChughHJ #dependent type #javascript
- Dependent types for JavaScript (RC, DH, RJ), pp. 587–606.
- PLDI-2012-KawaguchiRBJ #parallel
- Deterministic parallelism via liquid effects (MK, PMR, AB, RJ), pp. 45–54.
- PLDI-2012-LeungGAGJL #gpu #kernel #verification
- Verifying GPU kernels by test amplification (AL, MG, YA, RG, RJ, SL), pp. 383–394.
- POPL-2012-ChughRJ #logic #type system
- Nested refinements: a logic for duck typing (RC, PMR, RJ), pp. 231–244.
- VMCAI-2012-Jhala #verification
- Software Verification with Liquid Types (RJ), p. 23.
- ASPLOS-2011-CoburnCAGGJS #named #performance #persistent
- NV-Heaps: making persistent objects fast and safe with next-generation, non-volatile memories (JC, AMC, AA, LMG, RKG, RJ, SS), pp. 105–118.
- CAV-2011-Jhala #using #verification
- Using Types for Software Verification (RJ), p. 20.
- CAV-2011-JhalaMR #functional #named #source code #using #verification
- HMC: Verifying Functional Programs Using Abstract Interpreters (RJ, RM, AR), pp. 470–485.
- CAV-2010-KawaguchiRJ #named #safety #verification
- Dsolve: Safety Verification via Liquid Types (MK, PMR, RJ), pp. 123–126.
- FSE-2010-KillianNPBAJ #debugging #implementation #performance
- Finding latent performance bugs in systems implementations (CEK, KN, SP, RB, JWA, RJ), pp. 17–26.
- POPL-2010-RondonKJ #low level
- Low-level liquid types (PMR, MK, RJ), pp. 131–144.
- PLDI-2009-ChughMJL #data flow #javascript #staged
- Staged information flow for javascript (RC, JAM, RJ, SL), pp. 50–62.
- PLDI-2009-KawaguchiRJ #data type #type system #verification
- Type-based data structure verification (MK, PMR, RJ), pp. 304–315.
- TACAS-2009-EmmiJKM #implementation #verification
- Verifying Reference Counting Implementations (ME, RJ, EK, RM), pp. 352–367.
- OOPSLA-2008-TatlockTSJL #refactoring
- Deep typechecking and refactoring (ZT, CT, DS, RJ, SL), pp. 37–52.
- PLDI-2008-ChughVJL #analysis #concurrent #data flow #detection #source code #using
- Dataflow analysis for concurrent programs using datarace detection (RC, JWV, RJ, SL), pp. 316–326.
- PLDI-2008-RondonKJ
- Liquid types (PMR, MK, RJ), pp. 159–169.
- CAV-2007-JhalaM #abstraction #array #proving
- Array Abstractions from Proofs (RJ, KLM), pp. 193–206.
- ESEC-FSE-2007-VoungJL #concurrent #detection #named
- RELAY: static race detection on millions of lines of code (JWV, RJ, SL), pp. 205–214.
- ICSE-2007-TuckerSJL #named
- OPIUM: Optimal Package Install/Uninstall Manager (CT, DS, RJ, SL), pp. 178–188.
- PLDI-2007-KillianABJV #distributed #named
- Mace: language support for building distributed systems (CEK, JWA, RB, RJ, AV), pp. 179–188.
- POPL-2007-EmmiFJM
- Lock allocation (ME, JSF, RJ, RM), pp. 291–296.
- POPL-2007-JhalaM #analysis #interprocedural #source code
- Interprocedural analysis of asynchronous programs (RJ, RM), pp. 339–350.
- TACAS-2007-JhalaMX #type inference
- State of the Union: Type Inference Via Craig Interpolation (RJ, RM, RGX), pp. 553–567.
- FSE-2006-JhalaM #reasoning
- Bit level types for high level reasoning (RJ, RM), pp. 128–140.
- SAS-2006-JhalaMX #invariant
- Structural Invariants (RJ, RM, RGX), pp. 71–87.
- TACAS-2006-JhalaM #approach #refinement
- A Practical and Complete Approach to Predicate Refinement (RJ, KLM), pp. 459–473.
- CAV-2005-JhalaM #approximate
- Interpolant-Based Transition Relation Approximation (RJ, KLM), pp. 39–51.
- ESEC-FSE-2005-FischerJM #data flow
- Joining dataflow with predicates (JF, RJ, RM), pp. 227–236.
- ESEC-FSE-2005-HenzingerJM #interface
- Permissive interfaces (TAH, RJ, RM), pp. 31–40.
- FASE-2005-BeyerHJM #memory management #safety
- Checking Memory Safety with Blast (DB, TAH, RJ, RM), pp. 2–18.
- PLDI-2005-JhalaM #slicing
- Path slicing (RJ, RM), pp. 38–47.
- ICSE-2004-BeyerCM #generative #testing
- Generating Tests from Counterexamples (DB, AC, TAH, RJ, RM), pp. 326–335.
- IWPC-2004-BeyerHJM #eclipse #model checking #plugin
- An Eclipse Plug-in for Model Checking (DB, TAH, RJ, RM), pp. 251–255.
- PEPM-2004-BeyerCHJM #query #verification
- Invited talk: the blast query language for software verification (DB, AC, TAH, RJ, RM), pp. 201–202.
- PLDI-2004-HenzingerJM
- Race checking by context inference (TAH, RJ, RM), pp. 1–13.
- POPL-2004-HenzingerJMM #abstraction #proving
- Abstractions from proofs (TAH, RJ, RM, KLM), pp. 232–244.
- PPDP-2004-BeyerCHJM #query #verification
- Invited talk: the blast query language for software verification (DB, AC, TAH, RJ, RM), pp. 1–2.
- SAS-2004-BeyerCHJM #query #verification
- The Blast Query Language for Software Verification. (DB, AC, TAH, RJ, RM), pp. 2–18.
- CAV-2003-HenzingerJMQ #abstraction #refinement #thread
- Thread-Modular Abstraction Refinement (TAH, RJ, RM, SQ), pp. 262–274.
- ICALP-2003-HenzingerJM
- Counterexample-Guided Control (TAH, RJ, RM), pp. 886–902.
- CAV-2002-HenzingerJMNSW #proving
- Temporal-Safety Proofs for Systems Code (TAH, RJ, RM, GCN, GS, WW), pp. 526–538.
- POPL-2002-HenzingerJMS #abstraction #lazy evaluation
- Lazy abstraction (TAH, RJ, RM, GS), pp. 58–70.
- CAV-2001-JhalaM #architecture #composition #model checking #verification
- Microarchitecture Verification by Compositional Model Checking (RJ, KLM), pp. 396–410.
- ASE-2019-EndresSCJW #automation #named
- InFix: Automatically Repairing Novice Program Inputs (ME, GS, BC, RJ, WW), pp. 399–410.
- Haskell-2014-VazouSJ #experience #haskell #named #refinement
- LiquidHaskell: experience with refinement types in the real world (NV, ELS, RJ), pp. 39–51.
- OOPSLA-2017-BakstGKJ #canonical #distributed #source code #verification
- Verifying distributed programs via canonical sequentialization (AB, KvG, RGK, RJ), p. 27.
- OOPSLA-2017-SeidelSCWJ #data-driven #fault #learning
- Learning to blame: localizing novice type errors with data-driven diagnosis (ELS, HS, KC, WW, RJ), p. 27.
- PLDI-2016-VekrisCJ #refinement #typescript
- Refinement types for TypeScript (PV, BC, RJ), pp. 310–325.
- POPL-2016-AndryscoJL #float #performance
- Printing floating-point numbers: a faster, always correct method (MA, RJ, SL), pp. 555–567.
- POPL-2018-VazouTCSNWJ #refinement #smt #verification
- Refinement reflection: complete verification with SMT (NV, AT, VC, RGS, RRN, PW, RJ), p. 31.
- PLDI-2019-CauligiSJBWRGBJ #domain-specific language #named
- FaCT: a DSL for timing-sensitive computation (SC, GS, BJ, FB, RSW, JR, BG, GB, RJ, DS), pp. 174–189.
- PLDI-2019-HallahanXBJP #execution #lazy evaluation #symbolic computation
- Lazy counterfactual symbolic execution (WTH, AX, MTB, RJ, RP), pp. 411–424.
- POPL-2019-GleissenthallKB #distributed #source code #verification
- Pretend synchrony: synchronous verification of asynchronous distributed programs (KvG, RGK, AB, DS, RJ), p. 30.
- POPL-2020-GuoJJZWJP #abstraction #refinement #synthesis
- Program synthesis by type-guided abstraction refinement (ZG, MJ, DJ, JZ, ZW, RJ, NP), p. 28.