External Links

    Journal: Formal Asp. Comput.

    Volume 20, Issue 6

    561 -- 0Cliff B. Jones. Valediction
    563 -- 595Sébastien Labbé, Jean-Pierre Gallois. Slicing communicating automata specifications: polynomial algorithms for model reduction
    597 -- 617Robert M. Hierons, Florentin Ipate. Testing a deterministic implementation against a non-controllable non-deterministic stream X-machine
    619 -- 635Olga Grinchtein, Martin Leucker. Network invariants for real-time systems
    637 -- 662Jewgenij Botaschanjan, Manfred Broy, Alexander Gruler, Alexander Harhurin, Steffen Knapp, Leonid Kof, Wolfgang J. Paul, Maria Spichkova. On the correctness of upper layers of automotive systems

    Volume 20, Issue 4-5

    349 -- 350Kamel Barkaoui, Manfred Broy, Ana Cavalcanti, Antonio Cerone. Guest Editorial
    351 -- 377Roberto Barbuti, Andrea Maggiolo-Schettini, Paolo Milazzo, Angelo Troina. Bisimulations in calculi modelling membranes
    379 -- 405Aaron R. Bradley, Zohar Manna. Property-directed incremental invariant generation
    407 -- 428Giorgio Delzanno, Roberto Montagna. Reachability analysis of fragments of mobile ambients in AC term rewriting
    429 -- 450Raymond R. Devillers, Hanna Klaudel, Maciej Koutny. A compositional Petri net translation of general ::::pi:::: -calculus terms
    451 -- 479Murdoch James Gabbay, Aad Mathijssen. Capture-avoiding substitution as a nominal algebra
    481 -- 505Roland Meyer, Johannes Faber, Jochen Hoenicke, Andrey Rybalchenko. Model checking Duration Calculus: a practical approach
    507 -- 560Matteo Slanina, Henny B. Sipma, Zohar Manna. Deductive verification of alternating systems

    Volume 20, Issue 3

    239 -- 240Dines Bjørner. John Warner Backus: 3 Dec 1924-17 March 2007
    241 -- 258Julien Schmaltz, Dominique Borrione. A functional formalization of on chip communications
    259 -- 275Florian Kammüller. Formalizing non-interference for a simple bytecode language in Coq
    277 -- 294Gavin Lowe. Specification of communicating processes: temporal logic versus refusals-based refinement
    295 -- 301Steve Reeves, David Streader. Data refinement and singleton failures refinement are not equivalent
    303 -- 348Ivan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano. Efficient representation of the attacker s knowledge in cryptographic protocols analysis

    Volume 20, Issue 2

    141 -- 160Brijesh Dongol, Arjan J. Mooij. Streamlining progress-based derivations of concurrent programs
    161 -- 204Michael Möller, Ernst-Rüdiger Olderog, Holger Rasch, Heike Wehrheim. Integrating a formal method into a software engineering process with UML and Java
    205 -- 224Purandar Bhaduri, S. Ramesh. Interface synthesis and protocol conversion
    225 -- 238Hanifa Boucheneb. Interval timed coloured Petri net: efficient construction of its state class space preserving linear properties

    Volume 20, Issue 1

    1 -- 3Cliff B. Jones, Jim Woodcock. Editorial
    5 -- 19Jim Woodcock, Susan Stepney, David Cooper, John A. Clark, Jeremy Jacob. The certification of the Mondex electronic purse to ITSEC Level E6
    21 -- 39Tahina Ramananandro. ::::Mondex:::: , an electronic purse: specification and refinement checks with the ::::Alloy:::: model-finding method
    41 -- 59Dominik Haneberg, Gerhard Schellhorn, Holger Grandy, Wolfgang Reif. Verification of Mondex electronic purses with KIV: from transactions to a security protocol
    61 -- 77Michael Butler, Divakar Yadav. An incremental development of the Mondex system in Event-B
    79 -- 100Mirco Kuhlmann, Martin Gogolla. Modeling and validating Mondex scenarios described in UML and OCL with USE
    101 -- 116Chris George, Anne Elisabeth Haxthausen. Specification, proof, and model checking of the Mondex electronic purse using RAISE
    117 -- 139Leo Freitas, Jim Woodcock. Mechanising Mondex with Z/Eves
    runs on