


default search action
2nd 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 Computer Society 2004, ISBN 0-7803-8509-8

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

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














