Growing demands for the quality, safety, and security of software can only be satisfied by the rigorous application of formal methods during software design. Th

An overview of ATP techniques for the non-specialist, it discusses all the main approaches to proof: resolution, natural deduction, sequentzen, and the connecti

A handbook to the Coq software for writing and checking mathematical proofs, with a practical engineering focus. The technology of mechanized program verificati

A practical introduction to the development of proofs and certified programs using Coq. An invaluable tool for researchers, students, and engineers interested i

A one-stop reference, self-contained, with theoretical topics presented in conjunction with implementations for which code is supplied.