Online Computer Science Degree Guide: Formal Methods

Here are resources on formal methods and how they are used to translate formal language into mathematical formulas and systems. Mathematical methods are used because this type of analysis of a computer program is quite reliable. In addition, using a mathematical approach is easier to diagnose the precise hardware and software problems at hand. Formal methods are frequently used in systems where security and safety are the primary objectives. The following resource guide has links to information on specific formal methods as well as general information on what formal methods are, how they function, and why they’re important.

Specific Methods, Tools, and Notations

• ASM – information on applications of Abstract State Machines to different domains.
• ACL2 – a programming language used to model computer systems as well as a tool to help prove what the properties of those models are.
• ACSR – Algebra of Communicating Shared Resources is a timed process algebra for analyzing real-time system executions and synchronizations.
• GCSR – Graphical Communicating Shared Resources is the specification, modification, and analysis of real-time systems.
• VERSA – facilitates in the use of the AGCSR in the design and analysis of real-time systems.
• Action Semantics – a practical framework for semantic description, using a combination of the best operational, denotation, and algebraic semantics.
• Alloy Analyzer – a modeling language with links to tutorials and Alloy discussion forums.
• ADL – Assertion Definition Language is a high-level language that provides a formal grammar for the expression of programmatic statements.
• BDD – Binary Decision Diagrams is a method for verifying high-level descriptions of protocols.
• Boyer-Moore Theorem Power - overview of the history and function of the Boyer-Moore Theorem Power.
• CASL – the Common Algebraic Specification Language, links to its usage and design.
• CaféOBJ – the most advanced formal specification language with features from OBJ.
• Calculi for Mobile Processes – texts and tutorials for using this system.
• Coq Proof Assistant – an overview of what Coq is and how to get it.
• CWB – the Edinburgh Concurrency Workbench is a tool for exploring and verifying systems.
• DisCo - is a specification method for reactive systems, this page includes links to formal issues and publications in and of DisCo.
• DC – links to publications, courses and tool support for Duration Calculus.
• ESC – the Extended Static Checker is a programming tool that locates common run-time errors in Java programs.
• Extended ML – a guide for developing Standard ML programs.
• Ferma T – information on what this system is and how it operates including tutorials and download options.
• HyTech – this tool aids in analyzing embedded systems.
• IMPS – the Interactive Mathematical Proof System supplies computational data for conventional methods of mathematical reasoning.
• ITL – here is an overview of what Interval Temporal Logic is and how it functions.
• Isabelle – a proof assistant for expressing mathematical formulas in a formal language.
• JAPE – this is a tool for creating and developing interactive proof editors.
• JML – the Java Modeling Language is a type of specification language used to identify the performance of Java models.
• Kronos – is a tool that identifies and verifies real-time systems and expresses that data in TCTL temporal logic.
• Larch – is a group of sites that examine and analyze the different languages, methods, tools, and notations for formal specifications.
• LEGO – a proof assistant, this pages has links to an overview of what LEGO is and how it functions as well as links to courses and tutorials for how to use it.
• Lotos – Language Of Temporal Ordering Specification is a formal description technique FDT.
• MathSpad – an editor for creating articles that have a considerable amount of mathematical calculations.
• Maude – links to a Maude overview, documentation, and where to download this system.
• CRL – an algebraic language and tool set for studying the communicating processes with data.
• Mizar – an overview of Mizar including links to how to prepare Mizar articles.
• Model Checking – this is a process for identifying and verifying finite-state concurrent systems.
• Murphi – a description language using guarded commands repeated in an infinite loop.
• Nqthm – links to installation instructions as well as Nqthm-related news resources.
• NuPRL – a proof/program refinement logic project that applies computational mathematics and provides logic-based tools for automate programming.
• PEPA – Performance Evaluation Process Algebra, links to the group that created it, and software news
• Perfect Developer – a tool used for modeling and verifying software systems with formal proofs of correctness
• Petri Nets – links to online support services for those using Petri Nets.
• ProofPower – a toolbox for specification support comprised of a number of different packages.
• PVS – Prototype Verification System is a combination of a specification language and a theorem prover.
• RAISE – Rigorous Approach to Industrial Software Engineering, links to publications, courses, and tool support for this method.
• SME – information on the signal language, polychrony toolset and SME environment.
• Specware – a software development system for precisely specifying desired functionality of applications.
• SPIN – a software tool for formal verification of distributed software systems.
• Statestep – used in software engineering this tool is used both in outside computing procedures and in software development.
• STeP – the Stanford Temporal Prover, used in the formal verification of reactive, real-time and hybrid systems.
• TLA – the Temporal Logic of Actions is used to specify and analyze concurrent and reactive systems.
• TPS – Theorem Proving System, find overview, download options and papers and reviews of this system here.
• UNITY – a programming notation and logic for finding data information in parallel and distributed programs.
• VeriSoft – a tool for systematic software testing by searching for coordination problems and assertion violations in software.
• X-Machines - complete and comprehensive overview of the history and theory of X-machines and how they are used.