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

Links to resources on Formal Methods

Logics

1. PC::=Propositional Calculus, foundation of nearly all other logics formulae are constructed from atomic propositions by operators acting like and, or, if_then, not, etc.

2. LPC::=Lower Predicate Calculus, A predicate is a property of objects in a Universe of Discourse. Predicate calculus includes PC but defines special atomic propositions and additional operators for all, for some, etc.

3. LTL::=Linear Temporal Logic.

4. Temporal_Logic::=Logic for expressing changing properties, for example [ tl.html ]

5. CTL::=Compter Tree Logic, PC with 8 new modal operators that quantify possible and necessary futures.

If you can handle Dutch.... [ http://turing.wins.uva.nl/~jaspars/animations/ ] ( EN = /\, NIET= not, OF = \/ , alsdan = if_then, desda=iff, noch = not iff)

(Proofs): [ A0840257.html ]

(Tableaux): Research [ http://i12www.ira.uka.de/TABLEAUX/ ] , Notes [ Semantic Tableaux in logic_2_Proofs ] , and Cheat Sheet [ semtab.jpg ] Math [ contents.cgi ]

(Prolog): Programming in Logic: [ prolog.html ]

(Verification): TOny Hoare starts the ball rolling in the 1960s: [ 363235.363259 ]

(OBDDs): Examples of OBDDs [ http://indy4.fdl.cc.mn.us/obdd/ ] and other DDs: [ demo.html ]

Tutorials and Classes

(LICS web tutor): LICS has a tutorial: [ index.html ] [ home.html ]

Paul Black and Anne Sobel presented: [ formaltut.html ]

Tools

(SMV): http://www.csci.csusb.edu/dick/cs656/smv

One popular tool for computer people is the Prototype Verification System:

6. PVS::= See http://pvs.csl.sri.com/, at SRI.

(SPIN): A tool that checks sytems expressed in Promela to see if the meet LTL specifications: [ whatispin.html ]

(Promela): Process or Protocol Meta Language: [ promela.htm ] , The Concise Promela Reference.

(prolog): [ project2.html ]

Books

(textbook): LICS

Logic, proofs by trees:

• Richard Jeffreys
• Formal Logic: It's Scope and Limits
• McGraw-Hill Education

Other

(Math for profit): [ nf20020122_8839.htm ]

Glossary

7. LICS::="Logic In Computer Science", [ http://www.cis.ksu.edu/~huth/lics/ ]
8. TBA::="To Be Announced".

Other

(LISP): [ lisp.html ]

(TeX): [ comp.text.TeX.html ]

. . . . . . . . . ( end of section Links to resources on Formal Methods) <<Contents | Index>>