Formal Methods

The applied mathematics of computer system engineering used to specify and model the behavior of a system and to mathematically verify that the system design and implementation satisfy system functional and safety properties.

All categories

Books under this sub-category (22 books)

A Practical Theory of Programming, Second Edition

Post date: 28 Nov 2004
Describes theory of programming as something that will provide a much greater degree of precision by providing a method of calculation to software engineers.
Publication date: 31 Dec 2004
 
A Practical Theory of Programming, Second Edition

A Practical Theory of Programming, Second Edition

Post date: 28 Nov 2004
Describes theory of programming as something that will provide a much greater degree of precision by providing a method of calculation to software engineers.
Publication date: 31 Dec 2004


Automated Theorem Proving

Post date: 12 Mar 2007
Gives students a thorough understanding of the central techniques in automated theorem proving, enabling them to transfer methods to different logics or applications.
Publication date: 20 Jan 2004
 
Automated Theorem Proving

Automated Theorem Proving

Post date: 12 Mar 2007
Gives students a thorough understanding of the central techniques in automated theorem proving, enabling them to transfer methods to different logics or applications.
Publication date: 20 Jan 2004


Case Studies in Systematic Software Development

Post date: 18 Jun 2005
Covers the case studies on the application of the most widely known and used formal methods in software development, called the Vienna Development Method or VDM.
Publisher: Prentice Hall
Publication date: 31 Dec 1990
 
Case Studies in Systematic Software Development

Case Studies in Systematic Software Development

Post date: 18 Jun 2005
Covers the case studies on the application of the most widely known and used formal methods in software development, called the Vienna Development Method or VDM.
Publisher: Prentice Hall
Publication date: 31 Dec 1990


Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant

Post date: 13 Nov 2016
This textbook covers practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.
Publisher: The MIT Press
Publication date: 30 Jun 2016
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported
Document Type: Textbook
 
Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant

Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant

Post date: 13 Nov 2016
This textbook covers practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.
Publisher: The MIT Press
Publication date: 30 Jun 2016
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported Document Type: Textbook


Communicating Sequential Processes

Post date: 07 Nov 2005
This is an excellent introduction to Communicating Sequential Processes, or CSP, a language for describing patterns of interaction, and also to its mathematical theory.
Publisher: Prentice Hall
Publication date: 30 Nov -0001
 
Communicating Sequential Processes

Communicating Sequential Processes

Post date: 07 Nov 2005
This is an excellent introduction to Communicating Sequential Processes, or CSP, a language for describing patterns of interaction, and also to its mathematical theory.
Publisher: Prentice Hall
Publication date: 30 Nov -0001


Data, Syntax and Semantics - An Introduction to Modelling Programming Languages

Post date: 22 Sep 2006
An introduction to the mathematical theory of programming languages. Readers will need a first course in elementary set theory, logic and imperative programming as the background knowledge.
Publication date: 01 Jan 2006
 
Data, Syntax and Semantics - An Introduction to Modelling Programming Languages

Data, Syntax and Semantics - An Introduction to Modelling Programming Languages

Post date: 22 Sep 2006
An introduction to the mathematical theory of programming languages. Readers will need a first course in elementary set theory, logic and imperative programming as the background knowledge.
Publication date: 01 Jan 2006


Denotational Semantics: A Methodology for Language Development

Post date: 12 Oct 2006
Introduces a methodology for giving mathematical meaning to programming languages and systems. Presents the topic from an engineering viewpoint, emphasizing the descriptional and implementational aspects.
Publisher: McGraw-Hill
Publication date: 31 Dec 1986
License: Creative Commons Attribution 2.0 Generic
Document Type: Book
 
Denotational Semantics: A Methodology for Language Development

Denotational Semantics: A Methodology for Language Development

Post date: 12 Oct 2006
Introduces a methodology for giving mathematical meaning to programming languages and systems. Presents the topic from an engineering viewpoint, emphasizing the descriptional and implementational aspects.
Publisher: McGraw-Hill
Publication date: 31 Dec 1986
License: Creative Commons Attribution 2.0 Generic Document Type: Book


forall x: An Introduction to Formal Logic

Post date: 06 May 2017
An open access introductory textbook in formal logic. It covers translation, proofs, and formal semantics for sentential and predicate logic.
Publisher: Lulu.com
Publication date: 06 Jan 2012
License: Creative Commons Attribution-ShareAlike 3.0 Unported
Document Type: Textbook
 
