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