Ranjit Jhala

According to our database, Ranjit Jhala authored at least 118 papers between 2001 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2024

Mechanizing Refinement Types.

Michael Borkowski, Niki Vazou, Ranjit Jhala

Proc. ACM Program. Lang., January, 2024

2023

Complete First-Order Reasoning for Properties of Functional Programs.

Adithya Murali, Lucas Peña, Ranjit Jhala, P. Madhusudan

Proc. ACM Program. Lang., October, 2023

The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming.

Lennart Augustsson, Joachim Breitner, Koen Claessen, Ranjit Jhala, Simon Peyton Jones, Olin Shivers, Guy L. Steele Jr., Tim Sweeney

Proc. ACM Program. Lang., August, 2023

Flux: Liquid Types for Rust.

Nico Lehmann, Adam T. Geller, Niki Vazou, Ranjit Jhala

Proc. ACM Program. Lang., 2023

Robust Constant-Time Cryptography.

Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, Deian Stefan

CoRR, 2023

2022

Seq2Parse: neurosymbolic parse error repair.

Georgios Sakkas, Madeline Endres, Philip J. Guo, Westley Weimer, Ranjit Jhala

Proc. ACM Program. Lang., 2022

Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI.

Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, Deian Stefan

Proc. ACM Program. Lang., 2022

Mechanizing Refinement Types (extended).

Michael Borkowski, Niki Vazou, Ranjit Jhala

CoRR, 2022

Flux: Liquid Types for Rust.

Nico Lehmann, Adam T. Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala

CoRR, 2022

Embedded Domain Specific Verifiers.

Ranjit Jhala

Proceedings of the Principles of Systems Design, 2022

2021

Automatically eliminating speculative leaks from cryptographic code with blade.

Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kici, Ranjit Jhala, Dean M. Tullsen, Deian Stefan

Proc. ACM Program. Lang., 2021

Refinement Types: A Tutorial.

Ranjit Jhala, Niki Vazou

Found. Trends Program. Lang., 2021

mist: Refinements of Futures Past (Artifact).

Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala

Dagstuhl Artifacts Ser., 2021

Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types (Extended Version).

Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala

CoRR, 2021

Isolation Without Taxation: Near Zero Cost Transitions for SFI.

Matthew Kolosick, Shravan Narayan, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, Deian Stefan

CoRR, 2021

Solver-Aided Constant-Time Circuit Verification.

Rami Gökhan Kici, Klaus von Gleissenthall, Deian Stefan, Ranjit Jhala

CoRR, 2021

RAPID: checking API usage for the cloud in the cloud.

Michael Emmi, Liana Hadarean, Ranjit Jhala, Lee Pike, Nicolás Rosner, Martin Schäf, Aritra Sengupta, Willem Visser

Proceedings of the ESEC/FSE '21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2021

STORM: Refinement Types for Secure Web Applications.

Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala

Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation, 2021

Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types.

Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala

Proceedings of the 35th European Conference on Object-Oriented Programming, 2021

Solver-Aided Constant-Time Hardware Verification.

Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala

Proceedings of the CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15, 2021

2020

Digging for fold: synthesis-aided API discovery for Haskell.

Michael B. James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, Nadia Polikarpova

Proc. ACM Program. Lang., 2020

Program synthesis by type-guided abstraction refinement.

Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, Nadia Polikarpova

Proc. ACM Program. Lang., 2020

Automatically Eliminating Speculative Leaks With Blade.

Marco Vassena, Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala

CoRR, 2020

Block public access: trust safety verification of access control policies.

Malik Bouchet, Byron Cook, Bryant Cutler, Anna Druzkina, Andrew Gacek, Liana Hadarean, Ranjit Jhala, Brad Marshall, Daniel Peebles, Neha Rungta, Cole Schlesinger, Chriss Stephens, Carsten Varming, Andy Warfield

Proceedings of the ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2020

PABLO: Helping Novices Debug Python Code Through Data-Driven Fault Localization.

Benjamin Cosman, Madeline Endres, Georgios Sakkas, Leon Medvinsky, Yao-Yuan Yang, Ranjit Jhala, Kamalika Chaudhuri, Westley Weimer

