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

Contents

    Links to resources on Formal Methods

    References

    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 ]


    (MATHS): [ http://www.csci.csusb.edu/dick/maths/ ]


    (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:

    Research

    Jokes

    Other
    (Math for profit): [ nf20020122_8839.htm ]

    [ ideas.html ]

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

Formulae and Definitions in Alphabetical Order