Limor Fix limor dot fix at intel dot com 4720 Forbes Ave. Suite 410 Pittsburgh, PA 15213 (412) 297-4100 (412) 297-4110 (fax)

Currently Limor is co-managing the Intel Pittsburgh Lab as the Associate Director of the Lab. Limor is also an Intel Principal Engineer and she has a PhD in Computer Science from the Technion, Israel,1992. After graduation, Limor conducted post-doc research in Cornell university and in 1994 she joined Intel in Israel. In the past 10 years Limor has lead a major change in Intel s validation technology and methodology. She developed innovative formal verification tools and methodology that have been widely adopted by Intel s design teams. Limor has published 25 papers, and she was invited to more than 15 technical program committees of leading international conferences. In the last three years Limor in on the executive committee of the Design Automation Conference (DAC), the leading conference for design tools with 10,000 participants and 250 companies demo suites.

Limor's research interests include formal specification langauges, Limor has lead the development of the ForSpec formal specification langauge that had been donated by Intel to Accellera/IEEE and had a major impact in the IEEE-1850 standard. In addition, Limor's research also include BDD's, SAT solvers, and model checking of both hardware and distributed software. In particular, Limor has lead the research and development of Intel's three generations of advanced formal verification systems, Forecast, Thunder and Foresight.

Books

L. Fix, I. Getreu, L. Lavango (eds.): Proceedings of the 40th Design Automation Conference, DAC 2003, LA, CA, USA, June 2003, ACM2003.

S. Malik, L. Fix, A.B. Kahng (eds.): Proceedings of the 41th Design Automation Conference, DAC 2004, San Diego, CA, USA, June 7-11, 2004, ACM2004

EDA-Handbook. To be published early 2006.

Conferences and Technical reports:

L. Fix, N. Francez, O. Grumberg: ``Semantics-driven decompositions for the verification of distributed programs'', IFIP TC2 Working Conference on Programming Concepts and Methods, See Galilee, Israel, April 1990.

L. Fix, N. Francez, O. Grumberg: ``Program Composition and Modular Verification'', Proc. 18th ICALP, Madrid, July 1991. LNCS 510 J. Leach Albert. B. Monien, M. Rodriguez Artalejo (Eds.), Springer-Verlag.

L. Fix, N. Francez, O. Grumberg: ``Program composition via unification'', Proc. 19h ICALP, Wien, July 1992. LNCS 623 W. Kuich (Ed.), Springer-Verlag.

L. Fix and O. Grumberg: ``Verification of Temporal Properties'', TR 93-1368 Aug. 1993, CS Cornell Univ.

L. Fix, F.B. Schneider: ``Reasoning about programs by exploiting the environment'', ICALP'94. Also TR-94-1409 Feb 10994, CS Cornell Univ.

L. Fix, T.A. Henzinger: ``The most abstract common refinement'', TR 1994, CS Cornell Univ.

R. Alur, L. Fix, T.A. Henzinger: ``A determinizable class of timed automata'', 6th International Conference, CAV'94, Stanford, California, USA, June 1994, pp. 1-13, LNCS 818. David L. Dill (Ed.) Springer-Verlag.

L. Fix, F.B. Schneider: ``Hybrid Verification by Exploiting the Environment'', 3rd. International School and Symposium: Formal Techniques in Real Time and Fault Tolerant Systems, Sep. 1994, LNCS 863, pp. 1-18, Springer-Verlag, Schleswig (Kiel), Germany. Also, TR 94-1436 Cornell Univ.

G. Kamhi, O. Weissberg, L. Fix, Z. Binyamini, Z. Shtadler: "Automatic data-path extraction for efficient usage of HDD", 9th International Conference, CAV'97, pp. 95-106 LNCS 1254, Springer.

G. Kamhi, L. Fix: "Adaptive variable reordering for symbolic model checking", IEEE/ACM International Conference on Computer Aided Design (ICCAD) 1998.

G. Kamhi, L. Fix, Z. Binyamini: "Symbolic Model Checking visualization", Second International Conference on Formal Methods in Computer-Aided Design (FMCAD) 1998.

S. Mador-Haim, L. Fix: "Inputs elimination and data abstraction in model checking", Second International Conference on Formal Methods in Computer-Aided Design (FMCAD) 1998.

