The Community for Technology Leaders
2010 8th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010) (2010)
Grenoble
July 26, 2010 to July 28, 2010
ISBN: 978-1-4244-7885-9
TABLE OF CONTENTS

Systematic testing for control applications (PDF)

Rupak Majumdar , UC Los Angeles and MPI-SWS, USA
Indranil Saha , UC Los Angeles, USA
Zilong Wang , Nankai University, China
pp. 1-10

A design flow based on modular refinement (PDF)

Nirav Dave , Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge, 02139, USA
Man Cheuk Ng , Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge, 02139, USA
Michael Pellauer , Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge, 02139, USA
Arvind , Computer Science and Artificial Intelligence Lab, Massachusetts Institute of Technology, Cambridge, 02139, USA
pp. 11-20

Designing application specific circuits with concurrent C# programs (PDF)

David Greaves , Computer Laboratory, University of Cambridge, CB3 0FD, United Kingdom
Satnam Singh , Microsoft Research Cambridge, CB3 0FB, United Kingdom
pp. 21-30

ATLAS: Automatic Term-level abstraction of RTL designs (PDF)

Bryan A. Brady , UC Berkeley, USA
Randal E. Bryant , CMU, USA
Sanjit A. Seshia , UC Berkeley, USA
John W. O'Leary , Intel, USA
pp. 31-40

A flexible schema for generating explanations in lazy theory propagation (PDF)

Roberto Bruttomesso , Università della Svizzera Italiana, Lugano, Switzerland
Edgar Pek , University of Urbana-Champaign, Illinois, USA
Natasha Sharygina , Università della Svizzera Italiana, Lugano, Switzerland
pp. 41-48

Numerical stability analysis of floating-point computations using software model checking (PDF)

Franjo Ivancic , NEC Laboratories America, Princeton, NJ, USA
Malay K. Ganai , NEC Laboratories America, Princeton, NJ, USA
Sriram Sankaranarayanan , University of Colorado at Boulder, USA
Aarti Gupta , NEC Laboratories America, Princeton, NJ, USA
pp. 49-58

Modular verification of synchronization with reentrant locks (PDF)

Tevfik Bultan , Department of Computer Science, University of California, Santa Barbara, USA
Fang Yu , Department of Computer Science, University of California, Santa Barbara, USA
Aysu Betin Can , Informatics Institute, Middle East Technical University, Ankara, Turkey
pp. 59-68

Design contest overview: Combined architecture for network stream categorization and intrusion detection (CANSCID) (PDF)

Michael Pellauer , Massachusetts Institute of Technology, Computation Structures Group, Computer Science and AI Lab, Cambridge, USA
Abhinav Agarwal , Massachusetts Institute of Technology, Computation Structures Group, Computer Science and AI Lab, Cambridge, USA
Asif Khan , Massachusetts Institute of Technology, Computation Structures Group, Computer Science and AI Lab, Cambridge, USA
Man Cheuk Ng , Massachusetts Institute of Technology, Computation Structures Group, Computer Science and AI Lab, Cambridge, USA
Muralidaran Vijayaraghavan , Massachusetts Institute of Technology, Computation Structures Group, Computer Science and AI Lab, Cambridge, USA
Forrest Brewer , University of California, Santa Barbara, High Level Design Group, Electrical and Computer Engineering, USA
Joel Emer , Massachusetts Institute of Technology, Computation Structures Group, Computer Science and AI Lab, Cambridge, USA
pp. 69-72

A regular expression matching using non-deterministic finite automaton (PDF)

Hiroki Nakahara , Kyushu Institute of Technology, Iizuka, Japan
Tsutomu Sasao , Kyushu Institute of Technology, Iizuka, Japan
Munehiro Matsuura , Kyushu Institute of Technology, Iizuka, Japan
pp. 73-76

FPGA-based combined architecture for stream categorization and intrusion detection (PDF)

Sunil Shukla , IBM Research, T.J. Watson Research Center, NY, USA
Rodric Rabbah , IBM Research, T.J. Watson Research Center, NY, USA
Martin Vorbach , PACT XPP Technologies AG, Munich, Germany
pp. 77-80

