King's College London

Research portal

Research Outputs

  1. 2019
  2. Lattice-based SMT for Program Verification

    Even Mendoza, K., Hyyvarinen, A., Chockler, H. & Sharygina, N., 9 Oct 2019, MEMOCODE 2019 - 17th ACM-IEEE International Conference on Formal Methods and Models for System Design: 17th ACM-IEEE International Conference on Formal Methods and Models for System Design. ACM, A16

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  3. Synthesizing reactive systems using robustness and recovery specifications

    Bloem, R., Chockler, H., Ebrahimi, M. & Strichman, O., 1 Oct 2019, Proceedings of the 19th Conference on Formal Methods in Computer-Aided Design, FMCAD 2019. Barrett, C. & Yang, J. (eds.). Institute of Electrical and Electronics Engineers Inc., p. 147-151 5 p. 8894276

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  4. 2018
  5. Function Summarization Modulo Theories

    Asadi, S., Blicha, M., Fedyukovich, G., Hyyvarinen, A., Even Mendoza, K., Sharygina, N. & Chockler, H., 16 Nov 2018, LPAR-22: 22nd International Conference on Logic for Programming, Articial Intelligence and Reasoning. Vol. 57. p. 56-75 (EPiC Series in Computing).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  6. Lookahead-Based SMT Solving

    Hyyvarinen, A., Marescotti, M., Sadigova, P., Chockler, H. & Sharygina, N., 16 Nov 2018, LPAR-22: LPAR-22: 22ND INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING. EasyChair

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  7. Lattice-Based Refinement in Bounded Model Checking

    Even Mendoza, K., Asadi, S., Hyyvarinen, A., Chockler, H. & Sharygina, N., 18 Jul 2018, Verified Software. Theories, Tools, and Experiments (VSTTE) 2018. Switzerland: Springer, p. 50-68 19 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  8. Timed Vacuity

    Chockler, H., Guha, S. & Kupferman, O., 15 Jul 2018, International Symposium on Formal Methods. Springer, Vol. 10951. p. 438-455 (LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  9. Combining Experts’ Causal Judgments

    Alrajeh, D., Chockler, H. & Halpern, J. Y., 2 Feb 2018, Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence. AAAI Press, p. 6311-6318 9 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  10. 2017
  11. Theory Refinement for Program Verification

    Hyyvarinen, A., Asadi, S., Even Mendoza, K., Fedyukovich, G., Chockler, H. & Sharygina, N., 9 Aug 2017, 20th International Conference on Theory and Applications of Satisfiability Testing (SAT). Springer, Vol. 10491. p. 347-363

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  12. HiFrog: SMT-based Function Summarization for Software Verification

    Alt, L., Asadi, S., Chockler, H., Even Mendoza, K., Fedyukovich, G., Hyvärinen, A. E. J. & Sharygina, N., 24 Apr 2017, 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. Springer, Vol. 10206. p. 207-213 7 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  13. Synthesizing non-vacuous systems

    Bloem, R., Chockler, H., Ebrahimi, M. & Strichman, O., 15 Jan 2017, Proceedings of 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI): Lecture Notes in Computer Science. Springer‐Verlag Berlin Heidelberg, Vol. 10145. p. 55-72 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10145 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  14. 2016
  15. Probabilistic Fault Localisation

    Landsberg, D., Chockler, H. & Kroening, D., 1 Nov 2016, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Hardware and Software: Verification and Testing. Springer‐Verlag Berlin Heidelberg, Vol. 10028 LNCS. p. 65-81 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10028 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  16. Causality and responsibility for formal verification and beyond

    Chockler, H., 26 Aug 2016, Electronic Proceedings in Theoretical Computer Science, EPTCS. Open Publishing Association, Vol. 224. p. 1-8 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  17. 2015
  18. Learning the Language of Error

    Chapman, M., Chockler, H., Kesseli, P., Kroening, D., Strichman, O. & Tautschnig, M., Oct 2015, Proceedings of ATVA 2015: Automated Technology for Verification and Analysis . Springer, Vol. 9364. p. 114-130 18 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  19. Causal Analysis for Attributing Responsibility in Legal Cases

    Chockler, H., Fenton, N., Keppens, J. & Lagnado, D., Jun 2015, ICAIL '15: Proceedings of the 15th International Conference on Artificial Intelligence and Law. ACM Digital Library, p. 33–42 10 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  20. Challenges of existing technology

    Chockler, H., Kroening, D., Mariani, L. & Sharygina, N., 1 Jan 2015, Validation of Evolving Software. Springer International Publishing Switzerland, p. 7-17 11 p.

    Research output: Chapter in Book/Report/Conference proceedingChapter

  21. Complementarities among the technologies presented in the book

    Chockler, H., Kroening, D., Mariani, L. & Sharygina, N., 1 Jan 2015, Validation of Evolving Software. Springer International Publishing Switzerland, p. 19-21 3 p.

    Research output: Chapter in Book/Report/Conference proceedingChapter

  22. Lightweight static analysis check of upgrades in c/c++ software

    Chockler, H. & Ruah, S., 1 Jan 2015, Validation of Evolving Software. Springer International Publishing Switzerland, p. 25-36 12 p.

    Research output: Chapter in Book/Report/Conference proceedingChapter

  23. Evaluation of Measures for Statistical Fault Localisation and an Optimising Scheme

    Landsberg, D., Chockler, H., Kroening, D. & Lewis, M., 2015, 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. Egyed, A. & Schaefer, I. (eds.). London, UK: Springer International Publishing, Vol. 9033. p. 115-129 15 p. (Lecture Notes in Computer Science; vol. 9033).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  24. Science forum: RIPOSTE: a framework for improving the design and analysis of laboratory-based research.

    Masca, N. G. D., Hensor, E. M. A., Cornelius, V. R., Buffa, F. M., Marriott, H. M., Eales, J. M., Messenger, M. P., Anderson, A. E., Boot, C., Bunce, C., Goldin, R. D., Harris, J., Hinchliffe, R. F., Junaid, H., Kingston, S., Martin-Ruiz, C., Nelson, C. P., Peacock, J., Seed, P. T., Shinkins, B. & 4 others, Staples, K. J., Toombs, J., Wright, A. K. A. & Teare, M. D., 2015, eLife. p. e05519 (eLife; vol. 4).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  25. 2014
  26. The computational complexity of structure-based causality

    Aleksandrowicz, G., Chockler, H., Halpern, J. Y. & Ivrii, A., 1 Jan 2014, Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence. Palo Alto, California: AAAI Press, Vol. 2. p. 974-980 7 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  27. 2013
  28. Attention-based coverage metrics

    Ben-David, S., Chockler, H. & Kupferman, O., 1 Dec 2013, Hardware and Software: Verification and Testing: 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings. Bertacco, V. & Legay, A. (eds.). Springer International Publishing, p. 230-245 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8244 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  29. Improving representative computation in ExpliSAT

    Chockler, H., Pidan, D. & Ruah, S., 1 Dec 2013, Hardware and Software: Verification and Testing: 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings. Bertacco, V. & Legay, A. (eds.). Springer International Publishing, p. 359-364 6 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8244 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  30. Finding rare numerical stability errors in concurrent computations

    Chockler, H., Even, K. & Yahav, E., 15 Jul 2013, International Symposium on Software Testing and Analysis (ISSTA). ACM, p. 12-22 11 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  31. Using cross-entropy for satisfiability

    Chockler, H., Ivrii, A., Matsliah, A., Rollini, S. F. & Sharygina, N., 18 Mar 2013, Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC . ACM, p. 1196-1203 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  32. PINCETTE - Validating Changes and Upgrades in Networked Software

    Chockler, H., Denaro, G., Ling, M., Fedyukovich, G., Hyvärinen, A., Mariani, L., Muhammad, A., Oriol, M., Rajan, A., Sery, O. & Sharygina, N., 5 Mar 2013, 17th European Conference on Software Maintenance and Reengineering, CSMR 2013. IEEE Computer Society, p. 461-464 5 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  33. 2012
  34. Computing Interpolants without Proofs

    Chockler, H., Ivrii, A. & Matsliah, A., 6 Nov 2012, Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012. Revised Selected Papers. Springer, Vol. 7857. p. 72-85 14 p. (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  35. Verification of software changes with ExpliSAT

    Chockler, H. & Ruah, S., 3 Jun 2012, International Workshop on Hot Topics in Software Upgrades (HotSWUp). IEEE Computer Society, p. 31-35 5 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  36. 2011
  37. Incremental formal verification of hardware

    Chockler, H., Ivrii, A., Matsliah, A., Moran, S. & Nevo, Z., 2011, International Conference on Formal Methods in Computer-Aided Design, FMCAD 2011: . Boston: FMCAD Inc, p. 135 - 143 19 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  38. Variants of LTL Query Checking

    Chockler, H., Gurfinkel, A. & Strichman, O., 2011, Hardware and Software: Verification and Testing: 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers. Barner, S., Harris, Kroening, D. & Raz, O. (eds.). BERLIN: Springer-Verlag Berlin Heidelberg, p. 76-92 17 p. (Lecture Notes in Computer Science; vol. 6504).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  39. 2010
  40. Coverage in interpolation-based model checking

    Chockler, H., Kroening, D. & Purandare, M., 2010, Proceedings of the 47th Design Automation Conference, DAC 2010. N/A ed. New York: ACM, Vol. N/A. p. 182-187 6 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  41. 2009
  42. Cross-Entropy-Based Replay of Concurrent Programs

    Chockler, H., Farchi, E., Godlin, B. & Novikov, S., 2009, 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. Chechik, M. & Wirsing, M. (eds.). BERLIN: Springer-Verlag Berlin Heidelberg, p. 201-215 15 p. (Lecture Notes in Computer Science; vol. 5503).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  43. Explaining Counterexamples Using Causality

    Beer, I., Ben-David, S., Chockler, H., Orni, A. & Trefler, R., 2009, Computer aided verification: 21st international conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009 ; proceedings. Bouajjani, A. & Maler, O. (eds.). N/A ed. Berlin: Springer-Verlag Berlin Heidelberg, Vol. N/A. p. 94-108 15 p. (Lecture Notes in Computer Science; vol. 5643).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  44. 2008
  45. Beyond Vacuity: Towards the Strongest Passing Formula

    Chockler, H., Gurfinkel, A. & Strichman, O., 2008, 2008 FORMAL METHODS IN COMPUTER-AIDED DESIGN. Cimatti, A. & Jones, RB. (eds.). NEW YORK: IEEE, p. 188-195 8 p.

    Research output: Chapter in Book/Report/Conference proceedingChapter

  46. Efficient automatic STE refinement using responsibility

    Chockler, H., Grumberg, O. & Yadgar, A., 2008, 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. Ramakrishnan, CR. & Rehof, J. (eds.). BERLIN: Springer-Verlag Berlin Heidelberg, p. 233-248 16 p. (LECTURE NOTES IN COMPUTER SCIENCE; vol. 4963).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  47. 2007
  48. Cross-Entropy Based Testing

    Chockler, H., Farchi, E., Godlin, B. & Novikov, S., 11 Nov 2007, Proceedings of Formal Methods in Computer-Aided Design (FMCAD). IEEE Computer Society, p. 101-108 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  49. Easier and More Informative Vacuity Checks

    Chockler, H. & Strichman, O., 30 May 2007, Proceedings of ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE). IEEE Computer Society, p. 189-198 10 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  50. 2006
  51. Formal verification of concurrent software: two case studies

    Chockler, H., Farchi, E., Glazberg, Z., Godlin, B., Nir-Buchbinder, Y. & Rabinovitz, I., 17 Jul 2006, Proceedings of the 4th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging (PADTAD). ACM

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  52. Behavioral Compatibility Without State Explosion: Design and Verification of a Component-Based Elevator Control System

    Attie, P. C., Lorenz, D. H., Portnova, A. & Chockler, H., 29 Jun 2006, Proceedings of Component-Based Software Engineering, 9th International Symposium (CBSE). Springer, p. 33-49 17 p. (Lecture Notes in Computer Science; vol. 4063).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  53. Automatic Verification of Fault-Tolerant Register Emulations

    Chockler, H. & Attie, P. C., 1 Feb 2006, Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY). 1 ed. Electronic Notes in Theoretical Computer Science, Vol. 149. p. 49-60 12 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  54. 2005
  55. Temporal Modalities for Concisely Capturing Timing Diagrams

    Chockler, H. & Fisler, K., 3 Oct 2005, Proceedings of Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME. Springer, p. 176-190 15 p. (Lecture Notes in Computer Science; vol. 3725).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  56. Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs

    Chockler, H. & Attie, P. C., 17 Jan 2005, Proceedings of Verification, Model Checking, and Abstract Interpretation, 6th International Conference (VMCAI). Springer, p. 465-481 17 p. (Lecture Notes in Computer Science; vol. 3385).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  57. 2003
  58. Coverage Metrics for Formal Verification

    Chockler, H., Kupferman, O. & Vardi, M. Y., 2003, Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference (CHARME). Italy: Springer, Vol. 2860. p. 111-125 15 p. (Lecture Notes in Computer Science; vol. 2860).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  59. Responsibility and Blame: A Structural-Model Approach

    Chockler, H. & Halpern, J. Y., 2003, IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence. Morgan Kaufmann Publishers Inc., p. 147-153

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  60. 2002
  61. Coverage of Implementations by Simulating Specifications

    Chockler, H. & Kupferman, O., 2002, 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). Kluwer Publishing, Vol. 223. p. 409-421 13 p.

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  62. omega-Regular Languages Are Testable with a Constant Number of Queries

    Chockler, H. & Kupferman, O., 2002, Randomization and Approximation Techniques, 6th International Workshop (RANDOM). Springer, Vol. 2483. p. 26-28 (Lecture Notes in Computer Science; vol. 2483).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  63. 2001
  64. Coverage Metrics for Temporal Logic Model Checking

    Chockler, H., Kupferman, O. & Vardi, M. Y., Apr 2001, Coverage Metrics for Temporal Logic Model Checking. Genova, Italy: Springer, Vol. 2031. p. 528-542 (Lecture Notes in Computer Science).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  65. Which formulae shrink under random restrictions?

    Chockler, H. & Zwick, U., Jan 2001, Proceedings of the Twelfth Annual Symposium on Discrete Algorithms. ACM-SIAM, p. 702--708

    Research output: Chapter in Book/Report/Conference proceedingConference paper

  66. A Practical Approach to Coverage in Model Checking

    Chockler, H., Kupferman, O., Kurshan, R. & Vardi, M. Y., 2001, Computer Aided Verification, 13th International Conference (CAV). Paris: Springer, Vol. 2102. p. 66-78 (Lecture Notes in Computer Science; vol. 2102).

    Research output: Chapter in Book/Report/Conference proceedingConference paper

Export:RIS BibTex Word PDF - will at most contain 500 items

Refine results Clear filters

Language

Language

Publication year

Publication year

Full text

Full text

Meeting and poster abstracts

© 2018 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454