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 Senior 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. For 10 years Limor led 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 more than 30 papers, and she was invited to many technical program committees of leading international conferences. In the last seven years, Limor served 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. In 2008, Limor served as the general chair of DAC.

Limor's research interests include formal specification languages, Limor has led the development of the ForSpec formal specification language 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 led 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

Chapter on Formal Verification in "Electronic Design Automation for Integrated Circuits handbook - EDA for IC Implementation, Circuit Design, and Process Technology", Edited by L. Scheffer, L. Lavango, and G. Martin. 2006 CRC.

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

V. Liaskovitis, S. Chen, P.B. Gibbons, A. Ailamaki, G.E. Blelloch, B. Falsafi, L. Fix, N. Hardavellas, M. Kozuch, T. Mowry, C. Wilkerson. "Brief announcement: Parallel Depth First vs. Work Stealing schedulers on CMP Architectures". 18th ACM Sym. On Parallelism in Algorithms and Architectures, Cambridge, MA USA July 2006.

L. Fix, T. Heyman, M. Vardi, R. Armoni, Y. Zbar, Yakir, "verifying Industrial Circuits Achieving Bound 1000 and Beyond", ASP-DAC 2007

S. Chen, P.B. Gibbons, M. Kozuch, V. Liaskovitis, A. Ailamaki, G.E. Blelloch, B. Falsafi, L. Fix, N. Hardavellas, T. Mowry, C. Wilkerson. "Scheduling Threads for Constructive Cache Sharing on CMPs". In Proc. Of the 19th ACM SPAA, San Diego, CA, June 2007.

S. Chen, B. Falsafi, P.B. Gibbons, M. Kozuch, T.C. Mowry, R. Teodorescu, A. Ailamaki, L. Fix, G.R. Ganger, B. Lin and S.W. Schlosser. "Log-based Architecture for General-Purpose Monitoring of Deployed Code". In Proc. of the ACM Workshop ASID, San Jose, CA, Oct 2006. Held in conjunction with ACM ASPLOS'06.

A. Goode, M. Chen, A. Tarachandani, L. Mummert, R. Sukthankar, C. Helfrich, A. Stefanni, L. Fix, J. Saltzman, M. Satyanarayanan. "Interactive Search of Adipocytes in Large Collections of Digital Cellular Images." Proceedings of International Conference on Multimedia and Expo, 2007.

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.

Limor Fix, Orna Grumberg, Tamir Heyman, Assaf Schuster, "Verifying very large industrial circuits using 100 processes and beyond", vol. 18, num. 1, pp. 45-62, Feb. 2007.

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

P. Chatterjee, L. Fix, L. Loh, J. Michelson, "Deploying Formal: When and Where?", DAC'2007 Pavilion Panel.

DVCON Verification panel - 2008

DAC 2008 Pavilion Panel

DAC 2008 Marketing Forum Panel

International Conference Program & Executive Committees


CAV97, CAV98, FMACD98, CAV99, DAC00, FMCAD00, DAC01, DAC02, DATE02, DAC03, DATE03, CHARME03, DAC04, Isola04, DAC05-09, TACAS07, DATE07, VMCAI07, CAV07, HVC07, ICINCO08, FV09