@preamble{ "\def\bibpar{\\[.5ex]}" }
@string{TACAS = "{TACAS}"}
@string{brics = "{BRICS}"}
@string{daimi = "Department of Computer Science, University of Aarhus"}
@string{iesd = "Department of Mathematics and Computer Science, Aalborg University"}
@string{rs = "Research Series"}
@string{ns = "Notes Series"}
% Proceedings of the
%
% Workshop on Tools and Algorithms for The
% Construction and Analysis of Systems, TACAS
%
% (Aarhus, Denmark, 19--20 May, 1995)
% Uffe H. Engberg
% Kim G. Larsen
% Arne Skou (editors)
% May 1995
% Session 1
@InProceedings{TACAS-MN,
author = "Olaf M{\"u}ller and Tobias Nipkow",
title = "Combining Model Checking and Deduction for {I/O}-Automata",
pages = "1--12",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " We propose a combination of model checking and interactive
theorem proving where the theorem prover is used to represent
finite and infinite state systems, reason about them
compositionally and reduce them to small finite systems by
verified abstractions. As an example we verify a version of
the Alternating Bit Protocol with unbounded lossy and
duplicating channels: the channels are abstracted by
interactive proof and the resulting finite state system is
model checked.",
comment = "T.U. Munich, Germany"
}
@InProceedings{TACAS-LSW,
author = "Kim G. Larsen and Bernhard Steffen and Carsten Weise",
title = "A Constraint Oriented Proof Methodology Based on Modal
Transition Systems",
pages = "13--28",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " We present a constraint-oriented state-based proof
methodology for concurrent software systems which exploits
compositionality and abstraction for the reduction of the
verification problem under investigation. Formal basis for
this methodology are Modal Transition Systems allowing loose
state-based specifications, which can be refined by
successively adding constraints. Key concepts of our method
are {\em projective views}, {\em separation of proof
obligations}, {\em Skolemization} and {\em abstraction}.
Central to the method is the use of {\em Parametrized} Modal
Transition Systems. The method easily transfers to real-time
systems, where the main problem are parameters in timing
constraints.",
comment = "Aalborg, Denmark and Passau/Aachen, Germany. Email: {\tt
carsten@informatik.rwth-aachen.de}"
}
@InProceedings{TACAS-HH,
author = "Tom Henzinger and Pei-Hsin Ho",
title = "{\sc HyTech}: {T}he {C}ornell {H}ybrid {T}echnology {T}ool",
pages = "29--43",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " HyTech, the Cornell Hybrid Technology Tool, is an automatic
tool for analyzing hybrid systems. We review some of the
formal technologies that have been incorporated into HyTech,
and we illustrate the use of HyTech with two nontrivial case
studies.",
comment = "Cornell, USA"
}
% Session 2
@InProceedings{TACAS-Mad,
author = "Angelika Mader",
title = "The Modal $\mu$-calculus, Model Checking, Equation Systems
and {G}au{\ss} Elimination",
pages = "44--57",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
keywords = "modal $\mu$-calculus, model checking, Boolean equation
system, fixpoint",
abstract = " The paper presents a novel approach for solving Boolean
equation systems. It does not use approximation techniques and
backtracking. The method works similar to Gau{\ss} elimination
for linear equation systems. Homogeneous, hierarchical and
alternating fixpoints are treated uniformly. In contrast to
other techniques Gau{\ss} elimination leads to both a global
and a local model checking algorithm within one framework.",
comment = "Technical University, Munich, Germany"
}
@InProceedings{TACAS-GJJ+,
author = "Jesper G. Henriksen and Ole J. L. Jensen and Michael E.
J{\o}rgensen and Nils Klarlund and Robert Paige and Theis
Rauhe and Anders B. Sandholm",
title = "{MONA}: Monadic Second-Order Logic in Practice",
pages = "58--73",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " The purpose of this article is to introduce Monadic
Second-order Logic as a practical means of specifying
regularity. The logic is a highly succinct alternative to the
use of regular expressions. We have built a tool Mona, which
acts as a decision procedure and as a translator to
finite-state automata. The tool is based on new algorithms for
minimizing finite-state automata that use binary decision
diagrams (BDDs) to represent transition functions in
compressed form. A byproduct of this work is an algorithm that
matches the time but improves the space of Sieling and
Wegener's algorithm to reduce OBDDs in linear time.\bibpar The
potential applications are numerous. We discuss text
processing, Boolean circuits, and distributed systems. Our
main example is an automatic proof of properties for the
``Dining Philosophers with Encyclopedia'' example by Kurshan
and MacMillan. We establish these properties for the
parameterized case {\em without} the use of induction.\bibpar
Our results show that, contrary to common beliefs, high
computational complexity may be a desired feature of a
specification formalism. ",
comment = "Aarhus University, Denmark and New York University, USA"
}
@InProceedings{TACAS-MP,
author = "Oliver Matz and Andreas Potthoff",
title = "Computing Small Nondeterministic Finite Automata",
pages = "74--88",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " The minimization problem for nondeterministic finite
automata is studied. Two approaches are discussed, based on
the construction of two versions of ``canonical'' automata
(for a given regular language), in which minimal automata
occur as subautomata. A heuristic for this search is
introduced, which has been implemented in the program AMoRE.",
comment = "University of Kiel, Germany"
}
% Session 3
@InProceedings{TACAS-EL,
author = "Uffe H. Engberg and Kim S. Larsen",
title = "Efficient Simplification of Bisimulation Formulas",
pages = "89--103",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " The problem of checking or optimally simplifying
bisimulation formulas is likely to be computationally very
hard. We take a different view at the problem: we set out to
define a very fast algorithm, and then see what we can obtain.
Sometimes our algorithm can simplify a formula perfectly,
sometimes it cannot. However, the algorithm is extremely fast
and can, therefore, be added to formula-based bisimulation
model checkers at practically no cost. When the formula can be
simplified by our algorithm, this can have a dramatic positive
effect on the better, but also more time consuming, theorem
provers which will finish the job.",
comment = "Univ. of Aarhus and Odense, Denmark"
}
@InProceedings{TACAS-Lin,
author = "Huimin Lin",
title = "On Implementing Unique Fixpoint Induction for Value-passing
Processes",
pages = "104--118",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " We examine the possible pitfalls in formulating the unique
fixpoint induction proof rule in the setting of value-passing
process calculi and describe how this rule is implemented in
the verification tool {\em VPAM}. An argument is also given to
justify the implementation.",
comment = "Chinese Academy of Sciences, Beijing, China"
}
@InProceedings{TACAS-BP,
author = "Doeko J.B. Bosscher and Alban Ponse",
title = "Translating a Process Algebra with Symbolic Data Values to
Linear Format",
pages = "119--130",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " In the paper ``Translating a Valued Process Algebra with
Symnbolic Data Values to Linear Format'' the authors Bosscher
and Ponse describe a general method to translate a process
algebra with symbolic data values to a linear format. The
translation is described using the specification language
$\mu$CRL, which is a language based on the process algebra ACP
and algebraic data type theory. The translation is described
in two phases. First a translation of core fragment to linear
format. Second a larger part of the language. The motivation
for this study is oeriented to builing tools which can do
model checking for process algebras. It is believed by some
that linear formats offer better possibilities for checking
logical properties. Also linear formats conform to what is
sometimes called a data oriented view, instead of a process
oriented. Several authors translate specifications to this
format before a further analysis.",
comment = "CWI/PRG, Amsterdam, The Netherlands"
}
% Session 4
@InProceedings{TACAS-CHP,
author = "Michel Charpentier and G{\'e}rard Padiou and Abdellah El
Hadri",
title = "A {UNITY}-based Algorithm Design Assistant",
pages = "131--145",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
keywords = "Program verification, reactive programs, {\tt UNITY}
formalism, parallelism, distribution, theorem proving",
abstract = " We address the problem of the automatic verification of
reactive systems. For such algorithms, parallelism,
non-determinism and distribution, lead to frequent design
flaws and make debugging difficult. Proving programs with
respect to their specification may solve both these problems.
In this framework, we describe the implementation of an
algorithm design assistant based upon the {\tt UNITY}
formalism. A theorem prover and a Presburger formulas
calculator are used to perform the underlying proofs. We
illustrate the main difficulties encountered with
representative examples.",
comment = "ENSSEEIHT-IRIT, Toulouse, France and EMI, Rabat, Maroc"
}
@InProceedings{TACAS-Mat,
author = "Se{\'a}n Matthews",
title = "Implementing {$FS_0$} in {I}sabelle: adding structure at the
metalevel",
pages = "146--158",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " We show how a generic theorem prover like Isabelle can be
used to provide structuring facilties to a theory that lacks
them, without our having to modify the theory itself in any
way",
comment = "Max-Planck-Inst., Saarbrucken, Germany"
}
@InProceedings{TACAS-BF,
author = "J.P. Bodeveix and M. Filali",
title = "A framework for parallel program refinement",
pages = "159--173",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " This paper presents a formal framework for developing
provably correct parallel programs through refinements. We
formalize rigorously, with respect to typing, some imperative
programming constructs and propose refinements of them.
Moreover, we try to make the semantics denotation as close as
possible to the usual programming notation; the aim being to
make easy the reasoning at the semantics level. This
formalization is embedded within the HOL interactive theorem
prover and consequently reusable as a framework for general
programming by refinement. ",
comment = "IRIT, Toulouse, France"
}
@InProceedings{TACAS-Che,
author = "Boutheina Chetali",
title = "Formal Verification of Concurrent Program using the {Larch
Prover}",
pages = "174--186",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " This paper describes, by means of an example, how one may
mechanically verify concurrent programs on the theorem prover
{\sc Lp}. The chosen specification environment is {\sc Unity},
a subset of ordinary temporal logic for specifying and
verifying programs. We present the proof of a lift-control
program, we explain how we can use the theorem proving
methodology to prove safety and liveness, and to get
semi-automated proofs.",
comment = "CRIN-CNRS and INRIA-Lorraine, Nancy, France"
}
% Session 5
@InProceedings{TACAS-RGG+,
author = "Andrew W. Roscoe and Poul H.B. Gardiner and Michael H.
Goldsmith and Jason R. Hulance and David M. Jackson and J.
Bryan Scattergood",
title = "Hierarchical compression for model-checking {CSP} {\em or}
How to check $10^{20}$ dining philosophers for deadlock",
pages = "187--200",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " We discuss the integration of hierarchical, semantic-based
compression techniques for state machines into FDR, the
CSP-based refinement checker. These include normalisation,
bisimulation, factorisation by semantic equivalence and a new
technique we term diamond elimination. The resulting system,
FDR 2, is thus able to check and debug systems which,
dependent on the characteristics of the example under
consideration, may be exponentially larger than those within
the scope of the original tool.",
comment = "Oxfor University and Formal Systems Europe, Oxford, England"
}
@InProceedings{TACAS-CMS,
author = "Rance Cleaveland and Eric Madelaine and Steve Sims",
title = "A Front-End Generator for Verification Tools",
pages = "201--215",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " This paper describes the Process Algebra Compiler (PAC), a
front-end generator for process-algebra-based verification
tools. Given descriptions of a process algebra's concrete and
abstract syntax and semantics as structural operational rules,
the PAC produces syntactic routines and functions for
computing the semantics of programs in the algebra. Using this
tool greatly simplifies the task of adapting verification
tools to the analysis of systems described in different
languages; it may therefore be used to achieve source-level
compatibility between different verification tools. Although
the initial verification tools targeted by the PAC are MAUTO
and the Concurrency Workbench, the structure of the PAC caters
for the support of other tools as well.",
comment = "N.C. State University, U.S.A., INRIA, Antibes, Franc"
}
@InProceedings{TACAS-GR,
author = "Pascal Gribomont and Didier Rossetto",
title = "{CAVEAT}: technique and tool for computer aided verification
and transformation",
pages = "216--229",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " We describe {\sc caveat}, a technique and a tool (under
development) for the stepwise design and verification of
nearly finite-state concurrent systems, whose most variables
are boolean. The heart of {\sc caveat} is a tool for verifying
(inductive) invariants. The underlying method is classical\,:
formula~$I$ is an invariant for system~$\cal S$ if and only if
some formula~$\Phi_I$ is valid. {\sc caveat} uses the {\it
connection method\/} to extract from~$\Phi_I$ a (small)
set~$\Psi$ of {\it paths\/} (some kind of assertions) about
the non-boolean variables; $\Phi_I$~is valid if and only if
all paths contain {\it connections}, i.e., are inconsistent.
For typical systems given with a correct invariant, the
formula~$\Phi_I$ is rather large but $\Psi$ is quite small.
The second part of {\sc caveat} (not implemented yet) supports
an incremental development method that is fairly systematic,
but has proved to be flexible enough in practice.",
comment = "University of Li{\`e}ge, Belgium"
}
% BLL+ demo only
InProceedings{TACAS-BLL+,
author = "Johan Bengtsson and Kim G. Larsen and Fredrik Larsson and Paul
Pettersson and Wang Yi",
title = "{UPPAAL}: a Tool for Automatic Verification of Real Time
Systems",
pages = "??",
crossref = "BRICS-NS-95-2",
key = TACAS,
linkhtmlabs = "",
comment = "BRICS, Aalborg, Denmark and Uppsala University, Sweden",
linkdvi = "",
linkps = ""
}
% Session 6
@InProceedings{TACAS-DHG,
author = "Werner Damm and Hardi Hungar and Orne Grumberg",
title = "What if Model Checking Must be Truly Symbolic?",
pages = "230--244",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " There are many methodologies whose main concern it is to
reduce the complexity of a verification problem to be
ultimately able to apply model checking. Here we propose to
use a model checking like procedure which operates on a small,
truly symbolic description of the model. We do so by
exploiting systematically the separation between the (small)
control part and the (large) data part of systems which often
occurs in practice. By expanding the control part, we get an
intermediate description of the system which already allows
our symbolic model checking procedure to produce meaningful
results but which is still small enough to allow model
checking to be performed.",
comment = "Oldenburg, Germany and Haifa, Israel"
}
@InProceedings{TACAS-Tof,
author = "Chris Tofts",
title = "Analytic and locally approximate solutions to properties of
probabilistic processes",
pages = "245--259",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
comment = "Manchester University"
}
% Session 7
@InProceedings{TACAS-FFGI,
author = "Nicoletta De Francesco and Alessandro Fantechi and Stefania
Gnesi and Paola Inverardi",
title = "Model Checking of non-finite state processes by Finite
Approximation",
pages = "260--274",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " In this paper we present a verification methodology, using
an action-based logic, able to check properties for full CCS
terms, allowing also verification on infinite state systems.
Obviously, for some properties we are only able to give a
semidecision procedure. The idea is to use (a sequence of)
finite state transition systems which approximate the,
possibly infinite state, transition system corresponding to a
term. To this end we define a particular notion of
approximation, which is stronger than simulation, suitable to
define and prove liveness and safety properties of the process
terms.",
comment = "IEI-CNR, PISA, Italy"
}
@InProceedings{TACAS-BR,
author = "J{\"u}rgen Bohn and Stephan R{\"o}ssig",
title = "On Automatic and Interactive Design of Communicating
Systems",
pages = "275--289",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " The design of provable correct software requires formal
methods whose usage should be assisted by suitable tools.
Following a transformational approach the design needs
interactive user help when important design decisions have to
be made. Nevertheless simple parts should be automated as far
as possible. Ideally the user only guides the design process
by indicating the design ideas which are then carried out
automatically. Typically sequential implementations are more
appropriate for automation while parallelization needs
interaction to determine the intended program
architecture.\bibpar This paper presents a transformational
approach to the design of distributed systems where
environment and concurrently running components communicate
via synchronous message passing along directed channels.
System specifications that combine trace-based with
state-based reasoning are gradually modified by application of
transfromation rules until Occam-like programs are achieved
finally. We consider interactive and automatic aspects of such
a design process and illustrate our approach by sketching the
development of a shared register implementation.",
comment = "C.v.O University Oldenburg, Germany"
}
@InProceedings{TACAS-MK,
author = "Arnulf Mester and Heiko Krumm",
title = "Composition and Refinement Mapping based Construction of
Distributed Applications",
pages = "290--303",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " Major steps of the design of distributed applications
correspond to the integration of predefined patterns. To
support such design steps, a concept for refinement by pattern
composition is introduced which applies formal process
composition and provides functions for the tool assisted
construction and modification of specifications. The approach
is based on L. Lamport's Temporal Logic of Actions TLA and the
related theory of refinement mappings and system
composition.",
comment = "Universit{\"a}t Dortmund, Fachbereich Informatik, D-44221
Dortmund, Germany; Phone +49 231 755-4662, Fax -4730,
(mester,krumm)@ls4.informatik.uni-dortmund.de"
}
% Session 8
@InProceedings{TACAS-Jan,
author = "Wil Janssen",
title = "Layers as Knowledge Transitions in the Design of Distributed
Systems",
pages = "304--318",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " Knowledge based logics allow to give generic specifications
of classes of network protocols. This genericity is combined
with methods to derive sequentially structured or layered
implementations of distributed algorithms. Knowledge based
logic is used to specify layers in such algorithms as
knowledge transitions. The resulting layered implementations
are transformed to distributed algorithms by means a
transformation rule based on the principle of communication
closed layers. In this way a class of solutions to a problem
for different architectures can be derived along the
simultaneously. This design technique for distributed
algorithms is applied to a class of Two-Phase Commit
protocols.",
comment = "Univ. of Twente, The Netherlands"
}
@InProceedings{TACAS-KSV,
author = "Jens Knoop and Bernhard Steffen and J{\"u}rgen Vollmer",
title = "Parallelism for free: Efficient and optimal bitvector
analyses for parallel programs",
pages = "319--333",
crossref = "BRICS-NS-95-2",
key = "{TACAS}",
abstract = " In this paper we show how to construct optimal bitvector
analysis algorithms for parallel programs with shared memory
that are as efficient as their purely sequential counterparts,
and which can easily be implemented. Whereas the complexity
result is rather obvious, our optimality result is a
consequence of a new Kam/Ullman-style Coincidence Theorem.
Thus using our method, the standard algorithms for sequential
programs computing liveness, availability, very business,
reaching definitions, definition-use chains, or performing
partially redundant expression and assignment elimination,
partial dead code elimination or strength reduction, can
straightforward be transferred to the parallel setting at
almost no cost.",
comment = "University of Passau, Germany"
}
@Proceedings{BRICS-NS-95-2,
title = "Proceedings of the Workshop on Tools and Algorithms for The
Construction and Analysis of Systems, TACAS {\em (Aarhus,
Denmark, 19--20 May, 1995)}",
booktitle = "Proceedings of the Workshop on Tools and Algorithms for The
Construction and Analysis of Systems, TACAS {\em (Aarhus,
Denmark, 19--20 May, 1995)}",
year = 1995,
editor = "Uffe H. Engberg and Kim G. Larsen and Arne Skou",
number = "NS-95-2",
series = "Notes Series",
organization = "{BRICS}",
address = "Department of Computer Science, University of Aarhus",
month = may,
note = "vi+334pp",
abstract = " The aim of the workshop on {\em Tools and Algorithms for
the Construction and Analysis of Systems\/}, TACAS, is to
bring together researchers and practitioners interested in the
development and application of tools and algorithms for
specification, verification, analysis and construction of
distributed systems. The overall goal of the workshop is to
compare the various methods and the degree to which they are
supported by interacting or fully automatic tools.\bibpar The
23 papers of the proceedings cover the following topics:
refinement-based verification and construction techniques;
compositional verification methodologies; analysis and
verification via theorem-proving; decision procedures for
verification and analysis; specification formalisms, including
process algebras and temporal and modal logics; analysis
techniques for real-time and/or probabilistic systems;
approaches for value-passing systems, tool sets for
verification and analysis case studies. There were special
sessions for demonstration of verification tools."
}