High-throughput stream categorization and intrusion detection on GPU (PDF)

Mohammad Hassan Khabbazian , Tosan Group, School of Computer Science, Institute for Research in Fundamental Sciences (IPM), Tehran, Iran
Hassan Eslami , Department of Computer Engineering, Sharif University of Technology, Tehran, Iran
Ehsan Totoni , Department of Computer Engineering, Sharif University of Technology, Tehran, Iran
AhmadReza Khadem , Department of Computer Engineering, Sharif University of Technology, Tehran, Iran
pp. 81-84

Using hardware-software codesign language to implement CANSCID (PDF)

Oleg Medvedev , Lanit-Tercom, Saint-Petersburg, Russia
Ilya Posov , Center for informatization of Education “CTE”, Saint-Petersburg, Russia
pp. 85-88

A hardware accelerated system for deep packet inspection (PDF)

Adarsha Rao , Indian Institute of Science, Bangalore, India
Pramod Udupa , Indian Institute of Science, Bangalore, India
pp. 89-92

A high throughput parallel architecture for category specific Deep Packet Inspection (PDF)

Velacheri Jagadeesan Sananda , AMD, Lone Star Design Center, 7171 Southwest Parkway, Austin, Texas, USA
pp. 93-94

CANSCID-CUDA (PDF)

Michael Steffen , Iowa State University, Electrical and Computer Engineering, Ames, USA
Veerendra Allada , Iowa State University, Electrical and Computer Engineering, Ames, USA
Phillip Jones , Iowa State University, Electrical and Computer Engineering, Ames, USA
Joseph Zambreno , Iowa State University, Electrical and Computer Engineering, Ames, USA
pp. 95-98

Team [Ii][Ss][Uu][0–2]{4} design overview: MEMOCODE 2010 design contest (PDF)

Gunjan Pandey , Department of Electrical and Computer Engineering, Iowa State University, Ames, 50010, USA
Sudhanshu Vyas , Department of Electrical and Computer Engineering, Iowa State University, Ames, 50010, USA
Aditya Ashok , Department of Electrical and Computer Engineering, Iowa State University, Ames, 50010, USA
Moinuddin Sayed , Department of Electrical and Computer Engineering, Iowa State University, Ames, 50010, USA
Avinash Srinivasa , Department of Electrical and Computer Engineering, Iowa State University, Ames, 50010, USA
Pooja Mhapsekar , Department of Electrical and Computer Engineering, Iowa State University, Ames, 50010, USA
Adam Jackson , Department of Electrical and Computer Engineering, Iowa State University, Ames, 50010, USA
Matthew Nelson , Department of Electrical and Computer Engineering, Iowa State University, Ames, 50010, USA
Anand Saggi , Department of Electrical and Computer Engineering, Iowa State University, Ames, 50010, USA
Harini Sundararaman , Department of Electrical and Computer Engineering, Iowa State University, Ames, 50010, USA
Phillip H. Jones , Department of Electrical and Computer Engineering, Iowa State University, Ames, 50010, USA
pp. 99-102

Enhancing the assertion-based verification of TLM designs with reentrancy (PDF)

Laurence Pierre , TIMA (CNRS-GrenobleINP-UJF), 46 Av. Félix Viallet - 38031 Grenoble cedex - France
Luca Ferro , TIMA (CNRS-GrenobleINP-UJF), 46 Av. Félix Viallet - 38031 Grenoble cedex - France
pp. 103-112

Proving transaction and system-level properties of untimed SystemC TLM designs (PDF)

Daniel Grosse , Institute of Computer Science, University of Bremen, 28359, Germany
Hoang M. Le , Institute of Computer Science, University of Bremen, 28359, Germany
Rolf Drechsler , Institute of Computer Science, University of Bremen, 28359, Germany
pp. 113-122

Monitoring temporal SystemC properties (PDF)

Deian Tabakov , 6100 Main Str. MS-132, Houston, TX 77005, USA
Moshe Y. Vardi , 6100 Main Str. MS-132, Houston, TX 77005, USA
pp. 123-132

Power emulation: Methodology and applications for HW/SW power optimization (PDF)

