Validation of
Optimizing Compilers,
L. Zuck, A. Pnueli, and R. Leviahtan.
Weizmann Institute of Science Technical Report MCS01-12, August 2001.
VOC: A Translation
Validator for Optimizing Compilers,
L. Zuck, A. Pnueli, Y.Fang, and B. Goldberg.
(COCV'02, 2002.)
VOC: A Methodology for
Translation Validation of Optimizing Compilers,
L. Zuck, A. Pnueli, Y.Fang, and B. Goldberg.
(Journal of Universal Computer Science 9(3))
Translation
and Run-Time Validation for Optimized Code,
L. Zuck, A. Pnueli, Y.Fang, B. Goldberg, and Y.Hu.
(RV 2002.)
Translation
and Run-Time Validation for Optimized Code,
L. Zuck, A. Pnueli, B. Goldberg, C. Barrett, Y.Fang, and Y.Hu.
(To Appear in Journal of Formal Methods in System Design )
Run-Time of Speculative
Optimizations using CVC,
C. Barrett, B. Goldberg, and L. Zuck
(RV 2003.)
Into the Loops
,
B. Goldberg, L. Zuck, and C. Barrett
(COCV 2004.)
TVOC: A Translation
Validator for Optimizing Compilers ,
C. Barrett, Y. Fang,
Y. Hu, B. Goldberg, A. Pnueli, and L. D. Zuck
(CAV
2005.)
Generating Invariants
for Translation Validation,
Y. Fand and L. Zuck
(COCV
2006.)
Formal Verification
of Backward Compatibility of Microcode
T. Arons, E. Elster,
L. Fix, S. Mador-Haim, M. Mishaeli, J. Shalev, E. Singerman,
A. Tiemeyer, M. Y. Vardi, and L. D. Zuck, ``L. Zuck
(CAV
2005.)
Formal Analysis of Security
Protocols
The Faithfulness of Abstract
Protocol Analysis: Message Authentication,
J. D. Guttman, J. Thayer, and L.D. Zuck
(ACM CCS-8.)
Final version appean in Journal of Computer Security 2004
Automatic Deductive Verification
with Invisible Invariants,
A. Pnueli, S. Ruah, and L. Zuck
(TACAS 2001.)
Parameterized Verification with Automatically Computed Inductive Assertions
,
T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck.
(CAV 2001).
Liveness with (0,1,infinity)-Counter Abstraction,
A. Pnueli, J. Xu, and L. Zuck.
(CAV02).
Run-Time Results
Network Invariants in Action,
Y. Kesten, A. Pnueli, E. Shahar, and L. Zuck.
(CONCUR02).
Model Checking and Abstraction to the Aid of Parameterized
Systems,
L. Zuck and A. Pnueli
(Computer Lanugages,
Systems, and Structures, 30(3-4). 2004).
Liveness with Invisible Ranking,
Yi Fang, Nir Piterman, A. Pnueli and L. Zuck.
(VMCAI'04).
Run-Time Results
Liveness with Incomprehensible Ranking,
Yi Fang, Nir Piterman, A. Pnueli and L. Zuck.
(TACAS'04).
Run-Time Results
IIV: An Invisible Invariant Verifier,
I.~Balaban, Y.~Fang,
A.~Pnueli, and L.~D.~Zuck
(CAV 2005)
Invisible Safety of Distributed Protocols,
I.~Balaban,
A.~Pnueli, and L.~D.~Zuck
(ICALP 2006)
Livness by Invisible Invariants,
Y.~Fang, K.~McMillan,
A.~Pnueli, and L.~D.~Zuck
(FORTE 2006)
Automatic Verification of Probabilistic Free Choice
L. Zuck, A. Pnueli, and Yonit Kesten
(VMCAI 2002.)
Automatic Verification by Probabilistic Abstraction
T. Arons, L. Zuck, A. and Pnueli
(FOSSACS 2003.)
Run-Time Results
Taming Specifications
T. Margaria, A. P. Sistla, B. Steffen,
and L. Zuck,
(CONCUR 2005.)
Monitoring Off-the-Shelf Componenets
P. Sistla, M. Zhou, and
L. Zuck,
(VMCAI 2006.)
Monitoring Interfaces for Faults
Amir Pnueli, Aleksandr Zaks, Lenore Zuck
(ENTCS
2006)
Model Checking/Ranking/Shape
Analysis
From Model Checking to a Temporal Proof,
D. Peled and L. Zuck
(SPIN 2001).
From Falsification to
Verification,
D. Peled, A. Pnueli, and L. Zuck
(FSTTCS
2001.)
Shape Analysis by
Predicate Abstraction,
I. Balaban, A. Pnueli, and L. Zuck
(VMCAI 2005.)
Ranking Abstraction
as Companion to Predicate Abstraction,
I. Balaban, A. Pnueli,
and L. Zuck
(FORTE 2005.)