Ganesh Gopalakrishnan

Proceedings of the 5th Workshop on Parallel and Distributed Systems: Testing, 2007

Formal Analysis for Debugging and Performance Optimization of MPI.

[BibT_eX]

[DOI]

Proceedings of the 21th International Parallel and Distributed Processing Symposium (IPDPS 2007), 2007

Hierarchical cache coherence protocol verification one level at a time through assume guarantee.

[BibT_eX]

[DOI]

Xiaofang Chen

Yu Yang

Michael Delisi

Ching-Tsun Chou

Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2007

An Approach to Formalization and Analysis of Message Passing Libraries.

[BibT_eX]

[DOI]

Michael Delisi

Proceedings of the Formal Methods for Industrial Critical Systems, 2007

Transaction Based Modeling and Verification of Hardware Protocols.

[BibT_eX]

[DOI]

Xiaofang Chen

Steven M. German

Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

2006

Preface.

[BibT_eX]

[DOI]

John O'Leary

Proceedings of the Thread Verification Workshop, 2006

Exploiting Symmetry and Transactions for Partial Order Reduction of Rule Based Specifications.

[BibT_eX]

[DOI]

Ritwik Bhattacharya

Steven M. German

Proceedings of the Model Checking Software, 13th International SPIN Workshop, Vienna, Austria, March 30, 2006

Formal Verification of Programs That Use MPI One-Sided Communication.

[BibT_eX]

[DOI]

Salman Pervez

Rajeev Thakur

William D. Gropp

Proceedings of the Recent Advances in Parallel Virtual Machine and Message Passing Interface, 2006

Toward reliable and efficient message passing software through formal analysis.

[BibT_eX]

[DOI]

Proceedings of the 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), 2006

Reducing Verification Complexity of a Multicore Coherence Protocol Using Assume/Guarantee.

[BibT_eX]

[DOI]

Xiaofang Chen

Yu Yang

Ching-Tsun Chou

Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

Computation engineering - applied automata theory and logic.

[BibT_eX]

[DOI]

Springer, ISBN: 978-0-387-24418-1, 2006

2005

Live sequence charts applied to hardware requirements specification and verification.

[BibT_eX]

[DOI]

Annette Bunker

Int. J. Softw. Tools Technol. Transf., 2005

On the definition of sequential consistency.

[BibT_eX]

[DOI]

Ali Sezgin

Inf. Process. Lett., 2005

Gauss: A Framework for Verifying Scientific Computing Software.

[BibT_eX]

[DOI]

Steve Barrus

Yu Yang

Proceedings of the 3rd Workshop on Software Model Checking, 2005

UMM: an operational memory model specification framework with integrated model checking capability.

[BibT_eX]

[DOI]

Concurr. Pract. Exp., 2005

On the decidability of shared memory consistency verification.

[BibT_eX]

[DOI]

Ali Sezgin

Proceedings of the 3rd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2005), 2005

Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification.

[BibT_eX]

[DOI]

Sudhindra Pandav

Proceedings of the Correct Hardware Design and Verification Methods, 2005

Symbolic Partial Order Reduction for Rule Based Transition Systems.

[BibT_eX]

[DOI]

Ritwik Bhattacharya

Steven M. German

Proceedings of the Correct Hardware Design and Verification Methods, 2005

2004

Formal hardware specification languages for protocol compliance verification.

[BibT_eX]

[DOI]

Annette Bunker

Sally A. McKee

ACM Trans. Design Autom. Electr. Syst., 2004

Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models.

[BibT_eX]

[DOI]

Proceedings of the 18th International Parallel and Distributed Processing Symposium (IPDPS 2004), 2004

Memory-Model-Sensitive Data Race Analysis.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2004

QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings.

[BibT_eX]

[DOI]

Hemanthkumar Sivaraj

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

Formal Verification of a Complex Pipelined Processor.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2003

Industrial Practice of Formal Hardware Verification: A Sampling.

[BibT_eX]

[DOI]

Warren A. Hunt Jr.

Formal Methods Syst. Des., 2003

Random Walk Based Heuristic Algorithms for Distributed Memory Model Checking.

[BibT_eX]

[DOI]

Hemanthkumar Sivaraj

Proceedings of the 2nd International Workshop on Parallel and Distributed Model Checking, 2003

A Practical Methodology for Verifying Pipelined Microarchitectures.

[BibT_eX]

[DOI]

IEEE Des. Test Comput., 2003

Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2003

2002

An Efficient Partial Order Reduction Algorithm with an Alternative Proviso Implementation.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2002

