@string{brics = "{BRICS}"}
@string{daimi = "Department of Computer Science, University of Aarhus"}
@string{iesd = "Department of Computer Science, Institute
of Electronic Systems, Aalborg University"}
@string{rs = "Research Series"}
@string{ns = "Notes Series"}
@string{ls = "Lecture Series"}
@string{ds = "Dissertation Series"}
@techreport{BRICS-NS-96-15,
author = "{CoFI}",
title = "{CASL} -- The {CoFI Algebraic Specification
Language}; Tentative Design: Language Summary",
institution = brics,
year = 1996,
type = ns,
number = "NS-96-15",
address = daimi,
month = dec,
note = "34~pp",
abstract = "The Common Framework Initiative (CoFI) for
algebraic specification and development is an
international collaborative effort, coordinated
by Peter D. Mosses. This summary of the
tentative design of the CoFI Algebraic
Specification Language, CASL, is the basis for
closer investigation by various CoFI task
groups (Semantics, Tools, Methodology, Language
Design), after which a final CASL Design
Proposal will be made in Spring 1997.\bibpar
The language CASL is central to CoFI: it is a
reasonably expressive algebraic language for
specifying requirements and design for
conventional software. From CASL, simpler CoFI
languages (e.g., for interfacing with existing
tools) are to be obtained by restriction, and
CASL is to be incorporated in more advanced
CoFI languages (e.g., for specifying reactive
systems). CASL strikes a balance between
simplicity and expressiveness",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-NS-96-14,
author = "Mosses, Peter D.",
title = "A Tutorial on Action Semantics",
institution = brics,
year = 1996,
type = ns,
number = "NS-96-14",
address = daimi,
month = dec,
note = "46~pp. Tutorial notes for FME~'94 (Formal
Methods Europe, Barcelona, 1994) and FME~'96
(Formal Methods Europe, Oxford, 1996)",
abstract = "Action Semantics is useful for specifying
programming languages: documenting design
decisions, setting standards for
implementations, etc. This framework has
unusually good pragmatics, making
specifications easily accessible to
programmers. Thanks to its inherent modularity,
action semantics scales up smoothly to
describing practical, industrially-useful
languages.\bibpar
In this 1/2-day tutorial, action semantics is
explained, illustrated, and compared to other
frameworks such as VDM and RAISE",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@proceedings{BRICS-NS-96-13,
title = "Proceedings of the Second ACM SIGPLAN Workshop
on Continuations, CW~'97 {\em(ENS, Paris,
France, 14 January, 1997)}",
year = 1996,
editor = "Danvy, Olivier",
number = "NS-96-13",
series = ns,
address = daimi,
month = dec,
organization = brics,
note = "166~pp",
abstract = "The notion of continuation is ubiquitous in
many different areas of computer science,
including logic, constructive mathematics,
programming languages, and programming. This
workshop aims at providing a forum for
discussion of new results and work in progress;
work aimed at a better understanding of the
nature of continuations; applications of
continuations, and the relation of
continuations to other areas of logic and
computer science.\bibpar
CW~'97 is taking place on January 14th, 1997,
the day preceding POPL~'97. It consists of two
invited talks by Peter Landin and by John
Reynolds, and seven contributed papers. The
present BRICS technical report (distributed at
the workshop) serves as an informal
proceedings. Seven papers were selected among
eighteen submissions",
linkhtmlabs = ""
}
@techreport{BRICS-NS-96-12,
author = "Srivas, Mandayam K.",
title = "A Combined Approach to Hardware Verification:
Proof-Checking, Rewriting with Decision
Procedures and Model-Checking; Part {II}:
Articles. {BRICS} Autumn School on
Verification",
institution = brics,
year = 1996,
type = ns,
number = "NS-96-12",
address = daimi,
month = oct,
note = "56~pp",
abstract = "The notes consists of the following articles:
\begin{itemize}
\item[(1)] Modular Verification of SRT
Division, by H. Ruess, N. Shankar, and M.K.
Srivas. Presented at CAV~'96, Springer Verlag
LNCS 1102, pp. 123--134, July 1996, New
Brunswick, NJ.
\item[(2)] An Integration of Model-Checking
with Automated Proof Checking, by S. Rajan,
N. Shankar, and M.K. Srivas. Presented at the
Conference on Computer-Aided Verification,
CAV~'95, Liege, Belgium, July 1995. Springer
Verlag Lecture Notes in Computer Science vol.
939, pp. 84--97.
\item[(3)] Effective Theorem Proving for
Hardware Verification, by David Cyrluk, S.
Rajan, N. Shankar, and M. K. Srivas,
presented at the 2nd International Conference
on Theorem Provers in Circuit Design,
September 1994.
\end{itemize}
"
}
@techreport{BRICS-NS-96-11,
author = "Srivas, Mandayam K.",
title = "A Combined Approach to Hardware Verification:
Proof-Checking, Rewriting with Decision
Procedures and Model-Checking; Part {I}:
Slides. {BRICS} Autumn School on Verification",
institution = brics,
year = 1996,
type = ns,
number = "NS-96-11",
address = daimi,
month = oct,
note = "29~pp",
abstract = "Slides to lectures on {\em A Combined Approach
to Hardware Verification: Proof-Checking,
Rewriting with Decision Procedures and
Model-Checking}. See BRICS Notes NS-96-12"
}
@techreport{BRICS-NS-96-10,
author = "Pollack, Robert",
title = "What we Learn from Formal Checking; Part
{III}: Formalization is Not Just Filling In
Details. {BRICS} Autumn School on
Verification",
institution = brics,
year = 1996,
type = ns,
number = "NS-96-10",
address = daimi,
month = oct,
note = "iv+42~pp",
abstract = "I outline a small example in LEGO, a formal
development of basic lambda calculus. Some
``obvious'' theorems appear to be very
difficult to prove, in that their conventional
informal proofs are not easily formalizable. I
show a method using generalized induction that
makes these ``obvious'' theorems
straightfoward. The moral is that a user of
formal checking must be willing to solve new
problems, that formalization can teach us new
things about ``well understood'' areas, and
that using alternative definitions of basic
concepts is one way to learn these new things"
}
@techreport{BRICS-NS-96-9,
author = "Pollack, Robert",
title = "What we Learn from Formal Checking; Part {II:}
Using Type Theory: An Introduction. {BRICS}
Autumn School on Verification",
institution = brics,
year = 1996,
type = ns,
number = "NS-96-9",
address = daimi,
month = oct,
note = "iv+71~pp",
abstract = "An introduction to the Curry-Howard
isomorphism and the use of type theory for
representing mathematics and modelling computer
systems. I will concentrate on the Extended
Calculus of Constructions (ECC) of Luo, and on
the tool LEGO for checking proofs in ECC. The
main technical topic is the use of inductive
definitions to represent data types (booleans,
natural numbers, lists, syntax of a programming
language, \ldots) and relations (typing and
operational semantics of a programming
language, \ldots).\bibpar
{\bf Acknowledgement} This section was written
by Rod Bur stall and Judith Underwood"
}
@techreport{BRICS-NS-96-8,
author = "Pollack, Robert",
title = "What we Learn from Formal Checking; Part {I}:
How to Believe a Machine-Checked Proof. {BRICS}
Autumn School on Verification",
institution = brics,
year = 1996,
type = ns,
number = "NS-96-8",
address = daimi,
month = oct,
note = "iv+19~pp",
abstract = "There has been considerable discussion about
the value of a large machine-checked proof. I
suggest a view, and a technical approach, in
which belief in machine verifications is based
on evidence, which may be built up over time,
and requires participation of the readers. I
split the question of belief into two parts;
asking whether the claimed proof is actually a
derivation in the claimed formal system, and
then whether what it proves is the claimed
theorem. The first question is addressed by
independent checking of formal proofs. I
discuss how this approach extends the informal
notion of proof as surveyable by human readers,
and how surveyability of proofs reappears as
the issue of feasibility of proof-checking. The
second question has no technical answer"
}
@techreport{BRICS-NS-96-7,
author = "Melham, Tom F.",
title = "Some Research Issues in Higher Order Logic
Theorem Proving. {BRICS} Autumn School on
Verification",
institution = brics,
year = 1996,
type = ns,
number = "NS-96-7",
address = daimi,
month = oct,
note = "15~pp",
abstract = "The past twenty years have seen many advances
in the use of computers to do logical proofs
and in the deployment of this technology in
what, broadly speaking, might be called formal
methods applications. One important strand has
been research in interactive proof-construction
in higher-order logics, where the user guides
proof discovery and construction but may also
employ automatic decision procedures or
heuristics. Several well-developed
theorem-proving systems (e.g.\ HOL, Isabelle,
Coq, Nuprl) serve as vehicles for this
research; and the results of past work have
begun to reach industry through, for example,
the notable recent achievements in hardware
verification using PVS and the use of HOL at
several industrial sites.\bibpar
These lectures focus on three important areas
for future research in interactive higher order
logic theorem proving:
\begin{itemize}
\item Usability and interface design.
\item Embedding formalisms and embedded theorem
proving.
\item Integrating and implementing automated
proof methods.
\end{itemize}
Concentrating primarily on research issues, I
shall discuss some past and current work in
these areas and sketch what I see as some
important directions for the future. In keeping
with the aims of the BRICS Autumn School on
Verification, I have in mind an audience of
beginning Ph.D.\ students or newly-appointed
RAs---i.e.\ researchers who may be familiar
with some aspects of theorem proving, but who
want to expand their knowledge a little.
Experienced researchers, deeply versed in
higher order logic theorem proving, are likely
to find some of what I say already familiar to
them"
}
@techreport{BRICS-NS-96-6,
author = "Holzmann, Gerard J.",
title = "On-the-Fly Model Checking Tutorial. {BRICS}
Autumn School on Verification",
institution = brics,
year = 1996,
type = ns,
number = "NS-96-6",
address = daimi,
month = oct,
note = "31~pp",
abstract = "SPIN is a generic verification system for
models of distributed software systems. It has
been used to detect design errors in
applications ranging from abstract distributed
algorithms, to detailed code for controlling
telephone exchanges. This paper gives an
overview of the design and structure of the
verifier, reviews its automata-theoretical
foundation, and gives examples of some typical
applications of the model checker in practice."
}
@techreport{BRICS-NS-96-5,
author = "Henzinger, Thomas A.",
title = "Automatic Verification of Real-Time and Hybrid
Systems. {BRICS} Autumn School on
Verification",
institution = brics,
year = 1996,
type = ns,
number = "NS-96-5",
address = daimi,
month = oct,
note = "28~pp",
abstract = "We summarize several recent resul ts about
hybrid automata. Our goal is to demonstrate
that concepts from the theory of discrete
concurrent systems can give insights into
partly continuous systems, and that methods for
the verification of finite-state systems can be
used to analyze certain systems with
uncountable state spaces"
}
@techreport{BRICS-NS-96-4,
author = "Clarke, Jr., Edmund M.",
title = "Symbolic Model Checking. {BRICS} Autumn School
on Verification",
institution = brics,
year = 1996,
type = ns,
number = "NS-96-4",
address = daimi,
month = oct,
note = "55~pp",
abstract = "Logical errors in finite state reactive
systems are an important problem for designers.
They can delay getting a new product on the
market or cause the failure of some critical
device that is already in use. My research
group has developed a verification method
called {\em temporal logic model checking} for
this class of systems. In this approach
specifications are expressed in a propositional
temporal logic, and reactive systems are
modeled as state--transition graphs. An
efficient search procedure is used to determine
automatically if the specifications are
satisfied by the state--transition graph. The
technique has been used in the past to find
subtle errors in a number of non-trivial
circuit and protocol designs.\bibpar
During the last few years, the size of the
reactive systems that can be verified by model
checking techniques has increased dramatically.
By representing sets of states and transition
relations implicitly using Binary Decision
Diagrams (BDDs), we are now able to check
examples that are many orders of magnitude
larger than was previously the case. In this
tutorial we describe how the BDD-based model
checking techniques work and illustrate their
power by discussing the verification of several
complex protocol and circuit designs"
}
@techreport{BRICS-NS-96-3,
author = "Basin, David A.",
title = "Verification Based on Monadic Logic. {BRICS}
Autumn School on Verification",
institution = brics,
year = 1996,
type = ns,
number = "NS-96-3",
address = daimi,
month = oct,
note = "43~pp",
abstract = "We present a new approach to hardware
verification based on describing circuits in
Monadic Second-order Logic MSL. We show how to
use this logic to represent generic designs
like $n$-bit adders, which are parameterized in
space, and sequential circuits, where time is
an unbounded parameter. MSL admits a decision
procedure, implemented in the MONA tool, which
reduces formulas to canonical automata.\bibpar
The decision problem for MSL is non-elementary
decidable and thus unlikely to be usable in
practice. However, we have used MONA to
automatically verify, or find errors in, a
number of circuits studied in the literature.
Previously published machine proofs of the same
circuits are based on deduction and may involve
substantial interaction with the user.
Moreover, our approach is orders of magnitude
faster for the examples considered. We show why
the underlying computations are feasible and
how our use of MONA generalizes standard
BDD-based hardware reasoning"
}
@proceedings{BRICS-NS-96-2,
title = "Programme and Abstracts of the BRICS Autumn
School on Verification {\em(Aarhus, Denmark,
October 28 -- November 1, 1996)}",
year = 1996,
editor = "Cheng, Allan and Larsen, Kim G. and Nielsen,
Mogens",
number = "NS-96-2",
series = ns,
address = daimi,
month = aug,
organization = brics,
note = "ii+18pp",
abstract = "This note is intended to provide helpful
information, including Scientific Programme
with Abstracts, concerning attendance to the
{\em BRICS Autumn School on Verification,
Aarhus, Denmark, October 28 -- November 1,
1996}",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-NS-96-1,
author = "Berthiaume, Andr{\'e}",
title = "Quantum Computation. {M}ini-Course",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-1",
address = daimi,
month = jan,
note = "iv+126 pp",
abstract = "Computer science has a classical soul; many
definitions implicitly contain ideas from the
time we believed the world evolved according to
newtonian physics. Ideas such as: an object's
state is well defined, instantaneous actions at
a distance are impossible, etc. Modern physics
and more specifically quantum physics tells us
that Nature is not as straightforward as Newton
originally believed. One can prepare systems
such that the state is completely undefined in
any classical sense. Instantaneous actions at a
distance have been observed and sometimes
having less alternatives to produce a given
outcome may {\em improve\/} the probability of
getting this outcome! What would happen
computing models are allowed to operate within
the rules of quantum physics? What are the
advantages offered by a {\em quantum
computer\/}?\bibpar
This mini-course introduces the quantum
computer and presents some of the milestone
results in quantum complexity theory leading up
to Shor's famous polynomial time quantum
factoring algorithm. Foreknowledge of quantum
physics is useful but not necessary as the
relevant notions are introduced when needed. A
fascinating aspect of quantum computation is
the possibility of building such devices. Some
of the problems still to be overcome will
briefly addressed, but it is worth mentioning
that some ongoing experiments have shown some
very positive results. Quantum computers may
well be available sooner than we think. ",
linkhtmlabs = "",
linkps = ""
}