[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS656/556 Course Materials] >> index
[Index] || [Contents] || [Grades] Tue Aug 5 11:45:00 PDT 2003

# Formal Methods Web Site

## News Sat Mar 22 15:21:54 PST 2003

Completed grading posted at [ grading656 ] 6 A/A-s and 9 B+/B/B-s and one I! Thank you for working so hard!

. . . . . . . . . ( end of section News) <<Contents | Index>>

## Syllabi etc.

(Syllabi): Generic [ syllabus.html ] , CS656/556: [ syllabus.htm ] (HTML) and [ syllabus.pdf ] (PDF)

(Schedule): See [ schedule.txt ] (Tab delimitted text), [ schedule.htm ] (HTML), and [ schedule.pdf ] (PDF)

(Exercises in book): See [ exercises.html ] [ exercises.m ] [ exercises.mth ]

## Classes

(Introduction): who, what, why [ 01.html ]
(PC): Propositional Calculus [ 02.html ] [ 03.html ] [ 04.html ] [ 05.html ] [ 06.html ]
(OBDDs): Ordered Binary Decisison Diagrams [ 07.html ] [ 08.html ]
(LPC): Predicate calculus -- the machine code of reality: [ 09.html ] [ 10.html ]
(midterm): Logic [ 11.html ]
(CTL): Dynamic Logic [ 12.html ] [ 13.html ]
(SMV): tool [ 14.html ] [ 15.html ] [ SMVprogram ]
(Hoare): verifying programs [ 16.html ] [ 17.html ] [ 18.html ]
(presentations): [ 19.html ] [ 20.html ] [ http://www.csci.csusb.edu/dick/cs656/presentations/ ]
(final): comprehensive

[ Topics ]

## Resources by topic

(Assertions): See Linux Programmer's Manual [ assert.cat ] [ assert.html ] [ assert.man ]

Experiment with assertion driven coding: DiscountsR'Us Case study [ discounts.cpp ]

Demonstration of assertions in action [ isqrt0.cpp ] [ isqrtdemo0.cpp ] [ isqrtdemo.cpp ]

(Case Study): Discounts'RUs [ discounts.html ] [ discounts.mth ] [ discounts.plg ] (Prolog), [ discounts.cpp ] (assertion driven C++).

(Requirements): See DiscountsR'Us [ discounts.html ] [ discounts.mth ]

(puzzles): See [ Potions.htm ]

• Figure 2.2 of RobertsonAgusti 99 [ fig22.html ] [ fig22.mth ] [ fig22.txt ]

• Ross Ashby's Haunted House Problem [ haunting.smv ]

• Knights, normals and spies [ kns1.html ] [ kns1.mth ]

• The Lunch example [ lunch.html ] [ lunch.mth ] [ lunch.txt ]

(lambda): Lambda Calculus [ lambda.mbox ]

(proofs): Book's logic translating into MATHS [ logic.html ] [ logic.m ] [ logic.mth ]

(MATHS): My MATHS formal language [ maths.html ] [ maths.mth ]

(Hoare): Hoare's Axiomatic Paper [ p576-hoare.pdf ]

(Parnas): Parnas [ Parnas.txt ]

(prolog): Prolog Examples [ prolog ]

(PVS): Practical Verifier System. If you like Emacs this looks like a useful tool. Try this command

` 		~dick/cs556/pvs/pvs`
to see what I mean. I've published a local set of PVS sources [ pvs ]

Also see John Rushby's examples [ http://www.csl.sri.com/users/rushby/slides/pvs-examples/ ] and the SRI PVS page [ http://www.csl.sri.com/projects/pvs/ ] and the SRI formal methods page [ http://www.csl.sri.com/programs/formalmethods/ ]

(SMVprogram): SMV stuff [ smv ] [ ring.smv ]

(SCR): Software Cost reduction [ SCR ]

(truth_tables): Truth tables in C++ [ tf.cpp ]

(BNF): GoodsTrain Example [ train2.html ] [ train2.mth ] [ train.html ] [ train.mth ]

(news): News item in Business Week about profitable mathematics: [ nf20020122_8839.htm ]

. . . . . . . . . ( end of section Formal Methods Web Site) <<Contents | Index>>