A Complete Mechanization of Correctness of a String-Preprocessing Algorithm Milos BestaFrank Stomp OriginalPaper Pages: 5 - 27
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking Sharon BarnerOrna Grumberg OriginalPaper Pages: 29 - 66
A Formal Framework for Verification of Embedded Custom Memories of the Motorola MPC7450 Microprocessor Jayanta BhadraAndrew K. MartinJacob A. Abraham OriginalPaper Pages: 67 - 112
Two Case Studies of Semantics Execution in Maude: CCS and LOTOS Alberto VerdejoNarciso MartÃ-Oliet OriginalPaper Pages: 113 - 172
Formalization of Fixed-Point Arithmetic in HOL Behzad AkbarpourSofiène TaharAbdelkader Dekdouk OriginalPaper Pages: 173 - 200