Conference Papers

• Explaining Failures of Cyber-Physical Systems with Actual Causality. Khen Elimelech, Tom Yaacov, David A. Kelly, Hana Chockler, Moshe Y. Vardi: ICRA'26.
• Causal Liability in Autonomous Systems. Kaveh Aryan, Hana Chockler, Mohammad Reza Mousavi: FASE 2026: 283–303.
• Counterfactual Influence in Markov Decision Processes. Milad Kazemi, Jessica Lally, Ekaterina Tishchenko, Hana Chockler, Nicola Paoletti: CLeaR 2025: 792–817.
• Multiple Different Black Box Explanations for Image Classifiers. Hana Chockler, David A. Kelly, Daniel Kroening: ECAI 2025: 699–706.
• MRxaI: Black-Box Explainability for Image Classifiers in a Medical Setting. Nathan Blake, David A. Kelly, Santiago Calderon Pena, Akchunya Chanchal, Hana Chockler: EXPLIMED@ECAI 2025.
• Explaining Negative Classifications of AI Models in Tumor Diagnosis. David A. Kelly, Hana Chockler, Nathan Blake: UAI 2025: 2069–2081.
• Test Where Decisions Matter: Importance-driven Testing for Deep Reinforcement Learning. Stefan Pranger, Hana Chockler, Martin Tappler, Bettina Könighofer: NeurIPS 2024.
• Explaining Image Classifiers. Hana Chockler, Joseph Y. Halpern: KR'24.
• A Causal Analysis of Harm. Sander Beckers, Hana Chockler, Joseph Y. Halpern: EWAF 2023.
• Quantifying Harm. Sander Beckers, Hana Chockler, Joseph Y. Halpern: IJCAI 2023: 363–371.
• Challenges in Explaining Brain Tumor Detection. Bénédicte Legastelois, Amy Rafferty, Paul Brennan, Hana Chockler, Ajitha Rajan, Vaishak Belle: TAS 2023: 21:1–21:8.
• On Testing for Discrimination Using Causal Models. Hana Chockler, Joseph Y. Halpern: AAAI 2022: 5548–5555.
• A Study of Demographic Bias in CNN-Based Brain MR Segmentation. Stefanos Ioannou, Hana Chockler, Alexander Hammers, Andrew P. King: MLCN@MICCAI 2022: 13–22.
• A Causal Analysis of Harm. Sander Beckers, Hana Chockler, Joseph Y. Halpern: NeurIPS 2022.
• Explanations for Occluded Images. Hana Chockler, Daniel Kroening, Youcheng Sun: ICCV 2021: 1214–1223.
• Ranking Policy Decisions. Hadrien Pouget, Hana Chockler, Youcheng Sun, Daniel Kroening: NeurIPS 2021: 8702–8713.
• Explaining Image Classifiers Using Statistical Fault Localization. Youcheng Sun, Hana Chockler, Xiaowei Huang, Daniel Kroening: ECCV (28) 2020: 391–406.
• Lattice-based SMT for Program Verification. Karine Even Mendoza, Antti Hyyvarinen, Hana Chockler, Natasha Sharygina: MEMOCODE'19.
• Synthesizing reactive systems using robustness and recovery specifications. Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman: FMCAD 2019, p. 147–151.
• Function Summarization Modulo Theories. Sepideh Asadi, Martin Blicha, Grigory Fedyukovich, Antti Hyyvarinen, Karine Even Mendoza, Natasha Sharygina, Hana Chockler: LPAR-22 2018, p. 56–75.
• Lookahead-Based SMT Solving. Antti Hyyvarinen, Matteo Marescotti, Parvin Sadigova, Hana Chockler, Natasha Sharygina: LPAR-22 2018.
• Lattice-Based Refinement in Bounded Model Checking. Karine Even Mendoza, Sepideh Asadi, Antti Hyyvarinen, Hana Chockler, Natasha Sharygina: VSTTE 2018, p. 50–68.
• Timed Vacuity. Hana Chockler, Shibashis Guha, Orna Kupferman: FM 2018, p. 438–455.
• Combining Experts' Causal Judgments. Dalal Alrajeh, Hana Chockler, Joseph Y. Halpern: AAAI 2018, p. 6311–6318.
• Theory Refinement for Program Verification. Antti Hyyvarinen, Sepideh Asadi, Karine Even Mendoza, Grigory Fedyukovich, Hana Chockler, Natasha Sharygina: SAT 2017, p. 347–363.
• HiFrog: SMT-based Function Summarization for Software Verification. Leonardo Alt, Sepideh Asadi, Hana Chockler, Karine Even Mendoza, Grigory Fedyukovich, Antti Hyvärinen, Natasha Sharygina: TACAS 2017, p. 207–213.
• Synthesizing non-vacuous systems. Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman: VMCAI 2017, p. 55–72.
• Probabilistic Fault Localisation. David Landsberg, Hana Chockler, Daniel Kroening: HVC 2016, p. 65–81.
• Causality and responsibility for formal verification and beyond. Hana Chockler: EPTCS 224, 2016, p. 1–8.
• Learning the Language of Error. Martin Chapman, Hana Chockler, Pascal Kesseli, Daniel Kroening, Ofer Strichman, Michael Tautschnig: ATVA 2015, p. 114–130.
• Causal Analysis for Attributing Responsibility in Legal Cases. Hana Chockler, Norman Fenton, Jeroen Keppens, David Lagnado: ICAIL 2015.
• Evaluation of Measures for Statistical Fault Localisation and an Optimising Scheme. David Landsberg, Hana Chockler, Daniel Kroening, Matt Lewis: FASE 2015, p. 115–129.
• The computational complexity of structure-based causality. Gadi Aleksandrowicz, Hana Chockler, Joseph Y. Halpern, Alexander Ivrii: AAAI 2014, p. 974–980.
• Attention-based coverage metrics. Shoham Ben-David, Hana Chockler, Orna Kupferman: HVC 2013, p. 230–245.
• Finding rare numerical stability errors in concurrent computations. Hana Chockler, Karine Even, Eran Yahav: ISSTA 2013, p. 12–22.
• Using cross-entropy for satisfiability. Hana Chockler, Alexander Ivrii, Arie Matsliah, Simone Fulvio Rollini, Natasha Sharygina: SAC 2013, p. 1196–1203.
• Computing Interpolants without Proofs. Hana Chockler, Alexander Ivrii, Arie Matsliah: HVC 2012, p. 72–85.
• Incremental formal verification of hardware. Hana Chockler, Alexander Ivrii, Arie Matsliah, Shiri Moran, Ziv Nevo: FMCAD 2011, p. 135–143.
• Variants of LTL Query Checking. Hana Chockler, Arie Gurfinkel, Ofer Strichman: HVC 2010, p. 76–92.
• Coverage in interpolation-based model checking. Hana Chockler, Daniel Kroening, Mitra Purandare: DAC 2010, p. 182–187.
• Cross-Entropy-Based Replay of Concurrent Programs. Hana Chockler, Eitan Farchi, Benny Godlin, Sergey Novikov: FASE 2009, p. 201–215.
• Explaining Counterexamples Using Causality. Ilan Beer, Shoham Ben-David, Hana Chockler, Avigail Orni, Richard Trefler: CAV 2009, p. 94–108.
• Beyond Vacuity: Towards the Strongest Passing Formula. Hana Chockler, Arie Gurfinkel, Ofer Strichman: FMCAD 2008, p. 188–195.
• Efficient automatic STE refinement using responsibility. Hana Chockler, Orna Grumberg, Avi Yadgar: TACAS 2008, p. 233–248.
• Cross-Entropy Based Testing. Hana Chockler, Eitan Farchi, Benny Godlin, Sergey Novikov: FMCAD 2007, p. 101–108.
• Easier and More Informative Vacuity Checks. Hana Chockler, Ofer Strichman: MEMOCODE 2007, p. 189–198.
• Temporal Modalities for Concisely Capturing Timing Diagrams. Hana Chockler, Kathi Fisler: CHARME 2005, p. 176–190.
• Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs. Hana Chockler, Paul C. Attie: VMCAI 2005, p. 465–481.
• Coverage Metrics for Formal Verification. Hana Chockler, Orna Kupferman, Moshe Y. Vardi: CHARME 2003, p. 111–125.
• Responsibility and Blame: A Structural-Model Approach. Hana Chockler, Joseph Y. Halpern: IJCAI-03, p. 147–153.
• Coverage of Implementations by Simulating Specifications. Hana Chockler, Orna Kupferman: TCS 2002, p. 409–421.
• Coverage Metrics for Temporal Logic Model Checking. Hana Chockler, Orna Kupferman, Moshe Y. Vardi: TACAS 2001, p. 528–542.
• A Practical Approach to Coverage in Model Checking. Hana Chockler, Orna Kupferman, Robert Kurshan, Moshe Y. Vardi: CAV 2001, p. 66–78.