Proceedings of the 51st ACM Technical Symposium on Computer Science Education, 2020

Type error feedback via analytic program repair.

Georgios Sakkas, Madeline Endres, Benjamin Cosman, Westley Weimer, Ranjit Jhala

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Stratified Abstraction of Access Control Policies.

John Backes, Ulises Berrueco, Tyler Bray, Daniel Brim, Byron Cook, Andrew Gacek, Ranjit Jhala, Kasper Søe Luckow, Sean McLaughlin, Madhav Menon, Daniel Peebles, Ujjwal Pugalia, Neha Rungta, Cole Schlesinger, Adam Schodde, Anvesh Tanuku, Carsten Varming, Deepa Viswanathan

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

Pretend synchrony: synchronous verification of asynchronous distributed programs.

Klaus von Gleissenthall, Rami Gökhan Kici, Alexander Bakst, Deian Stefan, Ranjit Jhala

Proc. ACM Program. Lang., 2019

IODINE: Verifying Constant-Time Execution of Hardware.

Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala

Proceedings of the 28th USENIX Security Symposium, 2019

Lazy counterfactual symbolic execution.

William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, Ruzica Piskac

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

FaCT: a DSL for timing-sensitive computation.

Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

InFix: Automatically Repairing Novice Program Inputs.

Madeline Endres, Georgios Sakkas, Benjamin Cosman, Ranjit Jhala, Westley Weimer

Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering, 2019

2018

Predicate Abstraction for Program Verification.

Ranjit Jhala, Andreas Podelski, Andrey Rybalchenko

Proceedings of the Handbook of Model Checking., 2018

Refinement reflection: complete verification with SMT.

Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala

Proc. ACM Program. Lang., 2018

Dynamic witnesses for static type errors (or, Ill-Typed Programs Usually Go Wrong).

Eric L. Seidel, Ranjit Jhala, Westley Weimer

J. Funct. Program., 2018

Towards Verified, Constant-time Floating Point Operations.

Marc Andrysco, Andres Nötzli, Fraser Brown, Ranjit Jhala, Deian Stefan

Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018

2017

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

Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, Ranjit Jhala

Proc. ACM Program. Lang., 2017

Local refinement typing.

Benjamin Cosman, Ranjit Jhala

Proc. ACM Program. Lang., 2017

Verifying distributed programs via canonical sequentialization.

Alexander Bakst, Klaus von Gleissenthall, Rami Gökhan Kici, Ranjit Jhala

Proc. ACM Program. Lang., 2017

Deriving Law-Abiding Instances.

Ryan G. Scott, Vikraman Choudhury, Ryan Newton, Niki Vazou, Ranjit Jhala

CoRR, 2017

Finding and Preventing Bugs in JavaScript Bindings.

Fraser Brown, Shravan Narayan, Riad S. Wahby, Dawson R. Engler, Ranjit Jhala, Deian Stefan

Proceedings of the 2017 IEEE Symposium on Security and Privacy, 2017

FaCT: A Flexible, Constant-Time Programming Language.

Sunjay Cauligi, Gary Soeller, Fraser Brown, Brian Johannesmeyer, Yunlu Huang, Ranjit Jhala, Deian Stefan

Proceedings of the IEEE Cybersecurity Development, SecDev 2017, Cambridge, MA, USA, 2017

2016

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

Marco Gaboardi, Suresh Jagannathan, Ranjit Jhala, Stephanie Weirich

Dagstuhl Reports, 2016

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

Niki Vazou, Ranjit Jhala

CoRR, 2016

Dynamic Witnesses for Static Type Errors.

Eric L. Seidel, Ranjit Jhala, Westley Weimer

CoRR, 2016

Predicate Abstraction for Linked Data Structures.

Alexander Bakst, Ranjit Jhala

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Printing floating-point numbers: a faster, always correct method.

Marc Andrysco, Ranjit Jhala, Sorin Lerner

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Refinement types for TypeScript.

Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

2015

NSF expedition on variability-aware software: Recent results and contributions.

