1. An Introduction to Clam-Spark (CS) Notes: [ps, pdf]

2. The Clam-Spark Proposal: [ps, pdf]

3. Diving into the SPARK Approach: [ps]

4. A Guided Tour of the SPADE Proof Checker: [ps]

5. A Guided Tour of the CLAM Proof Planner: [ps]

6. NuSPADE: Proof Planning for SPARK Verification Proofs: [ps]

7. NuSPADE - an opportunity to polish up SPADE? [ps]

8. SPADE Rules - Logic, Tricks and NuSPADE [ps]

9. Proof Planning (Bluffers guide, Architectures) and Prototyping NuSPADE [ps]

10. The Polish Flag Problem [ps]

11. Framework for NuSPADE Development [ps]

12. Assisting in the Proof of Spark Exception Freedom [ps]

13. Meeting Praxis Critical Systems [ps]

14. POPLOG-PROLOG versus SICSTUS? (No Contest) [ps]

15. Pushing Tin: An Air Traffic Control Simulator [ps]

16. Modifying the SPARK Tools [ps]

17. Requirements and design of System: FRiENDLY [ps]

18. Documenting SIMPLIFIER Changes (For FRiENDLY) [ps]

19. Raising NuSPADE Issues (Volume 1) [ps]

20. Raising NuSPADE Issues (Volume 2) [ps]

21. Raising NuSPADE Issues (Volume 3) [ps]

22. Pushing Tin Project - First Design Draft [ps]

23. Pushing Tin Project - Second Design Draft [ps]

24. Pushing Tin Project - Third Design Draft [ps]

25. Pushing Tin Project - Fourth Design Draft [ps]

26. Pushing Tin Project - Fifth Design Draft [ps]

27. Pushing Tin Project - Amended Design Draft 5 [ps]

28. Pushing Tin Project - Algorithms [ps]

29. The SPARK Ada Experience [ps]

30. On Combining Proof and Algorithmic Patterns [ps]

31. Learning by Example - Exception Freedom in Polish Flag [ps]

32. Learning by Example - Exception Freedom in Table Utilities (Delete) [ps]

33. Porting SPADE-PC to SICSTUS [ps]

34. Automatic Discovery for RTC Proofs [ps]

35. Learning by Example - Table Utilities (Find) [ps]

36. Raising NuSPADE Issues (Volume 4) [ps]

37. The Mini-Corpus [ps]

38. VASST Trip Report [ps]

39. Generating Patterns for Constant Path Analysis (CPA) [ps]

40. Notes on Parsing SPARK for Property Extraction [ps]

41. Automation for Exception Freedom Proofs: Take-2 [ps]

42. Rippling and Proofs of Exception Freedom [ps]

43. Refining Constant Path Analysis (CPA) [ps]

44. Recurrence Relations and Invariant Discovery [ps]

45. Program Prover Needs the Programs! [ps]

46. Sketches Of Constant Path Analysis (CPA) [ps]

47. Program Transformation with XT and STRATEGO [ps]

48. New, New, New NUSPADE [ps]

49. Mechanics of Visualising VCs [ps]

50. Scottish Theorem Provers at St Andrews [ps]

51. Exploring AutoGAP heuristics for supporting the proof of bubble sort [ps]

52. Exploring AutoGAP heuristics for supporting the proof of bubble sort: Take Two [ps]

53. Extending AutoGAP [ps]

54. Invariant extensions to AutoGAP [ps]

55. Visits to NASA Ames and HP's Systems Research Center [ps]

56. Bubble sort revisited [ps]

57. Visiting Praxis: A Praxis Shopping List [ps]

58. Visiting Praxis: Into the deep [ps]

59. Visiting Praxis: Harder Examples [ps]

60. Visiting Praxis: Less critical SPARK [ps]

61. Visiting Praxis: Random SPARK Observations [ps]

62. Proof Planning for Bubble Sort Verification [ps]

63. Invariant Patterns for Program Reasoning [ps]

64. Trip Report: Automated Software Engineering 2003 (Montreal) [ps]

65. SPADEWiz: A SPADE Wizard [ps]

66. Experiment: Industrial strength analysis [ps]

67. Praxis Retreat: A Roadmap (Why am I here? ; Where am I going?) [ps]

68. Praxis Retreat: A Survey [ps]

69. Praxis Retreat: A Targeted Survey [ps]

70. Praxis Retreat: Whole System Survey [ps]

71. Praxis Retreat: Random Notes [ps]

72. Automatically Enriching SPARK Specifications [ps]

73. Translation Stuff [ps]

74. Onwards and Upwards [ps]

75. Invariant Patchy [ps]

76. Fiddling with Variable Names [ps]

77. Using Upwards [ps]

78. Array Sieve [ps]

79. Filtering Verification Conditions using Slugs [ps]

80. Praxis trip III: Towards Empirical Evaluation [ps]

81. Praxis trip III: Evaluation Problems and Solutions [ps]

82. Praxis trip III: System T [ps]

83. Praxis trip III: System S [ps]

84. Praxis trip III: Notes [ps]

85. NuSPADE goes to York: Trip Report [ps]

86. Spark Plugs [ps]

87. Environment Simulator for Teaching SPARK [ps]