default search action
3rd MEMOCODE 2005: Verona, Italy
- 3rd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2005), 11-14 July 2005, Verona, Italy, Proceedings. IEEE Computer Society 2005, ISBN 0-7803-9227-2
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
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
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
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
Panel on design for verification. 232-235
Posters
- Nicola Bombieri
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
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
Extended abstract: a race-free hardware modeling language. 255-256 - Íñ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
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.
last updated on 2025-01-14 21:01 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: