| Date | Presenters | Topics/Papers |
|---|---|---|
| March 5 | Ali // Giray | Runtime Verification // Error Diagnosis |
| March 12 | Roza // Salih | Deadlock and Datarace detection // Runtime Verification |
| March 19 | Pinar // Dogan | Concolic Testing // SystemC schedulings |
| March 26 | Ali // Giray | Partial Order Trace Analysis with Computation Slicing // Sequential Equivalence Checking |
| April 2 | Roza // Salih | Assertion-Based Verification // Mutation Analysis |
| April 9 | Pinar // Dogan | Concolic Testing II // Hardware-in-the-loop with SystemC |
| April 16 | Invited speaker | TBD |
| May 7 | Pinar // Dogan | Project presentations |
| May 14 | Roza // Salih | Project presentations |
| May 21 | Ali // Giray | Project presentations |
Project: Formal Verification of Fault Tolerant Tomasulo's algorithm in VHDL
Presentation1: Deadlock, Datarace detection PPT
- R. Agarwal and S. D. Stoller. Run-Time Detection of Potential Deadlocks for Programs with Locks, Semaphores, and Condition Variables. PDF
- O. Shacham, M. Sagiv, and A. Schuster. Scaling Model Checking of Dataraces Using Dynamic Information. PDF
Presentation2: Assertion-Based Verification PPT
Vardi, M.Y. "Formal techniques for SystemC verification." Proc. 44th ACM/IEEE Design Automation Conference (2007) PDF
Ali Habibi, Sofične Tahar: Design and verification of SystemC transaction-level models. IEEE Trans. VLSI Syst. 14(1): 57-68 (2006). PDF
A. Habibi and S. Tahar: Towards an Efficient Assertion Based Verification of SystemC Designs; Proc. IEEE International High Level Design Validation and Test Workshop, Sonoma Valley, California, USA, November 2004, pp. 19-22 PDF
Project: Mutation Analysis for SystemC/VHD/Verilog.
Presentation1: Runtime Verification PDF
- Alper Sen, Vinit Ogale and Magdy S. Abadir, Predictive Runtime Verification of Multi-Processor SoCs in SystemC. PDF
- Sudipta Kundu, Malay K. Ganai, Rajesh Gupta: Partial order reduction for scalable testing of. SystemC TLM designs. PDF
Presentation2: Mutation Analysis PPT
Leveraging a Commercial Mutation Analysis Tool for Research PDF
Impact of Hardware Emulation on the Verification Quality Improvement PDF
Project: Formal Protocol Verification of (LTE, 802.16) with Java PathFinder (or SPIN)
Presentation1: Runtime Verification PPT
- Runtime Safety Analysis of Multithreaded Programs, Koushik Sen, Grigore Rosu, and Gul Agha. PDF
- K. Havelund and G. Rosu, Monitoring Java Programs with Java PathExplorer. PDF
Presentation2: Partial Order Trace Analysis with Computation Slicing PPT
- Alper Sen and Vijay K. Garg, Formal Verification of Simulation Traces Using Computation Slicing PDF
- Alper Sen and Vijay K. Garg, Partial Order Trace Analyzer (POTA) for Distributed Programs PDF
Project: Build and verify a SystemC virtual prototype
Presentation1: SystemC schedulings PPT
- Automatic generation of schedulings for improving the test coverage of SoC, C. Helmstetter. PDF
- Nicolas Blanc, Daniel Kroening, Natasha Sharygina: Scoot: A Tool for the Analysis of SystemC Models. PDF
Presentation2: Hardware-in-the-loop with SystemC PPT
Mixed SW-SystemC SoC Emulation Framework PDF
Virtual in-circuit emulation for timing accurate system prototyping PDF
Project: Formal verification of a Cryptography circuit in VHDL
Presentation1: Error Diagnosis PPT
- Design Error Diagnosis and Correction via test Vector Simulation, A. Veneris et al. PDF
- On the relation between simulation-based and sat-based diagnosis, G. Roy, S. Safarpour. PDF
- Error Diagnosis in Equivalence Checking of High Performance Microprocessors, Alper Sen. PDF
Presentation2: Sequential Equivalence Checking PPT
- Principles of Sequential-Equivalence Verification, M. Mneimneh et al. PDF
- Towards Equivalence Checking Between TLM and RTL Models, N. Bombieri et al. PDF
Project: Concolic testing for SystemC
Presentation1: Concolic Testing PPT
- CUTE: A Concolic Unit Testing Engine for C, Koushik Sen, Darko Marinov, and Gul Agha. PDF
- K. Sen and G. Agha, "CUTE and jCUTE : Concolic Unit Testing and Explicit Path Model-Checking Tools". PDF
Presentation2: Concolic Testing II PPT