Journal: Formal Asp. Comput.

Volume 24, Issue 4-6

417 -- 422Peter Höfner. Preface
423 -- 431Tony Hoare, Stephan van Staden. In praise of algebra
433 -- 458José Nuno Oliveira. Towards a linear algebra of programming
459 -- 476Peter Höfner, Bernhard Möller. Dijkstra, Floyd and Warshall meet Kleene
477 -- 496Mani Swaminathan, Joost-Pieter Katoen, Ernst-Rüdiger Olderog. Layered reasoning for randomized distributed algorithms
497 -- 518Jasen Markovski, Pedro R. D'Argenio, Jos C. M. Baeten, Erik P. de Vink. Reconciling real and stochastic time: the need for probabilistic refinement
519 -- 535K. Rustan M. Leino, Kuat Yessenov. Stepwise refinement of heap-manipulating code in Chalice
537 -- 554Bengt Jonsson. Using refinement calculus techniques to prove linearizability
555 -- 567Michael Butler. External and internal choice with event groups in Event-B
569 -- 594Alberto Pettorossi, Maurizio Proietti, Valerio Senni. Constraint-based correctness proofs for logic program transformations
595 -- 607Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, James Worrell. On termination and invariance for faulty channel machines
609 -- 621Richard S. Bird. On building cyclic and shared structures in Haskell
623 -- 645Kento Emoto, Sebastian Fischer, Zhenjiang Hu. Filter-embedding semiring fusion for programming with MapReduce
647 -- 660Glynn Winskel. Deterministic concurrent strategies
661 -- 670Marta Z. Kwiatkowska, Gethin Norman, David Parker. Probabilistic verification of Herman's self-stabilisation algorithm
671 -- 678Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, James Worrell. Three tokens in Herman's algorithm
679 -- 699Robert M. Hierons, Manuel Núñez. Using schedulers to test probabilistic distributed systems
701 -- 726Yuxing Deng, Alwen Tiu. Characterisations of testing preorders for a finite probabilistic π-calculus
727 -- 748Sonja Georgievska, Suzana Andova. Probabilistic may/must testing: retaining probabilities by restricted schedulers
749 -- 768Matthew Hennessy. Exploring probabilistic bisimulations, part I
769 -- 792Ron van der Meyden. Architectural refinement and notions of intransitive noninterference
793 -- 805Jayadev Misra. A secure voting scheme based on rational self-interest

Volume 24, Issue 3

303 -- 0Jim Woodcock. Editorial
305 -- 306Cliff B. Jones. John McCarthy (1927-2011)
307 -- 330Michele Risi, Giuseppe Scanniello, Genoveffa Tortora. Using fold-in and fold-out in the architecture recovery of software systems
331 -- 353Wilkerson de L. Andrade, Patrícia D. L. Machado. Testing interruptions in reactive systems
355 -- 374Moonzoo Kim, Yunho Kim, Yunja Choi. Concolic testing of the multi-sector read operation for flash storage platform software
375 -- 391Jan Tobias Mühlberg, Gerald Lüttgen. Verifying compiled file system code
393 -- 416John Derrick, Graeme Smith. Temporal-logic property preservation under Z refinement

Volume 24, Issue 2

161 -- 162Joé Luiz Fiadeiro. Editorial
163 -- 186Antonio Filieri, Carlo Ghezzi, Giordano Tamburrelli. A formal approach to adaptive software: continuous assurance of non-functional requirements
187 -- 216Natallia Kokash, Christian Krause, Erik P. de Vink. Reo + mCRL2: A framework for model-checking dataflow in service compositions
217 -- 248José Bernardo Barros, Daniela Carneiro da Cruz, Pedro Rangel Henriques, Jorge Sousa Pinto. Assertion-based slicing and slice graphs
249 -- 266Peter A. Lindsay, Nisansala Yatapanage, Kirsten Winter. Cut Set Analysis using Behavior Trees and model checking
267 -- 302Mieke Massink, Diego Latella, Andrea Bracciali, Michael D. Harrison, Jane Hillston. Scalable context-dependent analysis of emergency egress models

Volume 24, Issue 1

1 -- 0Eerke A. Boiten, John Derrick, Jin Song Dong, Steve Reeves. Editorial
3 -- 26Carroll Morgan. Compositional noninterference from first principles
27 -- 44Wim H. Hesselink, Muhammad Ikram Lali. Formalizing a hierarchical file system
45 -- 65Jeff W. Sanders, Graeme Smith. Emergence and refinement
67 -- 95Viorel Preoteasa, Ralph-Johan Back. Invariant diagrams with data refinement
97 -- 125Stefan Hallerstede, Michael Leuschel. Experiments in program verification using Event-B
127 -- 160Frank Zeyda, Marcel Oliveira, Ana Cavalcanti. Mechanised support for sound refinement tactics