Books
A Practical Introduction to PSL (errata)
Referreed publications
Structural Contradictions
C. Eisner, D. Fisman Proc. Fourth International Haifa Verification Conference (HVC), to appear LNCS. Springer 2008.
Augmenting a Regular Expression-Based Temporal Logic with Local Variables
C. Eisner, D. Fisman Proc. 8th International Conference on Formal Methods in Computer Aided Design (FMCAD). IEEE 2008.
Functional Verification of Power Gated Designs by Compositional Reasoning
C. Eisner, A. Nahir, K. Yorav Proc. 20th International Conference on Computer Aided Verification (CAV), LNCS 5123. Springer 2008.
Policy Verification for System Automation with Model Checking: A Case Study
E. Zarpas, C. Eisner, S. Tal Proc. 9th IEEE Workshop on Policies for Distributed Systems and Networks, IEEE Computer Society, 2008.
GateAlert: A Clock Gating Tool
E. Arbel, C. Eisner, I. Itskovich
In Proc. 5th Annual Austin Conference on Energy-Efficient Design (ACEED), March 2007.
ExpliSAT: Guiding SAT-Based Software Verification with Explicit States
S. Barner, C. Eisner, Z. Glazberg, D. Kroening, I. Rabinovitz
In Proc. Second International Haifa Verification Conference (HVC), LNCS 4383, pp. 138-154, October 2006.
A Topological Characterization of Weakness
C. Eisner, D. Fisman, J. Havlicek
In Proc. 24th Annual ACM Symposium on Principles of Distributed Computing (PODC), pp. 1-8, July 2005.
Formal Verification of Software Source Code Through Semi-Automatic Modeling
C. Eisner
Software and Systems Modeling (SOSYM). Volume 4, Number 1, February 2005.
Reasoning with Temporal Logic on Truncated Paths
C. Eisner, D. Fisman, J. Havlicek, Y. Lustig, A. McIsaac and D. Van Campenhout
In Proc. 15th International Conference on Computer-Aided Verification (CAV), LNCS 2725, pp.27-39, July 2003.
The Definition of a Temporal Clock Operator
C. Eisner, D. Fisman, J. Havlicek, A. McIsaac and D. Van Campenhout
In Proc. 30th International Colloquium on Automata, Languages and Programming (ICALP), LNCS 2719, Springer, 2003.
Using Symbolic CTL Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard
C. Eisner
International Journal on Software Tools for Technology Transfer (STTT), Volume 4, Number 1, Springer, 2002.
Model checking the garbage collection mechanism of SMV
C. Eisner
In Electronic Notes in Theoretical Computer Science, Volume 55, Number 3, Elsevier Science Publishers, 2001.
The Temporal Logic Sugar
I. Beer, S. Ben-David, C. Eisner, D. Fisman, A. Gringauze and Y. Rodeh
In Proc. 13th International Conference on Computer Aided Verification (CAV), LNCS 2101, Springer, 2001.
Efficient Detection of Vacuity in Temporal Model Checking
I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh
Formal Methods in System Design, Volume 18, Number 2, Kluwer Academic Publishers, 2001.
A Methodology for Formal Design of Hardware Control with Application to Cache Coherence Protocols
C. Eisner, R. Hoover, W. Nation, K. Nelson, I. Shitsevalov, and K. Valk
In Proc. 37th Design Automation Conference (DAC), Association for Computing Machinery, Inc., June 2000.
Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard
C. Eisner
In Proc. 10th IFIP WG10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), LNCS 1703, Springer, 1999.
Efficient Detection of Vacuity in ACTL Formulas
I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh
In Proc. 9th International Conference on Computer Aided Verification (CAV), LNCS 1254, Springer, 1997.
RuleBase: Model Checking at IBM
I. Beer, S. Ben-David, C. Eisner, D. Geist, L. Gluhovsky, T. Heyman, A. Landver, P. Paanah, Y. Rodeh, G. Ronin, and Y. Wolfsthal
In Proc. 9th International Conference on Computer Aided Verification (CAV), LNCS 1254, Springer, 1997.
RuleBase: an Industry Oriented Formal Verification Tool
I. Beer, S. Ben-David, C. Eisner, and A. Landver
In Proc. 33rd Design Automation Conference (DAC), Association for Computing Machinery, Inc., June 1996.
Invited papers
PSL for Runtime Verification: Theory and Practice
C. Eisner
In Proc. 7th Workshop on Runtime Verification (RV), LNCS 4839, 2007.
Model Checking at IBM
S. Ben-David, C. Eisner, D. Geist and Y. Wolfsthal
Formal Methods in System Design, Volume 22, Number 2, Kluwer Academic Publishers, 2003.
Comparing Symbolic and Explicit Model Checking of a Software System
C. Eisner and D. Peled
In Proc. 9th International SPIN Workshop on Model Checking of Software (SPIN), LNCS 2318, Springer, 2002.
On the Effective Deployment of Functional Formal Verification
Y. Abarbanel-Vinov, N. Aizenbud-Reshef, I. Beer, C. Eisner, D. Geist, T. Heyman, I. Reuveni, E. Rippel, I. Shitsevalov, Y. Wolfsthal and T. Yatzkar-Haham
Formal Methods in System Design, Volume 19, Number 1, Kluwer Academic Publishers, 2001.
Other
Proposed New Appendix B for IEEE 1850 (PSL)
J C. Eisner, D. Fisman
IBM Technical Report H-0261, 2008.
The \top,\bot approach for truncated semantics
J C. Eisner, D. Fisman, J. Havlicek and J. Martensson
Accellera Technical Report 2006.01, May 2006.
Basic Results on the Semantics of Accellera PSL 1.1 Foundation Language
J J. Havlicek, D. Fisman and C. Eisner
Accellera Technical Report 2004.02, May 2004.
Sugar 2.0
C. Eisner and D. Fisman
Proposal Presented to the Accellera Formal Verification Technical Committee, March 2002.
IBM publications
S Barner, Cindy Eisner, Z Glazberg, D Kroening and I Rabinovitz. ExpliSAT: Guiding SAT-Based Software Verification with Explicit States. HVC 2006. October 2006.