Olaf Müller and Tobias Nipkow.
Combining model checking and deduction for I/O-automata.
In TACAS, pages 1--12.
vi+334pp.
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.
Comments: T.U. Munich, Germany.
Kim G. Larsen, Bernhard Steffen, and Carsten Weise.
A constraint oriented proof methodology based on modal transition systems.
In TACAS, pages 13--28.
vi+334pp.
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 projective views, separation of proof obligations, Skolemization and abstraction. Central to the method is the use of Parametrized Modal Transition Systems. The method easily transfers to real-time systems, where the main problem are parameters in timing constraints.
Comments: Aalborg, Denmark and Passau/Aachen, Germany. Email: carsten@informatik.rwth-aachen.de.
Tom Henzinger and Pei-Hsin Ho.
HYTECH: The Cornell Hybrid Technology Tool.
In TACAS, pages 29--43.
vi+334pp.
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.
Comments: Cornell, USA.
Angelika Mader.
The modal
-calculus, model checking, equation systems and
Gauß elimination.
In TACAS, pages 44--57.
vi+334pp.
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ß elimination for linear equation systems. Homogeneous, hierarchical and alternating fixpoints are treated uniformly. In contrast to other techniques Gauß elimination leads to both a global and a local model checking algorithm within one framework.
Comments: Technical University, Munich, Germany.
Jesper G. Henriksen, Ole J. L. Jensen, Michael E. Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders B. Sandholm.
MONA: Monadic second-order logic in practice.
In TACAS, pages 58--73.
vi+334pp.
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.
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 without the use of induction.
Our results show that, contrary to common beliefs, high computational complexity may be a desired feature of a specification formalism.
Comments: Aarhus University, Denmark and New York University, USA.
Oliver Matz and Andreas Potthoff.
Computing small nondeterministic finite automata.
In TACAS, pages 74--88.
vi+334pp.
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.
Comments: University of Kiel, Germany.
Uffe H. Engberg and Kim S. Larsen.
Efficient simplification of bisimulation formulas.
In TACAS, pages 89--103.
vi+334pp.
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.
Comments: Univ. of Aarhus and Odense, Denmark.
Huimin Lin.
On implementing unique fixpoint induction for value-passing processes.
In TACAS, pages 104--118.
vi+334pp.
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 VPAM. An argument is also given to justify the implementation.
Comments: Chinese Academy of Sciences, Beijing, China.
Doeko J.B. Bosscher and Alban Ponse.
Translating a process algebra with symbolic data values to linear format.
In TACAS, pages 119--130.
vi+334pp.
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
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.
Comments: CWI/PRG, Amsterdam, The Netherlands.
Michel Charpentier, Gérard Padiou, and Abdellah El Hadri.
A UNITY-based algorithm design assistant.
In TACAS, pages 131--145.
vi+334pp.
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 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.
Comments: ENSSEEIHT-IRIT, Toulouse, France and EMI, Rabat, Maroc.
Seán Matthews.
Implementing
in Isabelle: adding structure at the
metalevel.
In TACAS, pages 146--158.
vi+334pp.
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.
Comments: Max-Planck-Inst., Saarbrucken, Germany.
J.P. Bodeveix and M. Filali.
A framework for parallel program refinement.
In TACAS, pages 159--173.
vi+334pp.
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.
Comments: IRIT, Toulouse, France.
Boutheina Chetali.
Formal verification of concurrent program using the Larch Prover.
In TACAS, pages 174--186.
vi+334pp.
Abstract: This paper describes, by means of an example, how one may mechanically verify concurrent programs on the theorem prover LP. The chosen specification environment is 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.
Comments: CRIN-CNRS and INRIA-Lorraine, Nancy, France.
Andrew W. Roscoe, Poul H.B. Gardiner, Michael H. Goldsmith, Jason R. Hulance, David M. Jackson, and J. Bryan Scattergood.
Hierarchical compression for model-checking CSP or how to check
dining philosophers for deadlock.
In TACAS, pages 187--200.
vi+334pp.
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.
Comments: Oxfor University and Formal Systems Europe, Oxford, England.
Rance Cleaveland, Eric Madelaine, and Steve Sims.
A front-end generator for verification tools.
In TACAS, pages 201--215.
vi+334pp.
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.
Comments: N.C. State University, U.S.A., INRIA, Antibes, Franc.
Pascal Gribomont and Didier Rossetto.
CAVEAT: technique and tool for computer aided verification and transformation.
In TACAS, pages 216--229.
vi+334pp.
Abstract: We describe 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 CAVEAT is a tool for verifying (inductive) invariants. The underlying method is classical: formula I is an invariant for system
if and only if some formula 
is valid. CAVEAT
uses the connection method to extract from 
a (small)
set 
of paths (some kind of assertions) about the non-boolean
variables; 
is valid if and only if all paths contain
connections, i.e., are inconsistent. For typical systems given with a
correct invariant, the formula 
is rather large but 
is quite
small. The second part of CAVEAT (not implemented yet) supports an
incremental development method that is fairly systematic, but has proved to
be flexible enough in practice.
Comments: University of Liège, Belgium.
Werner Damm, Hardi Hungar, and Orne Grumberg.
What if model checking must be truly symbolic?
In TACAS, pages 230--244.
vi+334pp.
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.
Comments: Oldenburg, Germany and Haifa, Israel.
Chris Tofts.
Analytic and locally approximate solutions to properties of probabilistic processes.
In TACAS, pages 245--259.
vi+334pp.
Abstract: The aim of the workshop on 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.
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.
Comments: Manchester University.
Nicoletta De Francesco, Alessandro Fantechi, Stefania Gnesi, and Paola Inverardi.
Model checking of non-finite state processes by finite approximation.
In TACAS, pages 260--274.
vi+334pp.
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.
Comments: IEI-CNR, PISA, Italy.
Jürgen Bohn and Stephan Rössig.
On automatic and interactive design of communicating systems.
In TACAS, pages 275--289.
vi+334pp.
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.
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.
Comments: C.v.O University Oldenburg, Germany.
Arnulf Mester and Heiko Krumm.
Composition and refinement mapping based construction of distributed applications.
In TACAS, pages 290--303.
vi+334pp.
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.
Comments: Universität Dortmund, Fachbereich Informatik, D-44221 Dortmund, Germany; Phone +49 231 755-4662, Fax -4730, (mester,krumm)@ls4.informatik.uni-dortmund.de.
Wil Janssen.
Layers as knowledge transitions in the design of distributed systems.
In TACAS, pages 304--318.
vi+334pp.
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.
Comments: Univ. of Twente, The Netherlands.
Jens Knoop, Bernhard Steffen, and Jürgen Vollmer.
Parallelism for free: Efficient and optimal bitvector analyses for parallel programs.
In TACAS, pages 319--333.
vi+334pp.
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.
Comments: University of Passau, Germany.
Proceedings of the Workshop on Tools and Algorithms for The Construction and Analysis of Systems, TACAS (Aarhus, Denmark, 19--20 May, 1995), May 1995.
vi+334pp.
Abstract: The aim of the workshop on 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.
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.
![[BRICS symbol]](http://www.brics.aau.dk/BRICS/GIF/BRICS/msymbol8mm.GIF)
BRICS WWW home page