Ranjit Jhala

According to our database1, Ranjit Jhala
  • authored at least 96 papers between 2001 and 2017.
  • has a "Dijkstra number"2 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

On csauthors.net:

Bibliography

2017
Learning to blame: localizing novice type errors with data-driven diagnosis.
PACMPL, 2017

Local refinement typing.
PACMPL, 2017

Verifying distributed programs via canonical sequentialization.
PACMPL, 2017

Refinement Reflection: Complete Verification with SMT.
CoRR, 2017

Learning to Blame: Localizing Novice Type Errors with Data-Driven Diagnosis.
CoRR, 2017

Deriving Law-Abiding Instances.
CoRR, 2017

Local Refinement Typing.
CoRR, 2017

Finding and Preventing Bugs in JavaScript Bindings.
Proceedings of the 2017 IEEE Symposium on Security and Privacy, 2017

FaCT: A Flexible, Constant-Time Programming Language.
Proceedings of the IEEE Cybersecurity Development, SecDev 2017, Cambridge, MA, USA, 2017

2016
Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131).
Dagstuhl Reports, 2016

Refinement Types for TypeScript.
CoRR, 2016

Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT).
CoRR, 2016

Dynamic Witnesses for Static Type Errors.
CoRR, 2016

Predicate Abstraction for Linked Data Structures.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Printing floating-point numbers: a faster, always correct method.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Refinement types for TypeScript.
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong).
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

2015
NSF expedition on variability-aware software: Recent results and contributions.
it - Information Technology, 2015

Trust, but Verify: Two-Phase Typing for Dynamic Languages.
CoRR, 2015

Bounded Refinement Types.
CoRR, 2015

Predicate Abstraction for Linked Data Structures.
CoRR, 2015

On Subnormal Floating Point and Abnormal Timing.
Proceedings of the 2015 IEEE Symposium on Security and Privacy, 2015

Bounded refinement types.
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

Type Targeted Testing.
Proceedings of the Programming Languages and Systems, 2015

Trust, but Verify: Two-Phase Typing for Dynamic Languages.
Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

2014
Scripting Languages and Frameworks: Analysis and Verification (Dagstuhl Seminar 14271).
Dagstuhl Reports, 2014

From Safety To Termination And Back: SMT-Based Verification For Lazy Languages.
CoRR, 2014

Type Targeted Testing.
CoRR, 2014

Refinement types for Haskell.
Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification, 2014

Refinement types for Haskell.
Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, 2014

LiquidHaskell: experience with refinement types in the real world.
Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, 2014

2013
Abstract Refinement Types.
Proceedings of the Programming Languages and Systems, 2013

2012
Counterexample-guided Planning
CoRR, 2012

Software Verification with Liquid Types.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Nested refinements: a logic for duck typing.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Verifying GPU kernels by test amplification.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Deterministic parallelism via liquid effects.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Towards Verifying Android Apps for the Absence of No-Sleep Energy Bugs.
Proceedings of the 2012 Workshop on Power-Aware Computing Systems, HotPower'12, 2012

Dependent types for JavaScript.
Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

CSolve: Verifying C with Liquid Types.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011
Dependent Types for JavaScript
CoRR, 2011

System D: Dependent Dynamic Dictionaries
CoRR, 2011

HMC: Verifying Functional Programs Using Abstract Interpreters.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Using Types for Software Verification.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

NV-Heaps: making persistent objects fast and safe with next-generation, non-volatile memories.
Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, 2011

Software Verification with Liquid Types.
Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011

2010
Refinement type inference via abstract interpretation
CoRR, 2010

Finding latent performance bugs in systems implementations.
Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010

Low-level liquid types.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

An empirical study of privacy-violating information flows in JavaScript web applications.
Proceedings of the 17th ACM Conference on Computer and Communications Security, 2010

Dsolve: Safety Verification via Liquid Types.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
Software model checking.
ACM Comput. Surv., 2009

Verifying Reference Counting Implementations.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Type-based data structure verification.
Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

Staged information flow for javascript.
Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

Building Distributed Systems Using Mace.
Proceedings of the Proceedings P2P 2009, 2009

2008
Liquid types.
Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, 2008

Dataflow analysis for concurrent programs using datarace detection.
Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, 2008

Deep typechecking and refactoring.
Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2008

2007
The software model checker Blast.
STTT, 2007

Interpolant-Based Transition Relation Approximation.
Logical Methods in Computer Science, 2007

Interpolant-Based Transition Relation Approximation
CoRR, 2007

State of the Union: Type Inference Via Craig Interpolation.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

RELAY: static race detection on millions of lines of code.
Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007

Interprocedural analysis of asynchronous programs.
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Lock allocation.
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Mace: language support for building distributed systems.
Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code (Awarded Best Paper).
Proceedings of the 4th Symposium on Networked Systems Design and Implementation (NSDI 2007), 2007

OPIUM: Optimal Package Install/Uninstall Manager.
Proceedings of the 29th International Conference on Software Engineering (ICSE 2007), 2007

Bounds Checking with Taint-Based Analysis.
Proceedings of the High Performance Embedded Architectures and Compilers, 2007

Array Abstractions from Proofs.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006
A Practical and Complete Approach to Predicate Refinement.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Bit level types for high level reasoning.
Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2006

Structural Invariants.
Proceedings of the Static Analysis, 13th International Symposium, 2006

2005
Counterexample-guided Planning.
Proceedings of the UAI '05, 2005

The BLAST Software Verification System.
Proceedings of the Model Checking Software, 2005

Permissive interfaces.
Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005

Joining dataflow with predicates.
Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005

Path slicing.
Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, 2005

Checking Memory Safety with Blast.
Proceedings of the Fundamental Approaches to Software Engineering, 2005

Interpolant-Based Transition Relation Approximation.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004
The Blast Query Language for Software Verification..
Proceedings of the Static Analysis, 11th International Symposium, 2004

Invited talk: the blast query language for software verification.
Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2004

Abstractions from proofs.
Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004

Race checking by context inference.
Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, 2004

Invited talk: the blast query language for software verification.
Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004

An Eclipse Plug-in for Model Checking.
Proceedings of the 12th International Workshop on Program Comprehension (IWPC 2004), 2004

Generating Tests from Counterexamples.
Proceedings of the 26th International Conference on Software Engineering (ICSE 2004), 2004

2003
Software Verification with BLAST.
Proceedings of the Model Checking Software, 2003

Counterexample-Guided Control.
Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

Thread-Modular Abstraction Refinement.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

Extreme Model Checking.
Proceedings of the Verification: Theory and Practice, 2003

2002
Lazy abstraction.
Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

Temporal-Safety Proofs for Systems Code.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001
Compositional Methods for Probabilistic Systems.
Proceedings of the CONCUR 2001, 2001

Microarchitecture Verification by Compositional Model Checking.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001


  Loading...