ECE 598 SV

Formal Hardware/SoC Verification

Individual Presentations

Name	Topic	Papers
Byn Choi	Cache Coherence Protocols	Parametrized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking - K.L. McMillan Verification of the Futurebus+ Cache Coherence Protocol - Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness Formal Design of Cache Memory Protocols in IBM - Steven M. German
Jayanand Asok Kumar	Probabilistic Systems	Formal Verification of Probabilistic Systems - Luca de Alfaro A logic for reasoning about time and reliability - Hans Hansson, Bengt Jonsson
Christopher Rodrigues	Assembly Language Functions	Proof Carrying Code - George Necula
Gabriela Jacques da Silva	Operating Systems and Fault Injection	Thorough Static Analysis of Device Drivers Building SWIFI Tools from Temporal Logic Specifications
Lu Wan	Microprocessor Bus Protocol	Formal verification of an IBM CoreConnect processor local bus arbiter core, DAC2000 Formal Verification of a Pervasive Interconnect Bus System in a High-Performance Microprocessor, DAC2007 Verification of Cell Broadband Engine Processor, DAC 2006
Matthew Hicks
Francesco Sorrentino	Bounded Model Checking	Ensuring Consistency in Long Running Transactions - J.Fischer and R.Majumdar, ASE 2007 The Consistency of Web Conversations - J.Fischer, R.Majumdar, and F.Sorrentino., ASE 2008. Symbolic model checking without BDD's – A. Biere, A. Cimatti, E.M. Clarke, Y. Zhu.
Vladimeros Vladimerou	O-minimal Hybrid Systems
Siva Kumar Hari
Xuehai Qian	Correctness issues in Multiprocessor systems
R. Ulya Karpuzcu	Cache Coherence Protocol	Lamport clocks: verifying a directory cache-coherence protocol - Plakal et al. Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking- Qadeer S.
Pradeep Ramachandran	Microprocessors	Automatic Verification of Pipelined Microprocessor Control - J. Burch and D. Dill Functional verification of the POWER5 microprocessor and POWER5 multiprocessor systems - D. Victor et al
Patrick Meredith	Programming Language Semantics	Hardware Runtime Monitoring for Dependable COTS-based Real-Time Embedded Systems A Rewriting Logic Approach to Operational Semantics
Kyoung-Dae Kim	Software Model-Checking	Model-Checking of Component-Based Event-Driven Real-Time Embedded Software, Zonghua Gu, Kang G. Shin. Reusable Models for Timing and Livenes Analysis of Middleware for Distributed Real-Time and Embedded Systems, Venkita Subramonian, Christoper Gill, Cesar Sanchez, Henny B. Sipma.
Long Wang	Intrusion Detection	Formalizing System Behavior for Evaluating a System Hang Detector, Long Wang, Zbigniew Kalbarczyk, Ravishankar K. Iyer. Formalizing Sensitivity in Static Analysis for Intrusion Detection, Henry Hanping Feng, Jonathon T. Giffin, Yong Huang, Somesh Jha, Wenke Lee, and Barton P. Miller.
Swarup Sahoo