Deriving Efficient Cache Coherence Protocols Through Refinement.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2002

Robust rate based congestion control.

[BibT_eX]

[DOI]

Sneha Kumar Kasera

Comput. Commun. Rev., 2002

Incremental Proof of the Producer/Consumer Property for the PCI Protocol.

[BibT_eX]

[DOI]

Dominique Cansell

Dominique Méry

Airy Weinzoepflen

Proceedings of the ZB 2002: Formal Specification and Development in Z and B, 2002

Specifying Java thread semantics using a uniform memory model.

[BibT_eX]

[DOI]

Syam Krishna Babbellapati

Proceedings of the 2002 Joint ACM-ISCOPE Conference on Java Grande 2002, 2002

FSRC: fair and stable rate control - a TCP-friendly adaptive rate control scheme for packet audio applications.

[BibT_eX]

[DOI]

T. S. Lamba

Proceedings of the Proceedings 10th IEEE International Conference on Networks: Towards Network Superiority, 2002

A Distributed Partial Order Reduction Algorithm.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Networked and Distributed Systems, 2002

A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols.

[BibT_eX]

[DOI]

Prosenjit Chatterjee

Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking.

[BibT_eX]

[DOI]

Prosenjit Chatterjee

Hemanthkumar Sivaraj

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001

towards A formal Model of Shared Memory Consistency for Intel Itanium<sup>TM</sup>.

[BibT_eX]

[DOI]

Prosenjit Chatterjee

Proceedings of the 19th International Conference on Computer Design (ICCD 2001), 2001

Using live sequence charts for hardware protocol specification and compliance verification.

[BibT_eX]

[DOI]

Annette Bunker

Proceedings of the Sixth IEEE International High-Level Design Validation and Test Workshop 2001, 2001

2000

Formalization and Analysis of a Solution to the PCI 2.1 Bus Transaction Ordering Problem.

[BibT_eX]

[DOI]

Abdel Mokkedem

Formal Methods Syst. Des., 2000

Introduction: Formal Methods for CAD: Enabling Technologies and System-level Applications.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2000

Verification Methods for Weaker Shared Memory Consistency Models.

[BibT_eX]

[DOI]

Rajnish Ghughal

Proceedings of the Parallel and Distributed Processing, 2000

Achieving Fast and Exact Hazard-Free Logic Minimization of Extended Burst-Mode gC Finite State Machines.

[BibT_eX]

[DOI]

Chris J. Myers

Proceedings of the 2000 IEEE/ACM International Conference on Computer-Aided Design, 2000

Toward automated abstraction for protocols on branching networks.

[BibT_eX]

[DOI]

Proceedings of the IEEE International High-Level Design Validation and Test Workshop 2000, 2000

Verifying Transaction Ordering Properties in Unbounded Bus Networks through Combined Deductive/Algorithmic Methods.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

Verifying Advanced Microarchitectures that Support Speculation and Exceptions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

High-Level Asynchronous System Design Using the ACK Framework.

[BibT_eX]

[DOI]

Proceedings of the 6th International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 2000), 2000

1999

Timing constraints for high-speed counterflow-clocked pipelining.

[BibT_eX]

[DOI]

Jae-Tack Yoo

Kent F. Smith

IEEE Trans. Very Large Scale Integr. Syst., 1999

Peephole optimization of asynchronous macromodule networks.

[BibT_eX]

[DOI]

IEEE Trans. Very Large Scale Integr. Syst., 1999

Corrections To application-specific Programmable Control For High-performance Asynchronous Circuits.

[BibT_eX]

[DOI]

Proc. IEEE, 1999

Application-specific programmable control for high-performance asynchronous circuits.

[BibT_eX]

[DOI]

Proc. IEEE, 1999

A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 1999

1998

Using "Test Model-Checking" to Verify the Runway-PA8000 Memory Model.

[BibT_eX]

[DOI]

Rajnish Ghughal

Abdelillah Mokkedem

Proceedings of the Tenth Annual ACM Symposium on Parallel Algorithms and Architectures, 1998

PV: An Explicit Enumeration Model-Checker.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 1998

Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem.

[BibT_eX]

[DOI]

Abdelillah Mokkedem

Proceedings of the Formal Methods in Computer-Aided Design, 1998

The 'Test Model-Checking' Approach to the Verification of Formal Memory Models of Multiprocessors.

[BibT_eX]

[DOI]

Rajnish Ghughal

Abdelillah Mokkedem

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

Decomposing the Proof of Correctness of pipelined Microprocessors.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997

A fast parallel squarer based on divide-and-conquer.

[BibT_eX]

[DOI]

