The Community for Technology Leaders
Formal Methods and Models for Co-Design, ACM/IEEE International Conference on (2005)
Verona, Italy
July 11, 2005 to July 14, 2005
ISBN: 0-7803-9227-2
TABLE OF CONTENTS
Papers

A synchronous language at work: the story of Lustre (Abstract)

N. Halbwachs , Verimag, Grenoble, France
pp. 3-11

Synthesis of synchronous assertions with guarded atomic actions (Abstract)

M. Pellauer , Massachusetts Inst. of Technol., Cambridge, MA, USA
pp. 15-24

Automatic synthesis of cache-coherence protocol processors using Bluespec (Abstract)

M.C. Ng , Comput. Sci.&Artificial Intelligence Lab., Massachusetts Univ., Cambridge, MA, USA
null Arvind , Comput. Sci.&Artificial Intelligence Lab., Massachusetts Univ., Cambridge, MA, USA
N. Dave , Comput. Sci.&Artificial Intelligence Lab., Massachusetts Univ., Cambridge, MA, USA
pp. 25-34

Deterministic receptive processes are Kahn processes (Abstract)

O. Tardieu , Columbia Univ., New York, NY, USA
S.A. Edwards , Columbia Univ., New York, NY, USA
pp. 37-44

Structural operational semantics for supporting multi-cycle operations in RTL HDLs (Abstract)

D.D. Gajski , Center of Embedded Comput. Syst., California Univ., Irvine, CA, USA
S. Zhao , Center of Embedded Comput. Syst., California Univ., Irvine, CA, USA
pp. 45-53

PyPBS design and methodologies (Abstract)

G. Hoover , Dept. of Electr.&Comput. Eng., California Univ., Santa Barbara, CA, USA
F. Brewer , Dept. of Electr.&Comput. Eng., California Univ., Santa Barbara, CA, USA
pp. 55-64

Making PVS do what you want (PDF)

M. Archer , Center for High Assurance Comput. Syst., Naval Res. Lab., Washington, DC, USA
pp. 67

System design extreme makeover (Abstract)

D.D. Gajski , Center for Embedded Comput. Syst., California Univ., Irvine, CA, USA
pp. 71-75

Verification of low-level crypto-protocol implementations using automated theorem proving (Abstract)

J. Jurjens , Dept. of Informatics, Technische Univ. Munchen, Germany
pp. 89-98

Formal verification of SystemC by automatic hardware/software partitioning (Abstract)

D. Kroening , Comput. Syst. Inst., Eidgenossische Tech. Hochschule, Zurich, Switzerland
pp. 101-110

Translation-based co-verification (Abstract)

F. Xie , Dept. of Comput. Sci., Portland State Univ., OR, USA
pp. 111-120

Synchronization verification in system-level design with ILP solvers (Abstract)

S. Komatsu , VLSI Design&Educ. Center, Tokyo Univ., Japan
T. Sakunkonchak , VLSI Design&Educ. Center, Tokyo Univ., Japan
M. Fujita , VLSI Design&Educ. Center, Tokyo Univ., Japan
pp. 121-130

Automotive software and systems engineering (Abstract)

M. Broy , Inst. fur Inf., Technische Univ. Munchen, Germany
pp. 143-149

Service-oriented software and systems engineering - a vision for the automotive domain (Abstract)

I.H. Kruger , Dept. of Comput. Sci.&Eng., California Univ., San Diego, CA, USA
pp. 150

From bold idea to product - a case study (Abstract)

W. Pree , Dept. of Comput. Sci., Univ. of Salzburg, Austria
pp. 151

Three-valued logic in bounded model checking (Abstract)

T. Schuele , Dept. of Comput. Sci., Kaiserslautern Univ., Germany
K. Schneider , Dept. of Comput. Sci., Kaiserslautern Univ., Germany
pp. 177-186

On the decidability of shared memory consistency verification (Abstract)

A. Sezgin , Dept. of Comput. Eng., Atilim Univ., Ankara, Turkey
pp. 199-208

Thunderstriking constraints with JUPITER (Abstract)

C. Kloukinas , Dept. of Comput., City Univ., London, UK
pp. 211-220

On the use of a high-level fault model to analyze logical consequence of properties (Abstract)

G. Pravadelli , Dipt. di Informatica, Univ. di Verona, Italy
S. Brait , Dipt. di Informatica, Univ. di Verona, Italy
F. Fummi , Dipt. di Informatica, Univ. di Verona, Italy
pp. 221-230

Extended abstract: formal verification of architectural patterns in support of dependable distributed systems (Abstract)

R. Jeffords , Center for High Assurance Comput. Syst., Naval Res. Lab., Washington, DC, USA
R. Bharadwaj , Center for High Assurance Comput. Syst., Naval Res. Lab., Washington, DC, USA
pp. 243-244

Extended abstract: organizing automaton specifications to achieve faithful representation (Abstract)

E. Leonard , Center for High Assurance Comput. Syst., Naval Res. Lab., Washington, DC, USA
M. Archer , Center for High Assurance Comput. Syst., Naval Res. Lab., Washington, DC, USA
pp. 245-246

Extended abstract: evaluation of delay queues for a Ravenscar HW kernel (Abstract)

J. Furunas , Dept. of Comput. Sci.&Electron., Malardalen Univ., Sweden
G. Naeser , Dept. of Comput. Sci.&Electron., Malardalen Univ., Sweden
pp. 247-248

Extended abstract: an environment for design verification of smart card systems using attack simulation in SystemC (Abstract)

U. Neffe , Graz Univ. of Technol., Austria
R. Weiss , Graz Univ. of Technol., Austria
Ch. Steger , Graz Univ. of Technol., Austria
K. Rothbart , Graz Univ. of Technol., Austria
pp. 253-254

Extended abstract: transition traversal coverage estimation for symbolic model checking (Abstract)

X. Xu , Graduate Sch. of IPS, Waseda Univ., Tokyo, Japan
S. Kimura , Graduate Sch. of IPS, Waseda Univ., Tokyo, Japan
pp. 259-260

Author index (PDF)

pp. 261
312 ms
(Ver )