Title | Toward Zero-Defect Programming |
Author | Allan M. Stavely |
Publication Info | Addison Wesley Longman, 1999. ISBN 0-201-38595-3. |
Course Type | Software Engineering, Software Verification |
Notes | Toward Zero-Defect Programming describes current methods for writing (nearly) bug-free programs. These methods are based on practices developed at IBM and elsewhere under the name Cleanroom Software Engineering. The author shows how these methods can be applied in three key areas of software development:
Requiring formal or semi-formal specifications, and programming so that the code can be shown to agree with the specifications, forces software engineers to program more simply and more clearly, eliminating many defects as a consequence. Performing verification as part of a team process uncovers additional defects and encourages careful examination of the program for efficiency and other quality aspects. Testing the program, to compensate for human fallibility in the preceding steps, catches (nearly) all remaining bugs. The author departs somewhat from IBM Cleanroom methods in simplifying the procedures that readers must learn. His aim is to make specification and verification readily accessible to any student or practitioner who can write well-structured programs. No great mathematical sophistication is assumed. Although the book's examples are written in a number of programming languages to explain different points, the largest number are in C; therefore, a prior knowledge of C is useful. (adapted from the blurb on the back cover) |
Title | A Logical Approach to Discrete Math |
Author | David Gries and Fred B. Schneider |
Publication Info | Springer Verlag, 1993 |
Course Type | Logic, Introductory Computer Science, Software Engineering |
Notes | This text, though 7 years old, is the only text for discrete math course that teaches "logic as a tool". A course using it would devote 6 weeks to teaching a calculation logic. Along the way, students learn strategies for developing proofs and prove some 30-40 real theorems in propositional and predicate logic. Thereafter, students USE this logic and its notation in dealing with sets, a theory of integers, combinatorics, proofs of program correctness, and the like. Students LIKE this material because it finally presents a notion of proof that can be learned and put to use in many fields. They come away with a skill in formal manipulation and less fear of mathematics, in general. And many of them tend to use what they learned in other courses. The text looks forbidding. But if one approaches logic with the idea of teaching a useful SKILL, rather than with the idea of teaching facts, the students embraces the text and the course. |
Title | Logic in Computer Science: Modelling and Reasoning about Systems |
Author | Michael Huth and Mark Ryan |
Publication Info | Cambridge University Press, 2000 |
Course Type | Logic, Software Verification, Hardware Verification, Modelling systems |
Notes | Foreword by
Edmund M. Clarke
FORE Systems Professor of Computer Science
Carnegie Mellon University
Pittsburgh, PA
Formal methods have finally come of age! Specification languages,
theorem provers, and model checkers are beginning to be used routinely
in industry. Mathematical logic is basic to all of these techniques.
Until now textbooks on logic for computer scientists have not kept
pace with the development of tools for hardware and software
specification and verification. For example, in spite of the success
of model checking in verifying sequential circuit designs and
communication protocols, until now I did not know of a single text,
suitable for undergraduate and beginning graduate students, that attempts
to explain how this technique works. As a result, this material is rarely
taught to computer scientists and electrical engineers who will need
to use it as part of their jobs in the near future. Instead, engineers
avoid using formal methods in situations where the methods would be of
genuine benefit or complain that the concepts and notation used by the
tools are complicated and unnatural. This is unfortunate since the
underlying mathematics is generally quite simple, certainly no more
difficult than the concepts from mathematical analysis that every
calculus student is expected to learn.
Logic in Computer Science by Huth and Ryan is an exceptional book. I was amazed when I looked through it for the first time. In addition to propositional and predicate logic, it has a particularly thorough treatment of temporal logic and model checking. In fact, the book is quite remarkable in how much of this material it is able to cover: linear and branching time temporal logic, explicit state model checking, fairness, the basic fixpoint theorems for computation tree logic (CTL), even binary decision diagrams and symbolic model checking. Moreover, this material is presented at a level that is accessible to undergraduate and beginning graduate students. Numerous problems and examples are provided to help students master the material in the book. Since both Huth and Ryan are active researchers in logics of programs and program verification, they write with considerable authority. In summary, the material in this book is up-to-date, practical, and elegantly presented. The book is a wonderful example of what a modern text on logic for computer science should be like. I recommend it to the reader with greatest enthusiasm and predict that the book will be an enormous success. |
Title | Modelling Systems: Practical Tools and Techniques in Software Development |
Author | John Fitzgerald and Peter Gorm Larsen |
Publication Info | Cambridge University Press, 1998, ISBN 0521 623480 |
Course Type | Introductory Computer Science, Software Engineering, Development of formal models (VDM) |
Title | How to Design Programs |
Author | Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi |
Publication Info | (unpublished manuscript) |
Course Type | Introductory Computer Science |
Notes | This book presents a methodological, pattern-based approach to introductory programming. It uses Scheme to minimize syntactic overhead, but the ideas apply equally well to other languages, such as Java. The book has a companion programming environment, DrScheme, which offers several pedagogic benefits. Both are available at no cost. |
Title | Programming from Specifications 2/e |
Author | Carroll Morgan |
Publication Info | Prentice Hall 1990, 1994 (now out of print) |
Course Type | Software Engineering, Software Verification |
Notes | The text explains the "Refinement Calculus" as related to elementary procedural programming, and makes the link between "weakest-precondition style" progam development and "Z/VDM style" specification. |
Title | Higher Order Logic and Hardware Verification |
Author | Tom Melham |
Publication Info | Cambridge Tracts in Theoretical Computer Science 31 (Cambridge University Press, 1993) |
Course Type | Hardware Verification |
Title | new_theory `HOL`;; An Introduction to Hardware Verification in Higher Order Logic |
Author | Graham Birtwistle, Shiu-Kai Chin, Brian Graham |
Publication Info | On-line draft |
Course Type | Hardware Verification |
Title | Computer-Aided Verification. An Introduction to Model Building and Model Checking for Concurrent Systems |
Author | Rajeev Alur and Thomas A. Henzinger |
Publication Info | Draft. Contact the authors. |
Course Type | Hardware Verification |
Title | The Temporal Logic of Reactive and Concurrent Systems. Volume 1 (Specification) |
Author | Zohar Manna and Amir Pnueli |
Publication Info | Springer-Verlag. 1992. ISBN 0-387-97664- |
Course Type | Software Verification, Hardware Verification |
Title | Principles of Programming Languages |
Author | Shriram Krishnamurthi and Matthias Felleisen |
Publication Info | Rice University Computer Science TR 97-292 |
Course Type | Programming Languages |
Notes | Covers programming language principles using a sequence of definitional interpreters. Includes material on modelling state, control and memory management. Covers type systems including polymorphism. |
Title | Computation and Deduction |
Author | Frank Pfenning |
Publication Info | Lecture Notes, submitted for publication as textbook |
Course Type | Logic, Type Theory, Theory of Programming Languages |
Notes | Provides an introduction to logic, type theory, reasoning about programs, and programming languages using the logical framework Twelf as a tool |
Title | BRICS Autumn School Lecture Notes on Verification |
Author | various researchers |
Publication Info | Available on-line |
Course Type | Hardware Verification |
Title | An International Survey of Industrial Applications of Formal Methods,Volume 2 Case Studies |
Author | Craigen, Dan, Susan Gerhart, and Ted Ralston, |
Publication Info | NIST GCR 93/626, March 1993, National Institute of Standards and Technology |
Course Type | Software Engineering, Software Verification, Hardware Verification |
Notes | Volume 2 of 2 volume set Text version available at: ftp://hissa.ncsl.nist.gov/pub/formal_methods/vol2.txt |
Title | An International Survey of Industrial Applications of Formal Methods, Vol.1 |
Author | Craigen, Dan, Susan Gerhart, and Ted Ralston, |
Publication Info | NIST GCR 93/626, March 1993, National Institute of Standards and Technology |
Course Type | Software Engineering, Software Verification, Hardware Verification |
Notes | Text version available at: ftp://hissa.ncsl.nist.gov/pub/formal_methods/vol1.txt |
Title | Formal Methods: State of the Art and Future Directions |
Author | E. Clarke and J. Wing |
Publication Info | CMU Computer Science Technical Report . CMU-CS-96-178, August 1996. (22 pages, 123 references.) |
Course Type | Software Verification, Hardware Verification |
Title | Formal Methods in Computing |
Author | Ferenczi, M., Pataricza, A., Ronyai, L. |
Publication Info | Akademiai Kiado, Kluwer, 2005, p.436, ISBN 9630582589 |
Course Type | Logic, Introductory, Software Engineering |
Title | Formal Specification and Verification of Control Software for Cryptographic Equipment |
Author | D.R. Kuhn and J.F. Dray |
Publication Info | Proceedings, Annual Computer Security Applications Conference, IEEE Computer Society Press, 1990. |
Course Type | Software Engineering, Software Verification |
Notes | Case study, formal verification using FDM; includes data on hours required for verification and for complete project. |
Title | Formal Verification in a Commercial Setting |
Author | R.P. Kurshan |
Publication Info | Proc. DAC'97 Anaheim, California, June 9-13, 1997, pp 258-262 |
Course Type | Hardware Verification |
Title | Cyrix 6x86 Bug Puts Brakes on NT 4.0 |
Author | Robert L. Hummel |
Publication Info | Byte Magazine, 21(11):30,32, November 1996 |
Course Type | Hardware Verification |
Title | An Investigation of the Therac-25 Accidents |
Author | Nancy G. Leveson and Clark S. Turner |
Publication Info | IEEE Computer, 26(7):18-41, July 1993 |
Course Type | Software Engineering, Software Verification, Hardware Verification |
Title | High Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS)... with Lots on Formal Methods |
Author | David A. Wheeler |
Publication Info | online |
Course Type | Software Engineering, Software Verification |
This site is currently maintained by Kathi Fisler Department of Computer Science, Worcester Polytechnic Institute Last updated on Thursday, 10-Aug-2006 09:36:31 EDT Acknowledgements |