The tenth MEMOCODE conference will attract researchers and practitioners who create methods, tools, and architectures for the design of hardware/software systems.  These systems face increasing design complexity including tighter constraints on timing, power, costs, and reliability. MEMOCODE seeks submissions that present novel formal methods and design techniques addressing these issues to create, refine, and verify hardware/software systems. We also invite application-oriented papers, and especially encourage submissions that highlight the design perspective of formal methods and models, including success stories and demonstrations of hardware/software codesign. Furthermore, we invite poster presentations describing ongoing work with promising preliminary results..

INVITED TALK Clearing the Clutter: Unified Modeling and Verification Methodology for System Level Hardware Design
The state-of-the-art design practice for complex SoCs employ multiple models of hardware components with different use cases. The cost of building and maintaining those models is high, and verifying the consistency among those models is time consuming. This talk highlights needs and issues of creating these models, and present emerging approaches for developing solutions to address the issues. We also present outstanding problems that the industry needs to address, with a hope that the audience could shed a light on potential solutions to advance the state-of-the-art design and verification methodologies.

SPEAKER Yosinori Watanabe, Cadence Design Systems. Yosinori Watanabe is a senior architect in Cadence Design Systems, engaged in developing design environments, methodologies, and tools for design and verification of embedded systems and their IPs. Before joining Cadence in 1997, he was a member of the ALPHA microprocessor team at Digital Equipment Corporation. Dr. Watanabe received the IEEE Circuits and Systems (CAS) Outstanding Young Author Award and the IEEE CAS Best Paper Award on Transactions of Computer-Aided Design in 1995 and 1998, respectively. He holds a Ph.D. in electrical engineering and computer sciences from the University of California, Berkeley.

INVITED TALK Pioneering the Future of Design and Verification: A Spiral of Technological and Business Innovation
Changing the way the world designs and verifies semiconductors and systems takes far more than algorithmic or methodological breakthroughs. Over the past two decades, there have been four or five great verification breakthroughs, while many other promising technologies have been relegated to the dust bin. Bringing a nascent EDA technology to mainstream use and commercial success requires alternating technological and business innovations to accelerate adoption. In this session, you'll learn key concepts about bringing a disruptive technology to widespread adoption. Kathryn Kranen will share insights gained as a market pioneer of three technologies that have become the major pillars of today's mainstream system-on-chip design and verification: hardware emulation, constrained-random simulation, and formal property verification. You will also hear some of her visions of what the future of design and verification may hold.

SPEAKER Kathryn Kranen, President and Chief Executive Officer, Jasper Design Automation. Kathryn Kranen is responsible for leading Jasper┬╣s team in successfully bringing the company┬╣s pioneering technology to the mainstream design verification market. She has more than 20 years EDA industry experience and a proven management track record. While serving as president and CEO of Verisity Design, Inc., US headquarters of Verisity Ltd., Kathryn and the team she built created an entirely new market in design verification. (Verisity later became a public company, and was the top-performing IPO of 2001.) Prior to Verisity, Kathryn was vice president of North American sales at Quickturn Systems. She started her career as a design engineer at Rockwell International, and later joined Daisy Systems, an early EDA company. Kathryn graduated Summa cum Laude from Texas A&M University with a B.S. in Electrical Engineering. Kathryn is serving her fifth term on the EDA Consortium board of directors, and was elected its vice chairperson. In 2005, Kathryn was recipient of the prestigious Marie R. Pistilli Women in Electronic Design Automation (EDA) Achievement Award. In 2009, EE Times listed Kathryn as one of the "Top 10 Women in Microelectronics".

INVITED TALK Symbolic Tools for Program Proving
I'll argue that purely symbolic logical tools can be as efficient in practice as specialized program verification tools based on program control flow representations. In particular, many inference problems in program verification, such as synthesis of loop invariants, procedure summaries, refinement types and modular concurrent proofs can be reduced to solving symbolically for relational fixed points. A generic solver can produce all of these artifacts, given a verification condition generator for the given programming language and proof system. This generality comes at little cost in performance. In fact, significant performance gains can be achieved in practice, as re-use justifies the effort of heavily optimizing the implementation, a phenomenon we have observed in other generic engines such as SAT and SMT solvers, and BDD packages. This talk describes joint work with Andrey Rybalchencko and Nikolaj Bjorner.

SPEAKER Kenneth Mc Millan, Microsoft Research. I started out as an electrical engineer, designing chips and biomedical instruments. My undergraduate degree is in EE, from the University of Illinois, and I also have an MSEE from Stanford. This experience got me interested in the process of designing complex systems, and in particular, how we determine that complex system designs are correct. I switched to computer science, doing my Ph.D. with Ed Clarke at CMU, graduating in 1992. My thesis was on a technique called Symbolic Model Checking that could be used to verify logical properties of finite-state systems by efficiently exploring very large state spaces. I developed a model checker called SMV that implemented these techniques, as well as other techniques for combatting the so-called state explosion problem. I went on to do research at Bell Labs, Cadence Berkeley Labs, and now (as of 2010) Microsoft Research. At Cadence, I further developed SMV, incorporating methods of compositionality and abstraction to break large verification problems down into small ones in a tool called Cadence SMV. More recently, I've been mainly interested in the question of relevance. That is, if you want to prove a logical property of a complex object like an computer program or a hardware design, how do you decide what information about that system is relevant to that property? This lead to a technique called Craig interpolation that allows us to use logical proof as a basis for relevance, and can be used as the foundation of formal verification tools for hardware and software.

TUTORIAL Incremental Inductive Verification: IC3 and its Friends.

SPEAKER Fabio Somenzi, University of Colorado at Boulder. Fabio Somenzi received the Dr. Eng. degree from Politecnico di Torino in 1980. He was with ST Microelectronics until 1989, when he joined the University of Colorado at Boulder. His research interests revolve around model checking, synthesis, decision diagrams, and decision procedures.