default search action
Ranjit Jhala
Person information
- affiliation: University of California, San Diego, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j24]Cole Kurashige, Ruyi Ji, Aditya Giridharan, Mark Barbone, Daniel Noor, Shachar Itzhaky, Ranjit Jhala, Nadia Polikarpova:
CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs. Proc. ACM Program. Lang. 8(ICFP): 818-844 (2024) - [j23]Robin Webbers
, Klaus von Gleissenthall
Refinement Type Refutations. Proc. ACM Program. Lang. 8(OOPSLA2): 962-987 (2024) - [j22]Michael Borkowski
Mechanizing Refinement Types. Proc. ACM Program. Lang. 8(POPL): 2099-2128 (2024) - [c85]Naomi Smith
Icarus: Trustworthy Just-In-Time Compilers with Symbolic Meta-Execution. SOSP 2024: 473-487 - [i30]Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou:
Laurel: Generating Dafny Assertions Using Large Language Models. CoRR abs/2405.16792 (2024) - 2023
- [j21]Lennart Augustsson
The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming. Proc. ACM Program. Lang. 7(ICFP): 417-447 (2023) - [j20]Adithya Murali
Complete First-Order Reasoning for Properties of Functional Programs. Proc. ACM Program. Lang. 7(OOPSLA2): 1063-1092 (2023) - [j19]Nico Lehmann
Flux: Liquid Types for Rust. Proc. ACM Program. Lang. 7(PLDI): 1533-1557 (2023) - [i29]Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, Deian Stefan:
Robust Constant-Time Cryptography. CoRR abs/2311.05831 (2023) - 2022
- [j18]Georgios Sakkas
Seq2Parse: neurosymbolic parse error repair. Proc. ACM Program. Lang. 6(OOPSLA2): 1180-1206 (2022) - [j17]Matthew Kolosick, Shravan Narayan
Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI. Proc. ACM Program. Lang. 6(POPL): 1-30 (2022) - [c84]Ranjit Jhala:
Embedded Domain Specific Verifiers. Principles of Systems Design 2022: 535-553 - [e5]Ranjit Jhala, Isil Dillig:
PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022. ACM 2022, ISBN 978-1-4503-9265-5 [contents] - [i28]Nico Lehmann, Adam T. Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala:
Flux: Liquid Types for Rust. CoRR abs/2207.04034 (2022) - [i27]Michael Borkowski, Niki Vazou, Ranjit Jhala:
Mechanizing Refinement Types (extended). CoRR abs/2207.05617 (2022) - 2021
- [j16]Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala:
mist: Refinements of Futures Past (Artifact). Dagstuhl Artifacts Ser. 7(2): 03:1-03:11 (2021) - [j15]Ranjit Jhala, Niki Vazou:
Refinement Types: A Tutorial. Found. Trends Program. Lang. 6(3-4): 159-317 (2021) - [j14]Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kici, Ranjit Jhala, Dean M. Tullsen
Automatically eliminating speculative leaks from cryptographic code with blade. Proc. ACM Program. Lang. 5(POPL): 1-30 (2021) - [c83]Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala:
Solver-Aided Constant-Time Hardware Verification. CCS 2021: 429-444 - [c82]Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala:
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types. ECOOP 2021: 18:1-18:29 - [c81]Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala:
STORM: Refinement Types for Secure Web Applications. OSDI 2021: 441-459 - [c80]Michael Emmi, Liana Hadarean, Ranjit Jhala, Lee Pike, Nicolás Rosner, Martin Schäf
RAPID: checking API usage for the cloud in the cloud. ESEC/SIGSOFT FSE 2021: 1416-1426 - [i26]Rami Gökhan Kici, Klaus von Gleissenthall, Deian Stefan, Ranjit Jhala:
Solver-Aided Constant-Time Circuit Verification. CoRR abs/2104.00461 (2021) - [i25]Matthew Kolosick, Shravan Narayan, Conrad Watt, Michael LeMay
Isolation Without Taxation: Near Zero Cost Transitions for SFI. CoRR abs/2105.00033 (2021) - [i24]Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala:
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types (Extended Version). CoRR abs/2105.01954 (2021) - 2020
- [j13]Michael B. James, Zheng Guo, Ziteng Wang
Digging for fold: synthesis-aided API discovery for Haskell. Proc. ACM Program. Lang. 4(OOPSLA): 205:1-205:27 (2020) - [j12]Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang
Program synthesis by type-guided abstraction refinement. Proc. ACM Program. Lang. 4(POPL): 12:1-12:28 (2020) - [c79]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:
Stratified Abstraction of Access Control Policies. CAV (1) 2020: 165-176 - [c78]Georgios Sakkas, Madeline Endres, Benjamin Cosman
Type error feedback via analytic program repair. PLDI 2020: 16-30 - [c77]Benjamin Cosman
PABLO: Helping Novices Debug Python Code Through Data-Driven Fault Localization. SIGCSE 2020: 1047-1053 - [c76]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:
Block public access: trust safety verification of access control policies. ESEC/SIGSOFT FSE 2020: 281-291 - [i23]Marco Vassena, Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala:
Automatically Eliminating Speculative Leaks With Blade. CoRR abs/2005.00294 (2020) - [i22]Ranjit Jhala, Niki Vazou:
Refinement Types: A Tutorial. CoRR abs/2010.07763 (2020)
2010 – 2019
- 2019
- [j11]Klaus von Gleissenthall, Rami Gökhan Kici, Alexander Bakst
Pretend synchrony: synchronous verification of asynchronous distributed programs. Proc. ACM Program. Lang. 3(POPL): 59:1-59:30 (2019) - [c75]Madeline Endres, Georgios Sakkas, Benjamin Cosman
InFix: Automatically Repairing Novice Program Inputs. ASE 2019: 399-410 - [c74]Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan:
FaCT: a DSL for timing-sensitive computation. PLDI 2019: 174-189 - [c73]William T. Hallahan
Lazy counterfactual symbolic execution. PLDI 2019: 411-424 - [c72]Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala:
IODINE: Verifying Constant-Time Execution of Hardware. USENIX Security Symposium 2019: 1411-1428 - [i21]Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala:
Iodine: Verifying Constant-Time Execution of Hardware. CoRR abs/1910.03111 (2019) - [i20]Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, Nadia Polikarpova:
Program Synthesis by Type-Guided Abstraction Refinement. CoRR abs/1911.04091 (2019) - 2018
- [j10]Eric L. Seidel
Dynamic witnesses for static type errors (or, Ill-Typed Programs Usually Go Wrong). J. Funct. Program. 28: e13 (2018) - [j9]Niki Vazou, Anish Tondwalkar, Vikraman Choudhury
Refinement reflection: complete verification with SMT. Proc. ACM Program. Lang. 2(POPL): 53:1-53:31 (2018) - [c71]Marc Andrysco, Andres Nötzli
Towards Verified, Constant-time Floating Point Operations. CCS 2018: 1369-1382 - [p1]Ranjit Jhala, Andreas Podelski, Andrey Rybalchenko:
Predicate Abstraction for Program Verification. Handbook of Model Checking 2018: 447-491 - 2017
- [j8]Benjamin Cosman
Local refinement typing. Proc. ACM Program. Lang. 1(ICFP): 26:1-26:27 (2017) - [j7]Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, Ranjit Jhala:
Learning to blame: localizing novice type errors with data-driven diagnosis. Proc. ACM Program. Lang. 1(OOPSLA): 60:1-60:27 (2017) - [j6]Alexander Bakst
Verifying distributed programs via canonical sequentialization. Proc. ACM Program. Lang. 1(OOPSLA): 110:1-110:27 (2017) - [c70]Sunjay Cauligi, Gary Soeller, Fraser Brown, Brian Johannesmeyer, Yunlu Huang, Ranjit Jhala, Deian Stefan:
FaCT: A Flexible, Constant-Time Programming Language. SecDev 2017: 69-76 - [c69]Fraser Brown, Shravan Narayan
Finding and Preventing Bugs in JavaScript Bindings. IEEE Symposium on Security and Privacy 2017: 559-578 - [i19]Benjamin Cosman, Ranjit Jhala:
Local Refinement Typing. CoRR abs/1706.08007 (2017) - [i18]Ryan G. Scott, Vikraman Choudhury
Deriving Law-Abiding Instances. CoRR abs/1708.02328 (2017) - [i17]Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, Ranjit Jhala:
Learning to Blame: Localizing Novice Type Errors with Data-Driven Diagnosis. CoRR abs/1708.07583 (2017) - [i16]Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala:
Refinement Reflection: Complete Verification with SMT. CoRR abs/1711.03842 (2017) - 2016
- [c68]Eric L. Seidel
Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong). ICFP 2016: 228-242 - [c67]Panagiotis Vekris, Benjamin Cosman
Refinement types for TypeScript. PLDI 2016: 310-325 - [c66]Marc Andrysco, Ranjit Jhala, Sorin Lerner:
Printing floating-point numbers: a faster, always correct method. POPL 2016: 555-567 - [c65]Alexander Bakst
Predicate Abstraction for Linked Data Structures. VMCAI 2016: 65-84 - [i15]Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala:
Refinement Types for TypeScript. CoRR abs/1604.02480 (2016) - [i14]Eric L. Seidel, Ranjit Jhala, Westley Weimer:
Dynamic Witnesses for Static Type Errors. CoRR abs/1606.07557 (2016) - [i13]Niki Vazou, Ranjit Jhala:
Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT). CoRR abs/1610.04641 (2016) - [i12]Marco Gaboardi
Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131). Dagstuhl Reports 6(3): 59-77 (2016) - 2015
- [j5]Lucas Francisco Wanner
NSF expedition on variability-aware software: Recent results and contributions. it Inf. Technol. 57(3): 181-198 (2015) - [c64]Panagiotis Vekris, Benjamin Cosman
Trust, but Verify: Two-Phase Typing for Dynamic Languages. ECOOP 2015: 52-75 - [c63]Eric L. Seidel
Type Targeted Testing. ESOP 2015: 812-836 - [c62]Niki Vazou
Bounded refinement types. ICFP 2015: 48-61 - [c61]Marc Andrysco, David Kohlbrenner, Keaton Mowery, Ranjit Jhala, Sorin Lerner, Hovav Shacham:
On Subnormal Floating Point and Abnormal Timing. IEEE Symposium on Security and Privacy 2015: 623-639 - [i11]Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala:
Trust, but Verify: Two-Phase Typing for Dynamic Languages. CoRR abs/1504.08039 (2015) - [i10]Alexander Bakst, Ranjit Jhala:
Predicate Abstraction for Linked Data Structures. CoRR abs/1505.02298 (2015) - [i9]Niki Vazou, Alexander Bakst, Ranjit Jhala:
Bounded Refinement Types. CoRR abs/1507.00385 (2015) - 2014
- [j4]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan:
Abstractions from proofs. ACM SIGPLAN Notices 49(4S): 79-91 (2014) - [c60]Niki Vazou
LiquidHaskell: experience with refinement types in the real world. Haskell 2014: 39-51 - [c59]Niki Vazou
Refinement types for Haskell. ICFP 2014: 269-282 - [c58]Ranjit Jhala:
Refinement types for Haskell. PLPV 2014: 27-28 - [i8]Niki Vazou, Eric L. Seidel, Ranjit Jhala:
From Safety To Termination And Back: SMT-Based Verification For Lazy Languages. CoRR abs/1401.6227 (2014) - [i7]Eric L. Seidel, Niki Vazou, Ranjit Jhala:
Type Targeted Testing. CoRR abs/1410.5370 (2014) - [i6]Fritz Henglein, Ranjit Jhala, Shriram Krishnamurthi, Peter Thiemann:
Scripting Languages and Frameworks: Analysis and Verification (Dagstuhl Seminar 14271). Dagstuhl Reports 4(6): 84-107 (2014) - 2013
- [c57]Niki Vazou
Abstract Refinement Types. ESOP 2013: 209-228 - [e4]Ranjit Jhala, Koen De Bosschere:
Compiler Construction - 22nd International Conference, CC 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Lecture Notes in Computer Science 7791, Springer 2013, ISBN 978-3-642-37050-2 [contents] - 2012
- [c56]Patrick Maxim Rondon, Alexander Bakst
CSolve: Verifying C with Liquid Types. CAV 2012: 744-750 - [c55]Ravi Chugh, David Herman, Ranjit Jhala:
Dependent types for JavaScript. OOPSLA 2012: 587-606 - [c54]Panagiotis Vekris, Ranjit Jhala, Sorin Lerner, Yuvraj Agarwal:
Towards Verifying Android Apps for the Absence of No-Sleep Energy Bugs. HotPower 2012 - [c53]Ming Kawaguchi, Patrick Maxim Rondon, Alexander Bakst
Deterministic parallelism via liquid effects. PLDI 2012: 45-54 - [c52]Alan Leung, Manish Gupta, Yuvraj Agarwal, Rajesh Gupta, Ranjit Jhala, Sorin Lerner:
Verifying GPU kernels by test amplification. PLDI 2012: 383-394 - [c51]Ravi Chugh, Patrick Maxim Rondon, Ranjit Jhala:
Nested refinements: a logic for duck typing. POPL 2012: 231-244 - [c50]Ranjit Jhala:
Software Verification with Liquid Types. VMCAI 2012: 23 - [e3]Ranjit Jhala, Atsushi Igarashi
Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings. Lecture Notes in Computer Science 7705, Springer 2012, ISBN 978-3-642-35181-5 [contents] - [i5]Krishnendu Chatterjee, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar:
Counterexample-guided Planning. CoRR abs/1207.1373 (2012) - 2011
- [c49]Ranjit Jhala:
Software Verification with Liquid Types. APLAS 2011: 3 - [c48]Joel Coburn, Adrian M. Caulfield, Ameen Akel, Laura M. Grupp, Rajesh K. Gupta, Ranjit Jhala, Steven Swanson
NV-Heaps: making persistent objects fast and safe with next-generation, non-volatile memories. ASPLOS 2011: 105-118 - [c47]Ranjit Jhala:
Using Types for Software Verification. CAV 2011: 20 - [c46]Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko:
HMC: Verifying Functional Programs Using Abstract Interpreters. CAV 2011: 470-485 - [e2]Ranjit Jhala, Wouter Swierstra:
Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, PLPV 2011, Austin, TX, USA, January 29, 2011. ACM 2011, ISBN 978-1-4503-0487-0 [contents] - [e1]Ranjit Jhala, David A. Schmidt:
Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings. Lecture Notes in Computer Science 6538, Springer 2011, ISBN 978-3-642-18274-7 [contents] - [i4]Ravi Chugh, Patrick Maxim Rondon, Ranjit Jhala:
System D: Dependent Dynamic Dictionaries. CoRR abs/1103.5055 (2011) - [i3]Ravi Chugh, Ranjit Jhala:
Dependent Types for JavaScript. CoRR abs/1112.4106 (2011) - 2010
- [c45]Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala:
Dsolve: Safety Verification via Liquid Types. CAV 2010: 123-126 - [c44]Dongseok Jang, Ranjit Jhala, Sorin Lerner, Hovav Shacham:
An empirical study of privacy-violating information flows in JavaScript web applications. CCS 2010: 270-283 - [c43]Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala:
Low-level liquid types. POPL 2010: 131-144 - [c42]Charles Edwin Killian, Karthik Nagaraj, Salman Pervez, Ryan Braud, James W. Anderson, Ranjit Jhala:
Finding latent performance bugs in systems implementations. SIGSOFT FSE 2010: 17-26 - [i2]Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko:
Refinement type inference via abstract interpretation. CoRR abs/1004.2884 (2010)
2000 – 2009
- 2009
- [j3]Ranjit Jhala, Rupak Majumdar:
Software model checking. ACM Comput. Surv. 41(4): 21:1-21:54 (2009) - [c41]Charles Edwin Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, Amin Vahdat:
Building Distributed Systems Using Mace. Peer-to-Peer Computing 2009: 91-92 - [c40]Ravi Chugh, Jeffrey A. Meister, Ranjit Jhala, Sorin Lerner:
Staged information flow for javascript. PLDI 2009: 50-62 - [c39]Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala:
Type-based data structure verification. PLDI 2009: 304-315 - [c38]Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Majumdar:
Verifying Reference Counting Implementations. TACAS 2009: 352-367 - 2008
- [c37]Zachary Tatlock
Deep typechecking and refactoring. OOPSLA 2008: 37-52 - [c36]Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala:
Liquid types. PLDI 2008: 159-169 - [c35]Ravi Chugh, Jan Wen Voung, Ranjit Jhala, Sorin Lerner:
Dataflow analysis for concurrent programs using datarace detection. PLDI 2008: 316-326 - 2007
- [j2]Ranjit Jhala, Kenneth L. McMillan:
Interpolant-Based Transition Relation Approximation. Log. Methods Comput. Sci. 3(4) (2007) - [j1]Dirk Beyer
The software model checker Blast. Int. J. Softw. Tools Technol. Transf. 9(5-6): 505-525 (2007) - [c34]Ranjit Jhala, Kenneth L. McMillan:
Array Abstractions from Proofs. CAV 2007: 193-206 - [c33]Weihaw Chuang, Satish Narayanasamy, Brad Calder, Ranjit Jhala:
Bounds Checking with Taint-Based Analysis. HiPEAC 2007: 71-86 - [c32]Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner:
OPIUM: Optimal Package Install/Uninstall Manager. ICSE 2007: 178-188 - [c31]Charles Edwin Killian, James W. Anderson, Ranjit Jhala, Amin Vahdat:
Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code (Awarded Best Paper). NSDI 2007 - [c30]Charles Edwin Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, Amin Vahdat:
Mace: language support for building distributed systems. PLDI 2007: 179-188 - [c29]Michael Emmi, Jeffrey S. Fischer, Ranjit Jhala, Rupak Majumdar:
Lock allocation. POPL 2007: 291-296 - [c28]Ranjit Jhala, Rupak Majumdar:
Interprocedural analysis of asynchronous programs. POPL 2007: 339-350 - [c27]Jan Wen Voung, Ranjit Jhala, Sorin Lerner:
RELAY: static race detection on millions of lines of code. ESEC/SIGSOFT FSE 2007: 205-214 - [c26]Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu:
State of the Union: Type Inference Via Craig Interpolation. TACAS 2007: 553-567 - [i1]Ranjit Jhala, Kenneth L. McMillan:
Interpolant-Based Transition Relation Approximation. CoRR abs/0706.0523 (2007) - 2006
- [c25]Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu:
Structural Invariants. SAS 2006: 71-87 - [c24]Ranjit Jhala, Rupak Majumdar:
Bit level types for high level reasoning. SIGSOFT FSE 2006: 128-140 - [c23]Ranjit Jhala, Kenneth L. McMillan:
A Practical and Complete Approach to Predicate Refinement. TACAS 2006: 459-473 - 2005
- [c22]Ranjit Jhala, Kenneth L. McMillan:
Interpolant-Based Transition Relation Approximation. CAV 2005: 39-51 - [c21]Dirk Beyer
Checking Memory Safety with Blast. FASE 2005: 2-18 - [c20]Ranjit Jhala, Rupak Majumdar:
Path slicing. PLDI 2005: 38-47 - [c19]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar:
Permissive interfaces. ESEC/SIGSOFT FSE 2005: 31-40 - [c18]Jeffrey Fischer, Ranjit Jhala, Rupak Majumdar:
Joining dataflow with predicates. ESEC/SIGSOFT FSE 2005: 227-236 - [c17]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar:
The BLAST Software Verification System. SPIN 2005: 25-26 - [c16]Krishnendu Chatterjee, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar:
Counterexample-guided Planning. UAI 2005: 104-111 - 2004
- [c15]Dirk Beyer
Generating Tests from Counterexamples. ICSE 2004: 326-335 - [c14]Dirk Beyer
An Eclipse Plug-in for Model Checking. IWPC 2004: 251-255 - [c13]Dirk Beyer
Invited talk: the blast query language for software verification. PEPM 2004: 201-202 - [c12]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar:
Race checking by context inference. PLDI 2004: 1-13 - [c11]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan:
Abstractions from proofs. POPL 2004: 232-244 - [c10]Dirk Beyer
Invited talk: the blast query language for software verification. PPDP 2004: 1-2 - [c9]Dirk Beyer
The Blast Query Language for Software Verification.. SAS 2004: 2-18 - 2003
- [c8]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco A. A. Sanvido:
Extreme Model Checking. Verification: Theory and Practice 2003: 332-358 - [c7]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer:
Thread-Modular Abstraction Refinement. CAV 2003: 262-274 - [c6]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar:
Counterexample-Guided Control. ICALP 2003: 886-902 - [c5]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre:
Software Verification with BLAST. SPIN 2003: 235-239 - 2002
- [c4]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grégoire Sutre, Westley Weimer:
Temporal-Safety Proofs for Systems Code. CAV 2002: 526-538 - [c3]Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre:
Lazy abstraction. POPL 2002: 58-70 - 2001
- [c2]Ranjit Jhala, Kenneth L. McMillan:
Microarchitecture Verification by Compositional Model Checking. CAV 2001: 396-410 - [c1]Luca de Alfaro, Thomas A. Henzinger, Ranjit Jhala:
Compositional Methods for Probabilistic Systems. CONCUR 2001: 351-365
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-02 22:25 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: