Seven myths of formal methods A Hall - IEEE Software, 1990
How Amazon web services uses formal methods C Newcombe, T Rath, F Zhang, B Munteanu, M Brooker, and M Deardeuff - Communications of the ACM 2015
Model Checking TLA+ Specifications Y Yu, P Manolios, and L Lamport - Correct Hardware Design and Verification Methods (CHARME) 1999
A Summary of TLA+ L Lamport
TLA+ Verification of Cache-Coherence Protocols H Akhiani, D Doligez, P Harter, L Lamport, M Tuttle, and Y Yu
Shared Memory Consistency Models: A Tutorial S Adve and K Gharachorloo - IEEE Computer 1995 [read up through sequential consistency on page 11]
A Survey of Recent Advances in SAT-Based Formal Verification M Prasad, A Biere, and A Gupta
You are encouraged to attend Mike Ferdman's talk on "Maximizing Server Efficiency with Machine-Learning Accelerators" in ESB 1001 at 4pm
TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA C Trippel, Y Manerkar, D Lustig, M Pellauer, and M Martonosi
Complete Information Flow Tracking from the Gates Up M Tiwari, X Li, H Wassel, F Chong, and T Sherwood (concentrate on Section 3, only skim rest)
Execution Leases: A Hardware-Supported Mechanism for Enforcing Strong Non-Interference M Tiwari, H Wassel, B Mazloom, S Mysore, F Chong, and T Sherwood
Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis A Ferraiuolo, R Xu, D Zhang, A Myers, E Suh
Reading privileged memory with a side-channel Spectre and Meltdown technical breakdown
Shared Resource Matrix Methodology: An Approach to Identifying Storage and Timing Channels R Kemmerer
Automated analysis of cryptographic protocols using Murphi J Mitchell, M Mitchell, and U Stern
A Formal Foundation for Secure Remote Execution of Enclaves P Subramanyan, R Sinha, I Lebedev, S Devadas, S Seshia
Phantom: Practical oblivious computation in a secure processor M Maas, E Love, E Stefanov, M Tiwari, E Shi, K Asanovic, J Kubiatowicz, and D Song
SurfNoC: A Low Latency and Provably Non-Interfering Approach to Secure Networks-On-Chip H Wassel, Y Gao, J Oberg, T Huffmire, R Kastner, F Chong, and T Sherwood
Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T) R Nieuwenhuis, A Oliveras, and C Tinelli (you can ignore the proofs and the details of the results for the class discussion)
No class (Get together with your teams and work on your projects!)
Formal Requirements for Virtualizable Third Generation Architectures G Popek and R Goldberg