Conference Papers

Conference Papers

  • Lattice-based SMT for Program Verification. / Even Mendoza, Karine; Hyyvarinen, Antti; Chockler, Hana; Sharygina, Natasha. MEMOCODE’19: 17th ACM-IEEE International Conference on Formal Methods and Models for System Design. ACM, 2019.
  • Synthesizing reactive systems using robustness and recovery specifications. / Bloem, Roderick; Chockler, Hana; Ebrahimi, Masoud; Strichman, Ofer. Proceedings of the 19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019. ed. / Clark Barrett; Jin Yang. Institute of Electrical and Electronics Engineers Inc., 2019. p. 147-151 8894276.
  • Function Summarization Modulo Theories. / Asadi, Sepideh; Blicha, Martin; Fedyukovich, Grigory; Hyyvarinen, Antti; Even Mendoza, Karine; Sharygina, Natasha; Chockler, Hana. LPAR-22: 22nd International Conference on Logic for Programming, Articial Intelligence and Reasoning. Vol. 57 2018. p. 56-75 (EPiC Series in Computing).
  • Lookahead-Based SMT Solving. / Hyyvarinen, Antti; Marescotti, Matteo; Sadigova, Parvin; Chockler, Hana; Sharygina, Natasha. LPAR-22: 22nd International Conference on Logic for Programming, Articial Intelligence and Reasoning. Vol. 57 2018.
  • Lattice-Based Refinement in Bounded Model Checking. / Even Mendoza, Karine; Asadi, Sepideh; Hyyvarinen, Antti; Chockler, Hana; Sharygina, Natasha. Verified Software. Theories, Tools, and Experiments (VSTTE) 2018. Switzerland : Springer, 2018. p. 50-68.
  • Timed Vacuity. / Chockler, Hana; Guha, Shibashis; Kupferman, Orna. International Symposium on Formal Methods (FM). Vol. 10951 Springer, 2018. p. 438-455 (LNCS).
  • Combining Experts’ Causal Judgments. / Alrajeh, Dalal; Chockler, Hana; Halpern, Joseph Y. Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence. AAAI Press, 2018. p. 6311-6318.
  • Theory Refinement for Program Verification. / Hyyvarinen, Antti; Asadi, Sepideh; Even Mendoza, Karine; Fedyukovich, Grigory; Chockler, Hana; Sharygina, Natasha. 20th International Conference on Theory and Applications of Satisfiability Testing (SAT). Vol. 10491 Springer, 2017. p. 347-363.
  • HiFrog: SMT-based Function Summarization for Software Verification. / Alt, Leonardo; Asadi, Sepideh; Chockler, Hana; Even Mendoza, Karine; Fedyukovich, Grigory; Hyvärinen, Antti E. J.; Sharygina, Natasha. Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II. Vol. 10206 Springer, 2017. p. 207-213.
  • Synthesizing non-vacuous systems. / Bloem, Roderick; Chockler, Hana; Ebrahimi, Masoud; Strichman, Ofer. Proceedings of 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI): Lecture Notes in Computer Science. Vol. 10145 Springer‐Verlag Berlin Heidelberg, 2017. p. 55-72.
  • Probabilistic Fault Localisation. / Landsberg, David; Chockler, Hana; Kroening, Daniel. Lecture Notes in Computer Science: Hardware and Software: Verification and Testing. Vol. 10028 LNCS Springer‐Verlag Berlin Heidelberg, 2016. p. 65-81.
  • Causality and responsibility for formal verification and beyond. / Chockler, Hana. Electronic Proceedings in Theoretical Computer Science, EPTCS. Vol. 224 Open Publishing Association, 2016. p. 1-8.
  • Preface. / Benferhat, Salem; Chockler, Hana; Fabre, Eric; Fey, Görschwin; Gössler, Gregor; Groce, Alex; Hallé, Sylvain; Halpern, Joseph; Leue, Stefan; Nickovic, Dejan; Podgurski, Andy; Sokolsky, Oleg; Stefani, Jean Bernard; Travé-Massuyès, Louise; Vennekens, Joost; Wang, Chao; Weissenbacher, Georg. Electronic Proceedings in Theoretical Computer Science, Vol. 224, 26.08.2016.
  • Learning the Language of Error. / Chapman, Martin; Chockler, Hana; Kesseli, Pascal; Kroening, Daniel; Strichman, Ofer; Tautschnig, Michael. Proceedings of ATVA 2015: Automated Technology for Verification and Analysis . Vol. 9364 Springer, 2015. p. 114-130 (Lecture Notes in Computer Science).
  • Causal Analysis for Attributing Responsibility in Legal Cases. / Chockler, Hana; Fenton, Norman; Keppens, Jeroen; Lagnado, David. The 15th International Conference on Artificial Intelligence & Law – Proceedings. ACM Digital Library, 2015.
  • Challenges of existing technology. / Chockler, Hana; Kroening, Daniel; Mariani, Leonardo; Sharygina, Natasha. Validation of Evolving Software. Springer International Publishing Switzerland, 2015. p. 7-17 (Chapter).
  • Complementarities among the technologies presented in the book. / Chockler, Hana; Kroening, Daniel; Mariani, Leonardo; Sharygina, Natasha. Validation of Evolving Software. Springer International Publishing Switzerland, 2015. p. 19-21 (Chapter).
  • Lightweight static analysis check of upgrades in c/c++ software. / Chockler, Hana; Ruah, Sitvanit. Validation of Evolving Software. Springer International Publishing Switzerland, 2015. p. 25-36 (Chapter).
  • Validation of evolving software. / Chockler, Hana; Kroening, Daniel; Mariani, Leonardo; Sharygina, Natasha (Editors). Springer International Publishing Switzerland, 2015. 220 p.
  • Evaluation of Measures for Statistical Fault Localisation and an Optimising Scheme. / Landsberg, David; Chockler, Hana; Kroening, Daniel; Lewis, Matt . Fundamental Approaches to Software Engineering: 18th International Conference, FASE 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. ed. / Alexander Egyed; Ina Schaefer. Vol. 9033 London, UK : Springer International Publishing, 2015. p. 115-129 (Lecture Notes in Computer Science; Vol. 9033).
  • The computational complexity of structure-based causality. / Aleksandrowicz, Gadi; Chockler, Hana; Halpern, Joseph Y.; Ivrii, Alexander. Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence. Vol. 2 Palo Alto, California : AAAI Press, 2014. p. 974-980.
  • Attention-based coverage metrics. / Ben-David, Shoham; Chockler, Hana; Kupferman, Orna. Hardware and Software: Verification and Testing: 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings. ed. / Valeria Bertacco; Axel Legay. Springer International Publishing, 2013. p. 230-245 Lecture Notes in Computer Science  Vol. 8244 LNCS.
  • Improving representative computation in ExpliSAT. / Chockler, Hana; Pidan, Dmitry; Ruah, Sitvanit. Hardware and Software: Verification and Testing: 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings. ed. / Valeria Bertacco; Axel Legay. Springer International Publishing, 2013. p. 359-364 Lecture Notes in Computer Science Vol. 8244 LNCS.
  • Finding rare numerical stability errors in concurrent computations. / Chockler, Hana; Even, Karine; Yahav, Eran. International Symposium on Software Testing and Analysis (ISSTA). ACM, 2013. p. 12-22.
  • Using cross-entropy for satisfiability. / Chockler, Hana; Ivrii, Alexander; Matsliah, Arie; Rollini, Simone Fulvio; Sharygina, Natasha. Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC . ACM, 2013. p. 1196-1203.
  • PINCETTE – Validating Changes and Upgrades in Networked Software. / Chockler, Hana; Denaro, Giovanni; Ling, Meijia; Fedyukovich, Grigory; Hyvärinen, Antti; Mariani, Leonardo; Muhammad, Ali; Oriol, Manuel; Rajan, Ajitha; Sery, Ondrej; Sharygina, Natasha. 17th European Conference on Software Maintenance and Reengineering, CSMR 2013. IEEE Computer Society, 2013. p. 461-464.
  • Computing Interpolants without Proofs. / Chockler, Hana; Ivrii, Alexander; Matsliah, Arie. Hardware and Software: Verification and Testing – 8th International Haifa Verification Conference, HVC 2012. Revised Selected Papers. Vol. 7857 Springer, 2012. p. 72-85 (Lecture Notes in Computer Science).
  • Verification of software changes with ExpliSAT. / Chockler, Hana; Ruah, Sitvanit. International Workshop on Hot Topics in Software Upgrades (HotSWUp). IEEE Computer Society, 2012. p. 31-35.
  • Incremental formal verification of hardware. / Chockler, Hana; Ivrii, Alexander; Matsliah, Arie; Moran, Shiri ; Nevo, Ziv. International Conference on Formal Methods in Computer-Aided Design, FMCAD 2011. p. 135 – 143.
  • Variants of LTL Query Checking. / Chockler, Hana; Gurfinkel, Arie; Strichman, Ofer. Hardware and Software: Verification and Testing: 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers. ed. / S Barner; Harris; D Kroening; O Raz. BERLIN : Springer-Verlag Berlin Heidelberg, 2011. p. 76-92 (Lecture Notes in Computer Science; Vol. 6504).
  • Coverage in interpolation-based model checking. / Chockler, Hana; Kroening, Daniel; Purandare, Mitra. Proceedings of the 47th Design Automation Conference, DAC 2010. ed. New York : ACM, 2010. p. 182-187.
  • Cross-Entropy-Based Replay of Concurrent Programs. / Chockler, Hana; Farchi, Eitan; Godlin, Benny; Novikov, Sergey. Fundamental Approaches to Software Engineering: 12th International Conference, FASE 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. ed. / M Chechik; M Wirsing. BERLIN : Springer-Verlag Berlin Heidelberg, 2009. p. 201-215 (Lecture Notes in Computer Science; Vol. 5503).
  • Explaining Counterexamples Using Causality. / Beer, Ilan; Ben-David, Shoham; Chockler, Hana; Orni, Avigail; Trefler, Richard. Computer aided verification: 21st international conference, CAV 2009, Grenoble, France, June 26 – July 2, 2009 ; proceedings. ed. / A Bouajjani; O Maler. ed. Berlin : Springer-Verlag Berlin Heidelberg, 2009. p. 94-108 (Lecture Notes in Computer Science; Vol. 5643).
  • Beyond Vacuity: Towards the Strongest Passing Formula. / Chockler, Hana; Gurfinkel, Arie; Strichman, Ofer. 2008 Formal Methods in Computer-Aided Design (FMCAD). ed. / A Cimatti; RB Jones. NEW YORK : IEEE, 2008. p. 188-195.
  • Efficient automatic STE refinement using responsibility. / Chockler, Hana; Grumberg, Orna; Yadgar, Avi. Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008, Part of Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, March 29-April 6, 2008. Proceedings. ed. / CR Ramakrishnan; J Rehof. BERLIN : Springer-Verlag Berlin Heidelberg, 2008. p. 233-248 (LECTURE NOTES IN COMPUTER SCIENCE; Vol. 4963).
  • Cross-Entropy Based Testing. / Chockler, Hana; Farchi, Eitan; Godlin, Benny; Novikov, Sergey. Proceedings of Formal Methods in Computer-Aided Design (FMCAD). IEEE Computer Society, 2007. p. 101-108.
  • Easier and More Informative Vacuity Checks. / Chockler, Hana; Strichman, Ofer. Proceedings of ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE). IEEE Computer Society, 2007. p. 189-198.
  • Formal verification of concurrent software: two case studies. / Chockler, Hana; Farchi, Eitan; Glazberg, Ziv; Godlin, Benny; Nir-Buchbinder, Yarden; Rabinovitz, Ishai. Proceedings of the 4th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging (PADTAD). ACM, 2006.
  • Behavioral Compatibility Without State Explosion: Design and Verification of a Component-Based Elevator Control System. / Attie, Paul C.; Lorenz, David H.; Portnova, Alexandra; Chockler, Hana. Proceedings of Component-Based Software Engineering, 9th International Symposium (CBSE). Springer, 2006. p. 33-49 (Lecture Notes in Computer Science; Vol. 4063).
  • Automatic Verification of Fault-Tolerant Register Emulations. / Chockler, Hana; Attie, Paul C. Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY). Vol. 149 1. ed. Electronic Notes in Theoretical Computer Science, 2006. p. 49-60.
  • Temporal Modalities for Concisely Capturing Timing Diagrams. / Chockler, Hana; Fisler, Kathi. Proceedings of Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME. Springer, 2005. p. 176-190 (Lecture Notes in Computer Science; Vol. 3725).
  • Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs. / Chockler, Hana; Attie, Paul C. Proceedings of Verification, Model Checking, and Abstract Interpretation, 6th International Conference (VMCAI). Springer, 2005. p. 465-481 (Lecture Notes in Computer Science; Vol. 3385).
  • Coverage Metrics for Formal Verification. / Chockler, Hana; Kupferman, Orna; Vardi, Moshe Y. Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference (CHARME). Vol. 2860 Italy : Springer, 2003. p. 111-125 (Lecture Notes in Computer Science; Vol. 2860).
  • Responsibility and Blame: A Structural-Model Approach. / Chockler, Hana; Halpern, Joseph Y. IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence. Morgan Kaufmann Publishers Inc., 2003. p. 147-153.
  • Coverage of Implementations by Simulating Specifications. / Chockler, Hana; Kupferman, Orna. Foundations of Information Technology in the Era of Networking and Mobile Computing, IFIP 17th World Computer Congress – TC1 Stream / 2nd IFIP International Conference on Theoretical Computer Science (TCS 2002). Vol. 223 Kluwer Publishing, 2002. p. 409-421.
  • omega-Regular Languages Are Testable with a Constant Number of Queries. / Chockler, Hana; Kupferman, Orna. Randomization and Approximation Techniques, 6th International Workshop (RANDOM). Vol. 2483 Springer, 2002. p. 26-28 (Lecture Notes in Computer Science; Vol. 2483).
  • Coverage Metrics for Temporal Logic Model Checking. / Chockler, Hana; Kupferman, Orna; Vardi, Moshe Y. Proceedings of TACAS. Vol. 2031 Genova, Italy : Springer, 2001. p. 528-542 (Lecture Notes in Computer Science).
  • Which formulae shrink under random restrictions? / Chockler, Hana; Zwick, Uri. Proceedings of the Twelfth Annual Symposium on Discrete Algorithms. ACM-SIAM, 2001. p. 702–708.
  • A Practical Approach to Coverage in Model Checking. / Chockler, Hana; Kupferman, Orna; Kurshan, Robert; Vardi, Moshe Y. Computer Aided Verification, 13th International Conference (CAV). Vol. 2102 Paris : Springer, 2001. p. 66-78 (Lecture Notes in Computer Science; Vol. 2102).

In Archive