Lucas Francisco Wanner, Liangzhen Lai, Abbas Rahimi, Mark Gottscho, Pietro Mercati, Chu-Hsiang Huang, Frederic Sala, Yuvraj Agarwal, Lara Dolecek, Nikil D. Dutt, Puneet Gupta, Rajesh K. Gupta, Ranjit Jhala, Rakesh Kumar, Sorin Lerner, Subhasish Mitra, Alexandru Nicolau, Tajana Simunic Rosing, Mani B. Srivastava, Steven Swanson, Dennis Sylvester, Yuanyuan Zhou

it Inf. Technol., 2015

On Subnormal Floating Point and Abnormal Timing.

Marc Andrysco, David Kohlbrenner, Keaton Mowery, Ranjit Jhala, Sorin Lerner, Hovav Shacham

Proceedings of the 2015 IEEE Symposium on Security and Privacy, 2015

Bounded refinement types.

Niki Vazou, Alexander Bakst, Ranjit Jhala

Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

Type Targeted Testing.

Eric L. Seidel, Niki Vazou, Ranjit Jhala

Proceedings of the Programming Languages and Systems, 2015

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

Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala

Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

2014

Abstractions from proofs.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan

ACM SIGPLAN Notices, 2014

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

Fritz Henglein, Ranjit Jhala, Shriram Krishnamurthi, Peter Thiemann

Dagstuhl Reports, 2014

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

Niki Vazou, Eric L. Seidel, Ranjit Jhala

CoRR, 2014

Refinement types for Haskell.

Ranjit Jhala

Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification, 2014

Refinement types for Haskell.

Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, Simon L. Peyton Jones

Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, 2014

LiquidHaskell: experience with refinement types in the real world.

Niki Vazou, Eric L. Seidel, Ranjit Jhala

Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, 2014

2013

Abstract Refinement Types.

Niki Vazou, Patrick Maxim Rondon, Ranjit Jhala

Proceedings of the Programming Languages and Systems, 2013

2012

Nested refinements: a logic for duck typing.

Ravi Chugh, Patrick Maxim Rondon, Ranjit Jhala

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Verifying GPU kernels by test amplification.

Alan Leung, Manish Gupta, Yuvraj Agarwal, Rajesh Gupta, Ranjit Jhala, Sorin Lerner

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Deterministic parallelism via liquid effects.

Ming Kawaguchi, Patrick Maxim Rondon, Alexander Bakst, Ranjit Jhala

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.

Panagiotis Vekris, Ranjit Jhala, Sorin Lerner, Yuvraj Agarwal

Proceedings of the 2012 Workshop on Power-Aware Computing Systems, HotPower'12, 2012

Dependent types for JavaScript.

Ravi Chugh, David Herman, Ranjit Jhala

Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

CSolve: Verifying C with Liquid Types.

Patrick Maxim Rondon, Alexander Bakst, Ming Kawaguchi, Ranjit Jhala

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Dependent Types for JavaScript

Ravi Chugh, Ranjit Jhala

CoRR, 2011

System D: Dependent Dynamic Dictionaries

Ravi Chugh, Patrick Maxim Rondon, Ranjit Jhala

CoRR, 2011

HMC: Verifying Functional Programs Using Abstract Interpreters.

Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Using Types for Software Verification.

Ranjit Jhala

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

NV-Heaps: making persistent objects fast and safe with next-generation, non-volatile memories.

Joel Coburn, Adrian M. Caulfield, Ameen Akel, Laura M. Grupp, Rajesh K. Gupta, Ranjit Jhala, Steven Swanson

Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, 2011

Software Verification with Liquid Types.

Ranjit Jhala

Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011

2010

Refinement type inference via abstract interpretation

Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko

CoRR, 2010

Finding latent performance bugs in systems implementations.

Charles Edwin Killian, Karthik Nagaraj, Salman Pervez, Ryan Braud, James W. Anderson, Ranjit Jhala

Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010

Low-level liquid types.

Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala

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.

Dongseok Jang, Ranjit Jhala, Sorin Lerner, Hovav Shacham

Proceedings of the 17th ACM Conference on Computer and Communications Security, 2010

Dsolve: Safety Verification via Liquid Types.

Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

Software model checking.

Ranjit Jhala, Rupak Majumdar

ACM Comput. Surv., 2009

