2. MEMOCODE 2004: San Diego, California, USA

2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 23-25 June 2004, San Diego, California, USA, Proceedings. IEEE 2004 BibTeX

Keynote Talk I

Randal E. Bryant:
System modeling and verification with UCLID. 3-4
Electronic Edition (link) BibTeX

Model Checking

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

Modeling Languages

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

Tutorial

Rishiyur S. Nikhil:
Bluespec System Verilog: efficient, correct RTL from high level specifications. 69-70
Electronic Edition (link) BibTeX

Synthesis

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

Keynote Talk II

David L. Dill:
The battle of accountable voting systems. 105
Electronic Edition (link) BibTeX

Formal Verification

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

Panel

Brian Bailey:
Is formal being squeezed out of functional verification? 143
Electronic Edition (link) BibTeX
Gerard J. Holzmann:
Formal methods and software reliability. 145-146
Electronic Edition (link) BibTeX
Robert P. Kurshan:
Formal verification as a technology transfer problem. 147-150
Electronic Edition (link) BibTeX
Vladimir Levin:
Static driver verifier, a formal verification tool for Windows device drivers. 151
Electronic Edition (link) BibTeX
John O'Leary:
Formal verification in Intel CPU design. 152
Electronic Edition (link) BibTeX
Carl Pixley, D. Meyers, S. McMaster, A. Chittor:
Designers want proofs - but show me the money. 153-154
Electronic Edition (link) BibTeX
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
Electronic Edition (link) BibTeX

Keynote Talk III

Edward A. Lee, Stephen Neuendorffer:
Classes and subclasses in actor-oriented design. 161-168
Electronic Edition (link) BibTeX

Simulation and Testing

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

Compositional Verification

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