forall x: An Introduction to Formal Logic

forall x: An Introduction to Formal Logic

Post date: 06 May 2017
An open access introductory textbook in formal logic. It covers translation, proofs, and formal semantics for sentential and predicate logic.
Publisher: Lulu.com
Publication date: 06 Jan 2012
License: Creative Commons Attribution-ShareAlike 3.0 Unported Document Type: Textbook


Formal Specification and Documentation using Z: A Case Study Approach

Post date: 11 Jun 2005
Presents a pragmatic view of the use of formal methods, that it can still be beneficial (and is much more cost effective in general) than attempting proofs in many cases.
Publisher: Thomson Publishing
Publication date: 01 Feb 1996
 
Formal Specification and Documentation using Z: A Case Study Approach

Formal Specification and Documentation using Z: A Case Study Approach

Post date: 11 Jun 2005
Presents a pragmatic view of the use of formal methods, that it can still be beneficial (and is much more cost effective in general) than attempting proofs in many cases.
Publisher: Thomson Publishing
Publication date: 01 Feb 1996


Foundations of Computation, Second Edition

Post date: 28 Oct 2016
A free textbook for a one-semester course in theoretical computer science. It has been used for several years in a course at Hobart and William Smith Colleges. The course has no prerequisites other than introductory computer programming.
Publication date: 31 Dec 2011
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported
Document Type: Textbook
 
Foundations of Computation, Second Edition

Foundations of Computation, Second Edition

Post date: 28 Oct 2016
A free textbook for a one-semester course in theoretical computer science. It has been used for several years in a course at Hobart and William Smith Colleges. The course has no prerequisites other than introductory computer programming.
Publication date: 31 Dec 2011
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported Document Type: Textbook


How to Think About Algorithms - Loop Invariants and Recursion

Post date: 09 Oct 2006
These notes teach the students to think abstractly about algorithms and about the key algorithmic techniques used to develop them.
Publisher: Cambridge University Press
Publication date: 01 Feb 2008
 
How to Think About Algorithms - Loop Invariants and Recursion

How to Think About Algorithms - Loop Invariants and Recursion

Post date: 09 Oct 2006
These notes teach the students to think abstractly about algorithms and about the key algorithmic techniques used to develop them.
Publisher: Cambridge University Press
Publication date: 01 Feb 2008


Introduction to Programming Languages

Post date: 24 Oct 2004
An undergraduate text in the theory of programming languages.
Publication date: 15 Jul 2004
License: Creative Commons Attribution 2.0 Generic
Document Type: Textbook
 
Introduction to Programming Languages

Introduction to Programming Languages

Post date: 24 Oct 2004
An undergraduate text in the theory of programming languages.
Publication date: 15 Jul 2004
License: Creative Commons Attribution 2.0 Generic Document Type: Textbook


Lecture Notes on Semantics of Programming Languages

Post date: 12 Dec 2006
Introduces the structural, operational approach to programming language semantics.
Publication date: 01 Jan 2002
Document Type: Lecture Notes
 
Lecture Notes on Semantics of Programming Languages

Lecture Notes on Semantics of Programming Languages

Post date: 12 Dec 2006
Introduces the structural, operational approach to programming language semantics.
Publication date: 01 Jan 2002
Document Type: Lecture Notes


Principles of Programming Languages

Post date: 29 Aug 2016
An introduction to the study of programming languages that evolved from lecture notes used in a programming languages course for students at Johns Hopkins University.
Publication date: 01 Jan 2016
License: Creative Commons Attribution-ShareAlike 3.0 United States
Document Type: Book
 
Principles of Programming Languages

Principles of Programming Languages

Post date: 29 Aug 2016
An introduction to the study of programming languages that evolved from lecture notes used in a programming languages course for students at Johns Hopkins University.
Publication date: 01 Jan 2016
License: Creative Commons Attribution-ShareAlike 3.0 United States Document Type: Book


Programming from Specifications

Post date: 26 Nov 2004
Presents a rigorous treatment of most elementary program-development constructs, including iteration, recursion, procedures, parameters, modules and data refinement.
Publisher: Prentice Hall
Publication date: 31 Dec 1998
 
Programming from Specifications

Programming from Specifications

Post date: 26 Nov 2004
Presents a rigorous treatment of most elementary program-development constructs, including iteration, recursion, procedures, parameters, modules and data refinement.
Publisher: Prentice Hall
Publication date: 31 Dec 1998


Book Categories
Sponsors
Icons8, a free icon pack