Verifying Reference Counting Implementations.

Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Majumdar

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Type-based data structure verification.

Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala

Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

Staged information flow for javascript.

Ravi Chugh, Jeffrey A. Meister, Ranjit Jhala, Sorin Lerner

Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

Building Distributed Systems Using Mace.

Charles Edwin Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, Amin Vahdat

Proceedings of the Proceedings P2P 2009, 2009

2008

Liquid types.

Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala

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

Dataflow analysis for concurrent programs using datarace detection.

Ravi Chugh, Jan Wen Voung, Ranjit Jhala, Sorin Lerner

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

Deep typechecking and refactoring.

Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner

Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2008

2007

The software model checker Blast.

Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar

Int. J. Softw. Tools Technol. Transf., 2007

Interpolant-Based Transition Relation Approximation.

Ranjit Jhala, Kenneth L. McMillan

Log. Methods Comput. Sci., 2007

State of the Union: Type Inference Via Craig Interpolation.

Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

RELAY: static race detection on millions of lines of code.

Jan Wen Voung, Ranjit Jhala, Sorin Lerner

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.

Ranjit Jhala, Rupak Majumdar

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

Lock allocation.

Michael Emmi, Jeffrey S. Fischer, Ranjit Jhala, Rupak Majumdar

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

Mace: language support for building distributed systems.

Charles Edwin Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, Amin Vahdat

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

Charles Edwin Killian, James W. Anderson, Ranjit Jhala, Amin Vahdat

Proceedings of the 4th Symposium on Networked Systems Design and Implementation (NSDI 2007), 2007

OPIUM: Optimal Package Install/Uninstall Manager.

Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner

Proceedings of the 29th International Conference on Software Engineering (ICSE 2007), 2007

Bounds Checking with Taint-Based Analysis.

Weihaw Chuang, Satish Narayanasamy, Brad Calder, Ranjit Jhala

Proceedings of the High Performance Embedded Architectures and Compilers, 2007

Array Abstractions from Proofs.

Ranjit Jhala, Kenneth L. McMillan

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

A Practical and Complete Approach to Predicate Refinement.

Ranjit Jhala, Kenneth L. McMillan

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Bit level types for high level reasoning.

Ranjit Jhala, Rupak Majumdar

Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2006

Structural Invariants.

Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu

Proceedings of the Static Analysis, 13th International Symposium, 2006

2005

Counterexample-guided Planning.

Krishnendu Chatterjee, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar

Proceedings of the UAI '05, 2005

The BLAST Software Verification System.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar

Proceedings of the Model Checking Software, 2005

Permissive interfaces.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar

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.

Jeffrey Fischer, Ranjit Jhala, Rupak Majumdar

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

Path slicing.

Ranjit Jhala, Rupak Majumdar

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

Checking Memory Safety with Blast.

Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar

Proceedings of the Fundamental Approaches to Software Engineering, 2005

2004

The Blast Query Language for Software Verification..

Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar

Proceedings of the Static Analysis, 11th International Symposium, 2004

Race checking by context inference.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar

Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, 2004

Invited talk: the blast query language for software verification.

Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar

Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004

An Eclipse Plug-in for Model Checking.

Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar

Proceedings of the 12th International Workshop on Program Comprehension (IWPC 2004), 2004

Generating Tests from Counterexamples.

Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar

Proceedings of the 26th International Conference on Software Engineering (ICSE 2004), 2004

2003

Software Verification with BLAST.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre

Proceedings of the Model Checking Software, 2003

Counterexample-Guided Control.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar

Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

Thread-Modular Abstraction Refinement.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

Extreme Model Checking.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco A. A. Sanvido

Proceedings of the Verification: Theory and Practice, 2003

2002

Lazy abstraction.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre

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.

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grégoire Sutre, Westley Weimer

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001

Compositional Methods for Probabilistic Systems.

Luca de Alfaro, Thomas A. Henzinger, Ranjit Jhala

Proceedings of the CONCUR 2001, 2001

Microarchitecture Verification by Compositional Model Checking.

Ranjit Jhala, Kenneth L. McMillan

Proceedings of the Computer Aided Verification, 13th International Conference, 2001