The Community for Technology Leaders
Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE '04 (2004)
San Diego, CA, USA
June 23, 2004 to June 25, 2004
ISBN: 0-7803-8509-8
TABLE OF CONTENTS

System modeling and verification with UCLID (PDF)

R.E. Bryant , Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
pp. 3-4

Verification of SpecC using predicate abstraction (PDF)

H. Jain , Carnegie Mellon Univ., Pittburgh, PA, USA
D. Kroening , Carnegie Mellon Univ., Pittburgh, PA, USA
E. Clarke , Carnegie Mellon Univ., Pittburgh, PA, USA
pp. 7-16

Bounded model checking of infinite state systems: exploiting the automata hierarchy (PDF)

T. Schuele , Dept. of Comput. Sci., Kaiserslautern Univ., Germany
K. Schneider , Dept. of Comput. Sci., Kaiserslautern Univ., Germany
pp. 17-26

Check and simulate: a case for incorporating model checking in network simulation (PDF)

A. Sobeih , Dept. of Comput. Sci., Illinois at Urbana-Champaign Univ., Urbana, IL, USA
M. Viswanathan , Dept. of Comput. Sci., Illinois at Urbana-Champaign Univ., Urbana, IL, USA
J.C. Hou , Dept. of Comput. Sci., Illinois at Urbana-Champaign Univ., Urbana, IL, USA
pp. 27-36

Curing schizophrenia by program rewriting in Esterel (PDF)

O. Tardieu , INRIA, Antipolis, France
R. de Simone , INRIA, Antipolis, France
pp. 39-48

Synchronous extensions to operation centric hardware description languages (PDF)

G. Nordin , Carnegie Mellon Univ., Pittsburgh, PA, USA
J.C. Hoe , Carnegie Mellon Univ., Pittsburgh, PA, USA
pp. 49-56

PROBMELA: a modeling language for communicating probabilistic processes (PDF)

C. Baier , Inst. fur Informatik, Bonn Univ., Germany
F. Ciesinski , Inst. fur Informatik, Bonn Univ., Germany
M. Grosser , Inst. fur Informatik, Bonn Univ., Germany
pp. 57-66

Using invariants to optimize formal specifications before code synthesis (PDF)

R.D. Jeffords , Naval Res. Lab., Washington, DC, USA
E.I. Leonard , Naval Res. Lab., Washington, DC, USA
pp. 73-82

Efficient code synthesis from synchronous dataflow graphs (PDF)

D. Bjorklund , Turku Centre for Comput. Sci., Abo Akademi Univ., Turku, Finland
pp. 83-92

Designing a reorder buffer in Bluespec (PDF)

N. Dave , Comput. Sci. & Artificial Intelligence Lab, Massachusetts Inst. of Technol., Cambridge, MA, USA
pp. 93-102

The battle of accountable voting systems (PDF)

D.L. Dill , Dept. of Stanford Comput. Sci., CA, USA
pp. 105

Static priority scheduling of event triggered real time embedded systems (PDF)

C. Erbas , Dept. of Comput. Sci., Amsterdam Univ., Netherlands
pp. 109-118

The BUSpec platform for automated generation of verification aids for standard bus protocols (PDF)

Bhaskar Pal , Dept. of Comput. Sci. & Eng., Indian Inst. of Technol., Kharagpur, India
Ansuman Banerjee , Dept. of Comput. Sci. & Eng., Indian Inst. of Technol., Kharagpur, India
Pallab Dasgupta , Dept. of Comput. Sci. & Eng., Indian Inst. of Technol., Kharagpur, India
P.P. Chakrabarti , Dept. of Comput. Sci. & Eng., Indian Inst. of Technol., Kharagpur, India
pp. 119-128

Formal verification of pipelined processors with precise exceptions (PDF)

K. Kalyanasundaram , Sch. of Technol. & Comput. Sci., Tata Inst. of Fundamental Res., Mumbai, India
R.K. Shyamasundar , Sch. of Technol. & Comput. Sci., Tata Inst. of Fundamental Res., Mumbai, India
pp. 129-139

Formal methods and software reliability (PDF)

G.J. Holzmann , JPL Lab. for Reliable Software, California Inst. of Technol., Pasadena, CA, USA
pp. 145-146

Formal verification as a technology transfer problem (PDF)

R. Kurshan , Cadence Design Syst., USA
pp. 147-150

Formal verification in Intel CPU design (PDF)

J. O'Leary , Strategic CAD Labs, Intel Corp., Sta. Clara, CA, USA
pp. 152

Designers want proofs - but show me the money (PDF)

C. Pixley , Synopsys Inc., Mountain View, CA, USA
D. Meyers , Synopsys Inc., Mountain View, CA, USA
S. McMaster , Synopsys Inc., Mountain View, CA, USA
A. Chittor , Synopsys Inc., Mountain View, CA, USA
pp. 153-154

Classes and subclasses in actor-oriented design (PDF)

E. Lee , Dept. of EECS, California Univ, Berkeley, CA, USA
S. Neuendorffer , Dept. of EECS, California Univ, Berkeley, CA, USA
pp. 161-168

Checkers for SystemC designs (PDF)

D. Grobe , Inst. of Comput. Sci., Bremen Univ., Germany
R. Drechsler , Inst. of Comput. Sci., Bremen Univ., Germany
pp. 171-178

Hierarchical reconfiguration of dataflow models (PDF)

S. Neuendorffer , Dept. of EECS, California Univ., Berkeley, CA, USA
E. Lee , Dept. of EECS, California Univ., Berkeley, CA, USA
pp. 179-188

The ephemeral history register: flexible scheduling for rule-based designs (PDF)

D.L. Rosenband , Comput. Sci. & Artificial Intelligence Lab, Massachusetts Inst. of Technol., Cambridge, MA, USA
pp. 189-198

Automated, compositional and iterative deadlock detection (PDF)

S. Chaki , Carnegie Mellon Univ., Pittsburgh, PA, USA
E. Clarke , Carnegie Mellon Univ., Pittsburgh, PA, USA
J. Ouaknine , Carnegie Mellon Univ., Pittsburgh, PA, USA
N. Sharygina , Carnegie Mellon Univ., Pittsburgh, PA, USA
pp. 201-210

Compositional verification for secure loading of smart card applets (PDF)

C. Sprenger , Swiss Fed. Inst. of Technol., Zurich, Switzerland
pp. 211-222
94 ms
(Ver 3.3 (11022016))