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

Contents


    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)


    (Grading): See [ grading656 ]


    (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


Useful Links

[ links.html ] [ Links.html ] [ links.mth ] [ Links.mth ]

Topics for Papers/Presentations

[ 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 ]

[ enigma.cpp ] [ enigma2.cpp ]

  • 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>>


    Formulae and Definitions in Alphabetical Order