BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Jhala:Ranjit

Facilitated 2 volumes:

CC 2013Ed
VMCAI 2011Ed

Contributed to:

ECOOP 20152015
ESOP 20152015
ICFP 20152015
ICFP 20142014
ESOP 20132013
CAV 20122012
OOPSLA 20122012
PLDI 20122012
POPL 20122012
VMCAI 20122012
ASPLOS 20112011
CAV 20112011
CAV 20102010
FSE 20102010
POPL 20102010
PLDI 20092009
TACAS 20092009
OOPSLA 20082008
PLDI 20082008
CAV 20072007
ESEC/FSE 20072007
ICSE 20072007
PLDI 20072007
POPL 20072007
TACAS 20072007
FSE 20062006
SAS 20062006
TACAS 20062006
CAV 20052005
ESEC/FSE 20052005
FASE 20052005
PLDI 20052005
ICSE 20042004
IWPC 20042004
PEPM 20042004
PLDI 20042004
POPL 20042004
PPDP 20042004
SAS 20042004
CAV 20032003
ICALP 20032003
CAV 20022002
POPL 20022002
CAV 20012001
ASE 20192019
Haskell 20142014
OOPSLA 20172017
PLDI 20162016
POPL 20162016
POPL 20182018
PLDI 20192019
POPL 20192019
POPL 20202020

Wrote 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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.