@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." }