Hana Chockler  Hana Chockler photo       

contact information

Research Staff Member
Haifa Research Lab, Haifa, Israel
  +972dash4dash829dash6508

links


more information

More information:  EU FP7 project PINCETTE


2011

Incremental Formal Verification of Hardware
Hana Chockler, Alexander Ivrii, Arie Matsliah, Shiri Moran, Ziv Nevo
FMCAD 2011

Variants of ltl query checking
H Chockler, A Gurfinkel, O Strichman
Hardware and Software: Verification and Testing, 76--92, Springer, 2011


2010

Erratum for “What causes a system to satisfy a specification?”
H Chockler, J Y Halpern, O Kupferman
ACM Transactions on Computational Logic (TOCL) 11(4), 29, ACM, 2010

Coverage in Interpolation-based Model Checking
H Chockler, D Kroening, M Purandare
Proceedings of DAC, 2010


2009


Section 3: Tool Papers

2009 - portal.acm.org


Source Springer-Verlag Berlin, Heidelberg
H Chockler, A J Hu
Proceedings of the 4th International Haifa Verification Conference on Hardware and Software: Verification and Testing, 2009

Before and after vacuity
H Chockler, O Strichman
Formal Methods in System Design 34(1), 37--58, Springer, 2009

Cross-Entropy-Based Replay of Concurrent Programs
H Chockler, E Farchi, B Godlin, S Novikov
Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, pp. 201--215

Explaining counterexamples using causality
I Beer, S Ben-David, H Chockler, A Orni, R Trefler
Computer Aided Verification, pp. 94--108, 2009


2008

Efficient Automatic STE Refinement Using Responsibility
H Chockler, O Grumberg, A Yadgar
Tools and algorithms for the construction and analysis of systems: 14th international conference, TACAS 2008, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008: proceed, pp. 233

Beyond vacuity: Towards the strongest passing formula
H Chockler, A Gurfinkel, O Strichman
Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, pp. 1--8

What causes a system to satisfy a specification?
H Chockler, JY Halpern, O Kupferman
ACM TOCL, 2008


2007

Cross-entropy based testing
H Chockler, E Farchi, B Godlin, S Novikov
Formal Methods in Computer Aided Design, 2007, pp. 101--108

Easier and More Informative Vacuity Checks
H Chockler, O Strichman
Proceedings of MEMOCODE, 2007


2006

Easier and More Informative Vacuity Checks (Full version) Technion
H Chockler, O Strichman
IE Technical-Report TR-07-IEM/ISE-02, 2006

Behavioral Compatibility Without State Explosion: Design and Verification of a Component-Based &
PC Attie, DH Lorenz, A Portnova, H Chockler
Proceedings of CBSE, 2006

Coverage metrics for temporal logic model checking*
H Chockler, O Kupferman, MY Vardi
Formal Methods in System Design, 2006 - Springer

Automatic Verification of Fault-Tolerant Register Emulations
PC Attie, H Chockler
Electronic Notes in Theoretical Computer Science, 2006 - Elsevier

Formal verification of concurrent software: two case studies
H Chockler, E Farchi, Z Glazberg, B Godlin, Y Nir
Proceedings of PADTAD, 2006

Coverage metrics for formal verification
H Chockler, O Kupferman, M Vardi
International Journal on Software Tools for Technology …, 2006 - Springer


2005

Temporal Modalities for Concisely Capturing Timing Diagrams
H Chockler, K Fisler
LECTURE NOTES IN COMPUTER SCIENCE, 2005 - Springer

Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent Programs
PC Attie, H Chockler
Proceedings of VMCAI - Springer, 2005


2004

Efficiently verifiable suficient conditions for deadlockfreedom of large concurrent programs
PC Attie, H Chockler
Technical report, Northeastern University, Boston, MA, 2004. …

A lower bound for testing juntas
H. Chockler, D. Gutfreund
Information Processing Letters 90(6), 301--305, Elsevier, 2004

\omega-Regular languages are testable with a constant number of queries
H Chockler, O Kupferman
Theoretical Computer Science, 2004 - Springer


2003

Coverage metrics for formal verification
H Chockler, O Kupferman, MY Vardi
Proceedings of CHARME, 2003


Responsibility and blame: a structural-model approach
H Chockler, JY Halpern
Arxiv preprint cs/0312038, 2003 - arxiv.org


2002

\omega- Regular Languages Are Testable with a Constant Number of Queries
H Chockler, O Kupferman
Randomization and Approximation Techniques in Computer …, 2002 - books.google.com

Which bases admit non-trivial shrinkage of formulae?
H Chockler, U Zwick
Computational Complexity, 2002 - portal.acm.org

Coverage of Implementations by Simulating Specifications
H Chockler, O Kupferman
Proceedings of the IFIP 17th World Computer Congress-TC1 …, 2002 - portal.acm.org


2001

Which formulae shrink under random restrictions?
H Chockler, U Zwick
Proceedings of the twelfth annual ACM-SIAM symposium on …, 2001 - portal.acm.org

Coverage metrics for temporal logic model checking
MY Vardi, H Chockler, O Kupferman
Proc. of TACAS01, 2001

A Practical Approach to Coverage in Model Checking
H Chockler, O Kupferman, RP Kurshan, MY Vardi
Proceedings of CAV, 2001


Year Unknown

Computing Mutation Coverage in Interpolation-Based Model Checking

Computer-Aided Design ..., 2012 - ieeexplore.ieee.org


PINCETTE—Validating changes and upgrades in networked software
H Chockler
Formal Methods in Computer-Aided Design (FMCAD), 2010, pp. 277--277