Jae-Tack Yoo

Kent F. Smith

IEEE J. Solid State Circuits, 1997

Formal modeling and validation applied to a commercial coherent bus: a case study.

[BibT_eX]

Proceedings of the Advances in Hardware Design and Verification, 1997

Asynchronous Microengines for Efficient High-level Control.

[BibT_eX]

[DOI]

Proceedings of the 17th Conference on Advanced Research in VLSI (ARVLSI '97), 1997

1996

Synthesis for Hazard-free Customized CMOS Complex-Gate Networks Under Multiple-Input Changes.

[BibT_eX]

[DOI]

Steven M. Nowick

Proceedings of the 33st Conference on Design Automation, 1996

A Technique for Synthesizing Distributed Burst-mode Circuits.

[BibT_eX]

[DOI]

Proceedings of the 33st Conference on Design Automation, 1996

1995

High speed counterflow-clocked pipelining illustrated on the design of HDTV subband vector quantizer chips.

[BibT_eX]

[DOI]

Jae-Tack Yoo

Kent F. Smith

V. John Mathews

Proceedings of the 16th Conference on Advanced Research in VLSI (ARVLSI '95), 1995

1994

High-level optimizations in compiling process descriptions to asynchronous circuits.

[BibT_eX]

[DOI]

J. VLSI Signal Process., 1994

Specification and Validation of Control-Intensive IC's in hopCP.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 1994

Efficient symbolic simulation-based verification using the parametric form of Boolean expressions.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994

A correctness criterion for asynchronous circuit validation and optimization.

[BibT_eX]

[DOI]

Nick Michell

Steven M. Nowick

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994

CFSIM: A Concurrent Compiled Code Functional Simulator for hopCP.

[BibT_eX]

[DOI]

Int. J. Comput. Simul., 1994

Developing Micropipeline Wavefront Arbiters.

[BibT_eX]

[DOI]

IEEE Des. Test Comput., 1994

Performance Analysis and Optimization of Asynchronous Circuits.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1994 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1994

1993

Design and Verification of the Rollback Chip Using HOP: A Case Study of Formal Methods Applied to Hardware design.

[BibT_eX]

[DOI]

Richard Fujimoto

ACM Trans. Comput. Syst., 1993

Guest editors' introduction to the special issue on asynchronous systems.

[BibT_eX]

[DOI]

Integr., 1993

A transformational approach to asynchronous high-level synthesis.

[BibT_eX]

Proceedings of the VLSI 93, 1993

Hierarchical Constraint Solving in the Parametric Form with Applications to Efficient Symbolic Simulation Based Verification.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1993 International Conference on Computer Design: VLSI in Computers & Processors, 1993

1992

Design and Evaluation of the Rollback Chip: Special Purpose Hardware for Time Warp.

[BibT_eX]

[DOI]

Richard Fujimoto

Jya-Jang Tsai

IEEE Trans. Computers, 1992

VLSI asynchronous systems: specification and synthesis.

[BibT_eX]

[DOI]

Microprocess. Microsystems, 1992

From Process-Oriented Functional Specifications to Efficient Asynchronous Circuits.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Conference on VLSI Design, 1992

Dynamic Reordering of Hgh Latency Transactions Using a Modified a Micropipeline.

[BibT_eX]

[DOI]

Gernot Armin Liebchen

Proceedings of the Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1992

Some Techniques for Efficient Symbolic Simulation-Based Verification.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1992

SHILPA: a high-level synthesis system for self-timed circuits.

[BibT_eX]

[DOI]

Proceedings of the 1992 IEEE/ACM International Conference on Computer-Aided Design, 1992

Towards a Verification Technique for Large Synchronous Circuits.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, Fourth International Workshop, 1992

1989

HOP: A process model for synchronous hardware; semantics and experiments in process composition.

[BibT_eX]

[DOI]

Richard M. Fujimoto

Narayana Mani

Integr., 1989

Parallel Composition of Lockstep Synchronous Processes for Hardware Validation: Divide-and-Conquer Composition.

[BibT_eX]

[DOI]

Narayana Mani

Proceedings of the Automatic Verification Methods for Finite State Systems, 1989

1988

Implementing Functional Programs Using Mutable Abstract Data Types.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1988

Design and Performance of Special Purpose Hardware for Time Warp.

[BibT_eX]

[DOI]

Richard Fujimoto

Jya-Jang Tsai

Proceedings of the 15th Annual International Symposium on Computer Architecture, 1988

1987

Synthesizing Synchronous Digital VLSI Controllers Using Petri Nets.

[BibT_eX]