Ranan Fraer, Gila Kamhi, Limor Fix, Moshe Vardi: "Evaluating Semi-Exhaustive Verification Techniques for Bug Hunting" SMC, 1999 (CAV'99 workshop).

Ranan Fraer, Gila Kamhi, Barukh Ziv, Moshe Y. Vardi, Limor Fix: "Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification", CAV 2000.

Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchilia, Gila Kamhi, Armando Tacchella, Moshe Vardi: "Benefits of Bounded Model Checking at an Industrial Settings", CAV2001, LNCS 2102.

Scott Hazelhurst, Osnat Wiessberg, Gila Kamhi, Limor Fix: "A hybrid verification approach: getting deep into the design" DAC 2002.

R. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, E. Singerman, A. Tiemeyer, M. Vardi, Y. Zbar: The ForSpec temporal Logic: A new Temporal Property Specification Language". TACAS 2002, 296-311.

R. Armoni, L. Fix, A. Flaisher, O. Grumberg, N. Piterman, A. Tiemeyer, M. Vardi: "Enhanced Vacuity Detection in Linear Temporal Logic", CAV 2003, 368-380

P. Basu, S. Das, P. Dasgupta, P.p. Chakrabarti, C.R. Mohan, L. Fix, "Formal Verification Coverage: are the RTL-properties covering the design's architectural intent. DATE 2004, 668-669.

P. Basu, S. Das, P. Dasgupta, P.p. Chakrabarti, C.R. Mohan, L. Fix: "Formal Verification Coverage: Computing the coverage gap between temporal specifications", ICCAD'2004

R. Armoni, L. Fix, R. Fraer, S. Huddleston, N. Piterman, M. Vardi: "SAT-based induction for temporal safety properties", BMC workshop at CAV'04

P. Basu, S. Das, P. Dasgupta, P.p. Chakrabarti, C.R. Mohan, L. Fix, "Formal methods for analyzing the completeness of assertions suite against a high level fault model". VLSI Design'2005 conference at Kokata.

T. Arons, E. Elster, L. Fix, S. Mador-Haim, M. Mishaeli, J. Shalev, E. Singerman, A. Tiemeyer, M. Vardi, L. Zuck, Formal Verification of Backward compatibility of Microcode , 17th International Conference on Computer Aided Verification, July 2005, Edinburgh.

L. Fix, O. Grumberg, T. Heyman, A. Schuster, Verifying very large industrial circuits using 100 processes and beyond , Third International Symposium on Automated Technology for Verification and Analysis, Oct 2005

JOURNAL papers and articles

L. Fix, N. Francez, O. Grumberg: ``Program composition via unification'', Theoretical Computer Science 131 (1994) 139-179.

L. Fix, N. Francez, O. Grumberg: ``Program Composition and Modular Verification'', Distributed Computing.

L. Fix, O. Grumberg: ``Verification of temporal properties'', Journal of Logic and Computation 6(3): 343-361, 1996.

L. Fix, F.B. Schneider: ``Reasoning about programs by exploiting the environment'', Submitted to Formal Aspects of Computing, The International journal of Formal Methods.

R. Alur, L. Fix, T. Henzinger: "Event-Clock Automata: A determinizable class of timed automata", Theoretical Computer Science 211(1-2): 253-273, 1999.

R. Fraer, G. Kamhi, L. Fix, M. Vardi: "Evaluating Semi-Exhaustive Verification Techniques for Bug Hunting." Ele. Notes Theo. Computer Science 23(2) 1999.

L. Fix, L. Lavango: "DAC Highlights", Design &Test May/June 2003 (Vol. 20, no 3).

L. Fix: "Formal Property Verification For All", Design & Elektronik, Electronik I Norden, 2004

P. Basu, S. Das, A. Banerjee, P. Dasgupta, P.P. Chakrabarti, C.R. Mohan, L. Fix, R. Armoni. Design Intent Coverage -- A new paradigm for Formal Property Verification , IEEE Transaction on CAD, 2005.

Invited panels and talks

L. Fix, "Hardware Formal Verification: achievements and open problem", Workshop on Formal Design of Safety Critical Embedded Systems, Munich, Germany 1999.

L. Fix, "Hardware Verification", IJCAR 2001.

L. Fix, "Hardware Formal Verification", Shamir seminar, Jerusalem, Israel, 2002.

D. Dill, N. Janes, S. Rawat, G. Berry, L. Fix, H. Foster, R. Ranjan, G. Stalmarck, C. Widdoes, Panel on "Formal Verification Methods: getting around the brick wall". DAC 2002, 576-577.

B. Cook, L. Fix, Y. Wolfsthal, Panel on Industrial used of formal methods , IsoLA 2004.

A. Piziali, K. Normoyle, L. Fix, H. Foster, G. Smith, Panel on Designing Quality In: The Better Design Paradigm , DVCon 2005

International Conference Program & Executive Committees

CAV97, CAV98, FMACD98, CAV99, DAC00, FMCAD00, DAC01, DAC02, DATE02, DAC03, DATE03, CHARME03, DAC04, Isola04, DAC05