2. MEMOCODE 2004: San Diego, California, USA

Keynote Talk I

• Randal E. Bryant:
  System modeling and verification with UCLID. 3-4
  

Model Checking

• Himanshu Jain, Daniel Kroening, Edmund M. Clarke:
  Verification of SpecC using predicate abstraction. 7-16
  
• Tobias Schüle, Klaus Schneider:
  Bounded model checking of infinite state systems: exploiting the automata hierarchy. 17-26
  
• Ahmed Sobeih, Mahesh Viswanathan, Jennifer C. Hou:
  Check and simulate: a case for incorporating model checking in network simulation. 27-36
  

Modeling Languages

• Olivier Tardieu, Robert de Simone:
  Curing schizophrenia by program rewriting in Esterel. 39-48
  
• Grace Nordin, James C. Hoe:
  Synchronous extensions to operation centric hardware description languages. 49-56
  
• Christel Baier, Frank Ciesinski, Marcus Größer:
  PROBMELA: a modeling language for communicating probabilistic processes. 57-66
  

Tutorial

• Rishiyur S. Nikhil:
  Bluespec System Verilog: efficient, correct RTL from high level specifications. 69-70
  

Synthesis

• Ralph D. Jeffords, Elizabeth I. Leonard:
  Using invariants to optimize formal specifications before code synthesis. 73-82
  
• Dag Björklund:
  Efficient code synthesis from synchronous dataflow graphs. 83-92
  
• Nirav Dave:
  Designing a reorder buffer in Bluespec. 93-102
  

Keynote Talk II

• David L. Dill:
  The battle of accountable voting systems. 105
  

Formal Verification

• Cagkan Erbas, Selin C. Erbas, Andy D. Pimentel:
  Static priority scheduling of event triggered real time embedded systems. 109-118
  
• Bhaskar Pal, Ansuman Banerjee, Pallab Dasgupta, P. P. Chakrabarti:
  The BUSpec platform for automated generation of verification aids for standard bus protocols. 119-128
  
• Krishnamani Kalyanasundaram, R. K. Shyamasundar:
  Formal verification of pipelined processors with precise exceptions. 129-139
  

Panel

• Brian Bailey:
  Is formal being squeezed out of functional verification? 143
  
• Gerard J. Holzmann:
  Formal methods and software reliability. 145-146
  
• Robert P. Kurshan:
  Formal verification as a technology transfer problem. 147-150
  
• Vladimir Levin:
  Static driver verifier, a formal verification tool for Windows device drivers. 151
  
• John O'Leary:
  Formal verification in Intel CPU design. 152
  
• Carl Pixley, D. Meyers, S. McMaster, A. Chittor:
  Designers want proofs - but show me the money. 153-154
  
• Sandeep K. Shukla, Tevfik Bultan, Constance L. Heitmeyer:
  Panel: given that hardware verification has been an uphill battle, what is the future of software verification? 157-158
  

Keynote Talk III

• Edward A. Lee, Stephen Neuendorffer:
  Classes and subclasses in actor-oriented design. 161-168
  

Simulation and Testing

• Daniel Große, Rolf Drechsler:
  Checkers for SystemC designs. 171-178
  
• Stephen Neuendorffer, Edward A. Lee:
  Hierarchical reconfiguration of dataflow models. 179-188
  
• Daniel L. Rosenband:
  The ephemeral history register: flexible scheduling for rule-based designs. 189-198
  

Compositional Verification

• Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina:
  Automated, compositional and iterative deadlock detection. 201-210
  
• Christoph Sprenger, Dilian Gurov, Marieke Huisman:
  Compositional verification for secure loading of smart card applets. 211-222
  
• Yamine Aït Ameur, Remi Delmas, Virginie Wiels:
  A framework for heterogeneous formal modeling and compositional verification of avionics systems. 223-232
  

Last update Tue May 21 17:43:33 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page