3. MEMOCODE 2005: Verona, Italy

Keynote Talk I

• Nicolas Halbwachs:
  A synchronous language at work: the story of Lustre. 3-11
  

Hardware Synthesis

• Michael Pellauer, Mieszko Lis, Don Baltus, Rishiyur S. Nikhil:
  Synthesis of synchronous assertions with guarded atomic actions. 15-24
  
• Nirav Dave, Man Cheuk Ng, Arvind:
  Automatic synthesis of cache-coherence protocol processors using Bluespec. 25-34
  

Hardware Languages and Semantics

• Stephen A. Edwards, Olivier Tardieu:
  Deterministic receptive processes are Kahn processes. 37-44
  
• Shuqing Zhao, Daniel D. Gajski:
  Structural operational semantics for supporting multi-cycle operations in RTL HDLs. 45-53
  
• Greg Hoover, Forrest Brewer:
  PyPBS design and methodologies. 55-64
  

Invited Tutorial

• Myla Archer:
  Making PVS do what you want. 67
  

Keynote Talk II

• Daniel Gajski:
  System design extreme makeover. 71-75
  

Software Verification

• Tuba Yavuz-Kahveci, Tevfik Bultan:
  Verification of parameterized hierarchical state machines using action language verifier. 79-88
  
• Jan Jürjens:
  Verification of low-level crypto-protocol implementations using automated theorem proving. 89-98
  

System-Level Verification

• Daniel Kroening, Natasha Sharygina:
  Formal verification of SystemC by automatic hardware/software partitioning. 101-110
  
• Fei Xie, Xiaoyu Song, Haera Chung, Ranajoy Nandi:
  Translation-based co-verification. 111-120
  
• Thanyapat Sakunkonchak, Satoshi Komatsu, Masahiro Fujita:
  Synchronization verification in system-level design with ILP solvers. 121-130
  
• Nicolae Savoiu, Sandeep K. Shukla, Rajesh K. Gupta:
  Improving SystemC simulation through Petri net reductions. 131-140
  

Panel

• Manfred Broy:
  Automotive software and systems engineering (Panel). 143-149
  
• Ingolf Krüger:
  Service-oriented software and systems engineering - a vision for the automotive domain. 150
  
• Wolfgang Pree:
  From bold idea to product - a case study. 151
  

Keynote Talk III

• Felice Balarin, Roberto Passerone, Alessandro Pinto, Alberto L. Sangiovanni-Vincentelli:
  A formal approach to system level design: metamodels and unified design environments. 155-163
  

Model Checking

• Françoise Bellegarde, Samir Chouali, Jacques Julliand:
  Refinemant verification of fair transition systems can contribute to PLTL model checking. 166-175
  
• Tobias Schüle, Klaus Schneider:
  Three-valued logic in bounded model checking. 177-186
  

Micro-Architectural Specification and Verification

• Panagiotis Manolios, Sudarshan K. Srinivasan:
  A computationally ef~cient method based on commitment re~nement maps for verifying pipelined machines. 188-197
  
• Ali Sezgin, Ganesh Gopalakrishnan:
  On the decidability of shared memory consistency verification. 199-208
  

Core Algorithms

• Christos Kloukinas:
  Thunderstriking constraints with JUPITER. 211-220
  
• Stefano Brait, Franco Fummi, Graziano Pravadelli:
  On the use of a high-level fault model to analyze logical consequence of properties. 221-230
  

Panel

• Tevfik Bultan, Constance L. Heitmeyer, John O'Leary:
  Panel on design for verification. 232-235
  

Posters

• Nicola Bombieri, Andrea Fedeli, Franco Fummi:
  Extended abstract: on the property-based verification in SoC design flow founded on transaction level modeling. 239-240
  
• Masahiro Fujita:
  Extended abstract: a formal design approach from software oriented UML descriptions to hardware oriented RTL. 241-242
  
• Ralph D. Jeffords, Ramesh Bharadwaj:
  Extended abstract: formal verification of architectural patterns in support of dependable distributed systems. 243-244
  
• Elizabeth I. Leonard, Myla Archer:
  Extended abstract: organizing automaton specifications to achieve faithful representation. 245-246
  
• Gustaf Naeser, Johan Furunäs:
  Extended abstract: evaluation of delay queues for a Ravenscar HW kernel. 247-248
  
• Lars Pareto:
  Extended abstract: requirements modeling within iterative, incremental processes. 249-250
  
• Peter Poplavko, Twan Basten, Milan Pastrnak, Jef L. van Meerbergen, Marco Bekooij, Peter H. N. de With:
  Extended abstract: estimation times of on-chip multiprocessor stream-oriented applications. 250-251
  
• Klaus Rothbart, Ulrich Neffe, Christian Steger, Reinhold Weiss, Edgar Rieger, Andreas Mühlberger:
  Extended abstract: an environment for design verification of smart card systems using attack simulation in SystemC. 253-254
  
• Patrick Schaumont, Sandeep K. Shukla, Ingrid Verbauwhede:
  Extended abstract: a race-free hardware modeling language. 255-256
  
• Iñigo Ugarte, Pablo Sanchez:
  Extended abstract: polynomial model-based evaluation of the branch coverage metric for functional verification of hardware systems. 257-258
  
• Xingwen Xu, Shinji Kimura, Kazunari Horikawa, Takehiko Tsuchiya:
  Extended abstract: transition traversal coverage estimation for symbolic model checking. 259-260
  

Last update Fri May 24 13:25:58 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page