J. Haid , Infineon Technologies Austria AG, Design Center Graz, Austria
C. Bachmann , Graz University of Technology, Institute for Technical Informatics, Austria
A. Genser , Graz University of Technology, Institute for Technical Informatics, Austria
C. Steger , Graz University of Technology, Institute for Technical Informatics, Austria
R. Weiss , Graz University of Technology, Institute for Technical Informatics, Austria
pp. 133-138

Understanding loops: The influence of the decomposition of Karp, Miller, and Winograd (PDF)

Alain Darte , Compsys team, LIP, Computer Science Laboratory, UMR 5668 CNRS-ENS Lyon-UCB Lyon-Inria, France
pp. 139-148

Elastic systems (PDF)

Jordi Cortadella , Universitat Politècnica de Catalunya, Barcelona, Spain
Marc Galceran-Oms , Universitat Politècnica de Catalunya, Barcelona, Spain
Mike Kishinevsky , Strategic CAD Lab, Intel Corporation., Hillsboro, OR USA
pp. 149-158

Predictable multithreading of embedded applications using PRET-C (PDF)

Sidharta Andalam , Department of Electrical and Computer Engineering, University of Auckland, New Zealand
Partha Roop , Department of Electrical and Computer Engineering, University of Auckland, New Zealand
Alain Girault , Department of Electrical and Computer Engineering, University of Auckland, New Zealand
pp. 159-168

Feldspar: A domain specific language for digital signal processing algorithms (PDF)

Emil Axelsson , Chalmers University of Technology, Sweden
Koen Claessen , Chalmers University of Technology, Sweden
Gergely Devai , Eötvös Loránd University, Hungary
Zoltan Horvath , Eötvös Loránd University, Hungary
Karin Keijzer , Chalmers University of Technology, Sweden
Bo Lyckegard , Ericsson, Sweden
Anders Persson , Ericsson, Sweden
Mary Sheeran , Chalmers University of Technology, Sweden
Josef Svenningsson , Chalmers University of Technology, Sweden
Andras Vajdax , Ericsson Software Research, Sweden
pp. 169-178

A formal executable semantics of Verilog (PDF)

Patrick Meredith , Department of Computer Science, University of Illinois at Urbana-Champaign, USA
Michael Katelman , Department of Computer Science, University of Illinois at Urbana-Champaign, USA
Jose Meseguer , Department of Computer Science, University of Illinois at Urbana-Champaign, USA
Grigore Rosu , Department of Computer Science, University of Illinois at Urbana-Champaign, USA
pp. 179-188

Minimizing back pressure for latency insensitive system synthesis (PDF)

Bin Xue , FERMAT Lab, Virginia Tech, Blacksburg, USA
Sandeep K. Shukla , FERMAT Lab, Virginia Tech, Blacksburg, USA
S. S. Ravi , Computer Science Department, SUNY Albany, NY, USA
pp. 189-198

LTSs for translation validation of (multi-clocked) SIGNAL specifications (PDF)

Julio C. Peralta , INRIA Centre Rennes-Bretagne Atlantique, IRISA/CNRS, Campus Universitaire de Beaulieu, 35042 Rennes cedex, France
Thierry Gautier , INRIA Centre Rennes-Bretagne Atlantique, IRISA/CNRS, Campus Universitaire de Beaulieu, 35042 Rennes cedex, France
Loic Besnard , INRIA Centre Rennes-Bretagne Atlantique, IRISA/CNRS, Campus Universitaire de Beaulieu, 35042 Rennes cedex, France
Paul Le Guernic , INRIA Centre Rennes-Bretagne Atlantique, IRISA/CNRS, Campus Universitaire de Beaulieu, 35042 Rennes cedex, France
pp. 199-208

Compilation of imperative synchronous programs with refined clocks (PDF)

Mike Gemunde , Embedded Systems Group, Department of Computer Science, University of Kaiserslautern, Germany
Jens Brandt , Embedded Systems Group, Department of Computer Science, University of Kaiserslautern, Germany
Klaus Schneider , Embedded Systems Group, Department of Computer Science, University of Kaiserslautern, Germany
pp. 209-218

Author index (PDF)

pp. 1-2
82 ms
(Ver 3.3 (11022016))