. . . . . . . . . ( 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 ]
(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 ]
(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/pvsto 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>>