@string{JSC="Journal of Symbolic Computation"}
@incollection{Amarel,
author = "Saul Amarel",
title = "On representation of problems of reasoning about action",
pages = "131-171",
booktitle = "Machine Intelligence 3",
editor = "Donald Michie",
publisher = "Edinburgh University Press",
year = "1971"}
@inproceedings{CoudertBerthetMadre,
editor = "J. Sifakis",
author = "Olivier Coudert and Christian Berthet and Jean Christophe Madre",
title = "Verification of synchronous sequential machines
based on symbolic execution",
booktitle = "Automatic Verification Methods for Finite State Systems",
year = 1989,
publisher = "Springer-Verlag",
pages = {365-373},
number = "407",
series = {Lecture Notes in Computer Science}}
@Book{charniak80,
author = {E. Charniak and C. K. Riesbeck and D. V. McDermott},
title = {Artificial Intelligence Programming},
publisher = {Lawrence Erlbaum Associates},
year = 1980}
@mastersthesis{WingSangLee,
author = "Lee, Wing Sang",
title = "{ST} to {FL} translation for hardware design verification",
school = {The University of British Columbia},
month = "April",
year = "1994"}
@techreport{LeeGreenstreetSeger,
author = "Trevor W.~S.~Lee and Mark R.~Greenstreet and Carl-Johan Seger",
title = "Automatic Verification of Asynchronous Circuits",
institution = {The University of British Columbia},
number = {UBC TR~93-40},
month = "November",
year = "1993"}
@inproceedings{aagaard-iccad-95,
author = {Aagaard, Mark D. and Seger, Carl-Johan H.},
title = {The Formal Verification of a
Pipelined Double-Precision {IEEE} Floating-Point
Multiplier},
booktitle = iccad,
pages = {7-10},
year = 1995,
month = nov,
publisher = ieee-computer-society,
}
@incollection{hazelhurst-kropfbook-97,
author = {Hazelhurst, Scott and Seger, Carl-Johan H.},
title = {Symbolic Trajectory Evaluation},
booktitle = {Formal Hardware Verification},
publisher = {Springer-Verlag},
year = 1997,
chapter = 1,
pages = {3-78},
editor = {Kropf, Thomas},
}
@TECHREPORT{harrison-style,
author = "John Harrison",
title = "Floating point verification in {HOL} {L}ight:
the exponential function",
institution = "University of Cambridge Computer Laboratory",
address = "New Museums Site, Pembroke Street,
Cambridge, CB2 3QG, UK",
year = 1997,
type = "Technical Report",
number = 428,
note = "Available on the Web as
{\verb+http://www.cl.cam.ac.uk/users/jrh/papers/tang.html+}"}
@Article{oleary-itj-99,
author = {O'Leary, John and Zhao, Xudong and Gerth, Robert and
Seger, Carl-Johan H.},
title = {Formally Verifying {IEEE} Compliance of Floating-Point
Hardware},
journal = {Intel Technology Journal},
year = 1999,
month = {First Quarter},
note = {Online at {\tt{http://developer.intel.com/technology/itj/}}}
}
@techreport{SegerVoss,
author = "Carl-Johan H. Seger",
title = {Voss - A Formal Hardware Verification System: User's Guide},
institution = {The University of British Columbia},
number = {UBC TR~93-45},
month = "December",
year = "1993"}
@techreport{McMillan99,
author = "K. L. McMillan",
title = {A methodology for hardware verification using compositional model checking},
institution = {Cadence Berkeley Labs},
month = "April",
note = {Available at {\tt{http://www-cad.eecs.berkeley.edu/${\sim}$kenmcmil/}}},
year = "1999"}
@INPROCEEDINGS{aagaard-tphols-99,
AUTHOR = {Aagaard , Mark D. and Jones , Robert B. and Seger , Carl-Johan H. },
TITLE = "{Lifted-FL: A Pragmatic Implementation of Combined Model
Checking and Theorem Proving}",
BOOKTITLE = {Theorem Proving in Higher Order Logics (TPHOLs99)},
YEAR = {1999},
publisher = "Springer-Verlag",
pages = {323-340},
number = "1690",
series = {Lecture Notes in Computer Science},
}
@inproceedings{aagaard-dac-98,
author = {Aagaard, Mark D. and Jones, Robert B. and Seger, Carl-Johan
H.},
title = {Combining Theorem Proving and Trajectory Evaluation
in an Industrial Environment},
booktitle = {Design Automation Conference (DAC)},
year = 1998,
month = "July",
pages = {538-541},
organization = {ACM/IEEE},
}
@techreport{ButlerAutopilot,
author = "Ricky W. Butler",
title = "An Introduction to Requirements
Capture using {PVS}: Specification of a Simple Autopilot",
institution = {NASA},
number = {TR 110255},
month = "May",
year = "1996"}
@techreport{YoungAutopilot,
author = "William D. Young",
title = "The Specification of a Simple Autopilot in {ACL2}",
institution = {Computational Logic Inc},
number = {CLI Internal Note \#327},
month = "July",
year = "1996"}
@misc{HoareFest,
author = "Mike Gordon",
title = {Programming combinations of deduction and {BDD}-based symbolic calculation},
note = {Draft available at
{\tt http://www.cl.cam.ac.uk/${\sim}$mjcg/celebration/}}
}
@misc{GordonVerilogSemantics,
author = "Mike Gordon",
title = {Synthesizable Verilog: syntax and semantics},
note = {Draft available at
{\tt http://www.cl.cam.ac.uk/users/mjcg/Verilog/V/V.ps.gz}}
}
@incollection{JoyceSeger,
author = "J. Joyce and C. Seger",
title = "{The HOL-Voss System: Model-Checking
inside a General-Purpose Theorem-Prover}",
booktitle = {Higher Order Logic
Theorem Proving and its Applications: 6th International
Workshop, HUG'93, Vancouver, B.C., August 11-13 1993},
editor = {J. J. Joyce and C.-J. H. Seger},
year = 1994,
publisher = "Spinger-Verlag",
pages = {185-198},
volume = "780",
series = {Lecture Notes in Computer Science}
}
@misc{HenrikNotes,
author = "Henrik Reif Andersen",
title = "{An Introduction to Binary Decision Diagrams}",
year = 1997,
month = "October",
organization ="Department of Information Technology, Technical University of Denmark,
Building 344, DK-2800 Lyngby, Denmark",
note ="Lecture notes for 49285 Advanced Algorithms E97.
Available from: {\tt{http://www.it.dtu.dk/${\sim}$hra}}"
}
@misc{PaulsonMiniscoping,
key = "Paulson",
note = {Larry Paulson, private communication.}
}
@book{EdinLCF,
author = {M. J. C. Gordon and R. Milner and C. P. Wadsworth},
title = {{Edinburgh LCF}: A Mechanised Logic of Computation},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 78,
year = 1979
}
@book{McMillanBook,
author = {Kenneth L. McMillan},
title = {Symbolic Model Checking},
publisher = {Kluwer Academic Publishers},
year = 1993
}
@book{ClarkeBook,
author = {Edmund M. Clarke Jr. and Orna Grumberg},
title = {Model Checking},
publisher = {The MIT Press},
year = 1999
}
@misc{PVS,
key = "PVS",
note = {See web page {\tt http://www.csl.sri.com/pvs.html}}
}
@misc{Prosper,
key = "Prosper",
note = {See web page {\tt http://www.dcs.gla.ac.uk/prosper/}}
}
@misc{BuDDy,
key = "Lind",
note = {J{\o}rn Lind-Nielsen's BuDDy
package is documented at {\tt http://www.itu.dk/research/buddy/}}
}
@inproceedings{Rajan95:CAV,
TITLE = {An Integration of Model-Checking with Automated Proof
Checking},
AUTHOR = {S. Rajan and N. Shankar and M.K. Srivas},
BOOKTITLE = {Computer-Aided Verification, CAV '95},
EDITOR = {Pierre Wolper},
PAGES = {84--97},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 939,
MONTH = jun,
YEAR = 1995,
ADDRESS = {Liege, Belgium}
}
@InCollection{basin98:_combin_ws1s_hol,
author = {Basin, David and Friedrich, Stefan},
title = {Combining {WS1S} and {HOL}},
booktitle = {Frontiers of Combining Systems, Second International
Workshop, Amsterdam, September 1998},
publisher = {Kluwer Academic Publishers},
year = 1998,
series = {Applied Logic Series},
note = {To appear}
}
@techreport{Butler96:rqts,
TITLE = {An Introduction to Requirements Capture Using {PVS}:
Specification of a Simple Autopilot},
AUTHOR = {Ricky W. Butler},
TYPE = {NASA Technical Memorandum},
NUMBER = 110255,
MONTH = may,
YEAR = 1996,
INSTITUTION = {NASA Langley Research Center},
ADDRESS = {Hampton, VA}
}
@article{Milner-types,
author = {R. Milner},
title = {A Theory of Type Polymorphism in Programming},
journal = {Journal of Computer and System Sciences},
volume = {17},
number = {3},
pages = {348-375},
month = {December},
year = {1978}
}
@incollection{BoyerMooreLinearArith,
author = "R. S. Boyer and J Moore",
title = "Integrating Decision Procedures into Heuristic Theorem Provers:
A Case Study of Linear Arithmetic",
pages = "83-124",
booktitle = "Machine Intelligence 11",
publisher = "Oxford University Press",
year = "1988"}
@article{BryantSurvey,
author = {Randall E. Bryant},
title = {Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams},
journal = {ACM Computing Surveys},
volume = {24},
number = {3},
pages = {293-318},
month = {September},
year = {1992}
}
@PhDThesis{RJBPhDThesis,
author = "R. J. Boulton",
title = "Efficiency in a Fully-Expansive Theorem Prover",
school = "University of Cambridge Computer Laboratory",
year = "1994",
address = "New Museums Site, Pembroke Street, Cambridge CB2 3QG, U.K.",
month = "May",
note = "Technical Report 337."}
@techreport{boulton92b,
author = {R. J. Boulton},
title = {On efficiency in theorem provers which fully expand proofs into
primitive inferences},
institution = {University of Cambridge Computer Laboratory},
year = {1992},
month = {February},
number = {248},
note = {This report is based on Richard Boulton's PhD thesis.}
}
@techreport{mjcg99a,
author = {Mike Gordon},
title = {Programming combinations of deduction and {BDD}-based
symbolic calculation },
institution = {University of Cambridge Computer Laboratory},
year = {1999},
month = {December},
number = {480},
}
@techreport{GordonLarsen,
author = {Mike Gordon and Ken Friis Larsen},
title = {Combining the {Hol98} Proof Assistant with
the {BuDDy} {BDD} package},
institution = {University of Cambridge Computer Laboratory},
year = {1999},
month = {December},
number = {481},
}
@book{GordonMelham,
editor = {M. J. C. Gordon and T. F. Melham},
title = {Introduction to HOL:
a theorem-proving environment for higher-order logic},
publisher = {Cambridge University Press},
year = {1993}
}
@book{MelhamBook,
editor = {T. F. Melham},
title = {Higher Order Logic and Hardware Verification},
publisher = {Cambridge University Press},
series = {Cambridge Tracts in Theoretical Computer Science 31},
year = 1993
}
@InCollection{WhyHOL,
author = "Mike Gordon",
editor = "G. Milne and P. A. Subrahmanyam",
title = "Why higher-order logic is a good formalism for specifying
and verifying hardware",
booktitle = "Formal Aspects of VLSI Design",
pages = "153--177",
publisher = "North-Holland",
year = 1986}
@InProceedings{SemanticChallenge,
Author = "Mike Gordon",
title = "The Semantic Challenge of {Verilog} {HDL}",
booktitle = "Tenth Annual IEEE Symposium on Logic in Computer Science",
place = "San Diago, California, USA",
dates = "26--29 June",
publisher = "{IEEE Computer Society Press}",
year = "1995",
pages = "136--145",
}
@INPROCEEDINGS{tphols2000-Gordon,
editor = "J. Harrison and M. Aagaard",
booktitle = "Theorem Proving in Higher Order Logics:
13th International Conference, TPHOLs 2000",
series = "Lecture Notes in Computer Science",
volume = 1869,
year = 2000,
publisher = "Springer-Verlag",
title = "Reachability programming in {HOL} using {BDD}s",
author = "Michael J.~C.~Gordon",
pages = "180--197"}
@InProceedings{Gordon:TPHOLs2000,
Author = "Mike Gordon",
title = "Reachability programming in {HOL98} using {BDDs}",
booktitle = "The 13th International Conference on Theorem Proving and Higher Order Logics",
place = "DoubleTree Hotel, Portland, Oregon, USA",
dates = "14 -- 18 August",
publisher = "{Springer-Verlag}",
year = "2000",
}
@Book{Isabelle-book,
author = "Lawrence C. Paulson",
title = "Isabelle: A Generic Theorem Prover",
publisher = "Springer-Verlag",
year = 1994,
volume = "828",
series = {Lecture Notes in Computer Science}}
@Article{paulson-jcs,
author = {Lawrence C. Paulson},
title = {The Inductive Approach to Verifying Cryptographic Protocols},
journal = {Journal of Computer Security},
year = 1998,
volume = 6,
pages = {85-128}}
@Book{Back,
author = "Ralph-Johan Back and Joakim von Wright",
title = "Refinement Calculus: A Systematic Introduction",
publisher = "Springer-Verlag",
year = 1998,
series = {Graduate Texts in Computer Science}}
@Book{Morgan,
author = {Carroll Morgan},
title = "Refinement Calculus: A Systematic Introduction",
publisher = "Prentice Hall",
year = 1990,
series = {Prentice Hall International Series in Computer Science}}
@InCollection{Hanna,
author = {F. K. Hanna and M Longley and N Daeche},
editor = {L. J. M. Claesen},
title = {Formal synthesis of digital systems},
booktitle = {Applied formal methods for correct VLSI design},
publisher = {North-Holland},
year = 1989,
pages = "153--169"
}
@inproceedings{Fourman,
author = "Finn, S. and Fourman, M. P. and Francis, M. and Harris, R.",
title = "Formal System Design ---
Interactive Synthesis based on Computer-Assisted Formal Reasoning",
editor = "Claesen, L.",
booktitle = "Formal VLSI Specification and Synthesis",
publisher = "Elsevier",
year = 1990
}
@InProceedings{Curzon91,
author = "Paul Curzon",
title = "A Verified Compiler for a Structured Assembly Language",
booktitle = "Proceedings of the 1991 International Workshop on the {HOL}
Theorem Proving System and its Applications",
year = "1992",
editor = "Myla Archer and Jeffrey J. Joyce and Karl N. Levitt and
Phillip J. Windley",
publisher = "{IEEE} Computer Society Press",
}