Last update:
Mon Jun 12 07:31:59 MDT 2023
C. B. Jones Editorial . . . . . . . . . . . . . . . 1--3
Martyn Thomas Development methods for trusted computer
systems . . . . . . . . . . . . . . . . 5--18
Roland Backhouse and
Paul Chisholm and
Grant Malcolm and
Erik Saaman Do-it-yourself type theory . . . . . . . 19--84
Mogens Nielsen and
Klaus Havelund and
Kim Ritter Wagner and
Chris George The RAISE language, method and tools . . 85--114
C. A. Middelburg VVSL: A language for structured VDM
specifications . . . . . . . . . . . . . 115--135
Brian Monahan Book reviews . . . . . . . . . . . . . . 137--144
D. J. Cooke Editorial . . . . . . . . . . . . . . . 145--146
C. T. Burton and
S. J. Cook and
S. Gikas and
J. R. Rowson and
S. T. Sommerville Specifying the Apple Macintosh\TM
Toolbox event manager . . . . . . . . . 147--171
Martin C. Henson Program development in the constructive
set theory TK . . . . . . . . . . . . . 173--192
Matthew Huntbach Meta-interpreters and partial evaluation
in Parlog . . . . . . . . . . . . . . . 193--211
Marta Z. Kwiatkowska Event fairness and non-interleaving
concurrency . . . . . . . . . . . . . . 213--228
He Jifeng Process simulation and refinement . . . 229--241
Sören Holmström A refinement calculus for specifications
in Hennessy--Milner logic with recursion 242--272
D. J. Walker Automated analysis of mutual exclusion
algorithms using CCS . . . . . . . . . . 273--292
John Cooke and
Crustian Calude and
Will Harwood and
Dan Simpson Book reviews . . . . . . . . . . . . . . 293--301
Peter Dybjer and
Herbert P. Sander A functional programming approach to the
specification and verification of
concurrent systems . . . . . . . . . . . 303--319
Tobias Nipkow Term rewriting and beyond --- theorem
proving in Isabelle . . . . . . . . . . 320--338
Simon Thompson A logic for Miranda . . . . . . . . . . 339--365
Pierre America Issues in the design of a parallel
object-oriented language . . . . . . . . 366--411
Tom Parke and
R. McLean Book reviews . . . . . . . . . . . . . . 412--415
J. N. Oliveira A reification calculus for
model-oriented software specification 1--23
José Carmo and
Amílcar Sernadas Branching versus linear logics yet again 24--59
Wim H. Hesselink Command algebras, recursion and program
transformation . . . . . . . . . . . . . 60--104
Anonymous Forthcoming events 1990 . . . . . . . . 105--108
H. A. Partsch and
F. A. Stomp A fast pattern matching algorithm
derived by transformational and
assertional reasoning . . . . . . . . . 109--122
Eike Best and
Jörg Desel Partial order behaviour and structure of
Petri nets . . . . . . . . . . . . . . . 123--138
Wim H. Hesselink Axioms and models of linear logic . . . 139--166
Jayadev Misra Equational reasoning about
nondeterministic processes . . . . . . . 167--195
Tim Denvir and
Rosamund Rawlings and
Tom Parke and
S. J. Goldsack and
Anthony Hall Book reviews . . . . . . . . . . . . . . 196--202
Anonymous Forthcoming events 1990 . . . . . . . . 203--205
Miki Hermann Chain properties of rule closures . . . 207--225
Xudong He and
John A. N. Lee Integrating predicate transition nets
with first order temporal logic in the
specification and verification of
concurrent systems . . . . . . . . . . . 226--246
R. J. R. Back and
J. von Wright Refinement concepts formalised in higher
order logic . . . . . . . . . . . . . . 247--272
C. Lengauer and
J. W. Sanders The projection of systolic programs . . 273--293
Anonymous Forthcoming events 1990 . . . . . . . . 294--298
M. S. Paterson Obituary: Professor David Michael
Ritchie Park . . . . . . . . . . . . . . 299--300
Huimin Lin and
Man-Chi Pong Modelling multiple inheritance with
colimits . . . . . . . . . . . . . . . . 301--311
Alain Ah-kee Proof obligations for blocks and
procedures . . . . . . . . . . . . . . . 312--330
Mike Stannett X-machines and the halting problem:
Building a super-Turing machine . . . . 331--341
Nandit Soparkar and
Abraham Silberschatz On the interconnection constants of
Hopfield nets . . . . . . . . . . . . . 342--358
N. P. Chapman Defining, analysing and implementing
communication protocols using attribute
grammars . . . . . . . . . . . . . . . . 359--392
Anonymous Forthcoming events 1990 . . . . . . . . 393--396
David Gries Editorial . . . . . . . . . . . . . . . 1--1
Olaf Owe and
Ole-Johan Dahl Generator induction in order sorted
algebras . . . . . . . . . . . . . . . . 2--20
Manfred Broy Towards a formal foundation of the
specification and description language
SDL . . . . . . . . . . . . . . . . . . 21--57
Susan Stepney and
Dave Whitley and
David Cooper and
Colin Grant A demonstrably correct compiler . . . . 58--101
David Pitt and
Dan Simpson Book reviews . . . . . . . . . . . . . . 102--105
Anonymous Forthcoming events . . . . . . . . . . . 106--108
C. B. Jones Editorial . . . . . . . . . . . . . . . 109--109
Geoff Barrett The fixed point theory of unbounded
non-determinism . . . . . . . . . . . . 110--128
Elspeth Cusack Refinement, conformance and inheritance 129--141
J. C. M. Baeten and
J. A. Bergstra Real time process algebra . . . . . . . 142--188
Beverly A. Sanders Eliminating the substitution axiom from
UNITY logic . . . . . . . . . . . . . . 189--205
David Murphy and
J. W. Sanders Book reviews . . . . . . . . . . . . . . 206--212
Anonymous Forthcoming events . . . . . . . . . . . 213--216
Tim Denvir Editorial . . . . . . . . . . . . . . . 217--217
Michael Hedberg Normalising the associative law: An
experiment with Martin-Löf's type theory 218--252
Vangalur S. Alagar and
Geetha Ramanathan Functional specification and proof of
correctness for time dependent behaviour
of reactive systems . . . . . . . . . . 253--283
Huajun Qin and
Philip Lewis Factorisation of finite state machines
under strong and observational
equivalences . . . . . . . . . . . . . . 284--307
Anonymous Forthcoming events . . . . . . . . . . . 308--312
John Cooke Editorial . . . . . . . . . . . . . . . 313--314
Peter Baumann Towards a semantics-based information
theory . . . . . . . . . . . . . . . . . 315--325
Rolf Hennicker Context induction: A proof principle for
behavioural abstractions and algebraic
implementations . . . . . . . . . . . . 326--345
M. Hennessy A proof system for communicating
processes with value-passing . . . . . . 346--366
Christiane Notarmarco and
Rod Mulvey Formal aspects of computing: \LaTeX
style guide for authors . . . . . . . . 367--376
Anonymous Forthcoming events . . . . . . . . . . . 377--378
Tim Denvir Editorial . . . . . . . . . . . . . . . 1--12
C. A. Middelburg Modular structuring of VDM
specifications in VVSL . . . . . . . . . 13--47
Chris George The NDB database specified in the RAISE
specification language . . . . . . . . . 48--75
Ian Hayes VDM and Z: A comparative case study . . 76--99
Edmund Kazmierczak Modularising the specification of a
small database system in extended ML . . 100--142
Fritz Henglein Book review . . . . . . . . . . . . . . 143--144
Anonymous Forthcoming events . . . . . . . . . . . 145--147
Parosh Abdulla Automatic verification of a class of
systolic circuits . . . . . . . . . . . 149--194
Johan J. Lukkien and
Jan L. A. van de Snepscheut Weakest preconditions for progress . . . 195--236
Anonymous Forthcoming events . . . . . . . . . . . 237--238
J. Fiadeiro and
T. Maibaum Temporal theories as modularisation
units for concurrent system
specification . . . . . . . . . . . . . 239--272
James H. Anderson and
Mohamed G. Gouda A criterion for atomicity . . . . . . . 273--298
Michael Fisher A model checker for linear time temporal
logic . . . . . . . . . . . . . . . . . 299--319
Anonymous Forthcoming events . . . . . . . . . . . 320--322
Olaf Owe Axiomatic treatment of processes with
shared variables revisited . . . . . . . 323--340
Heinz Fassbender and
Heiko Vogler An implementation of syntax directed
functional programming on nested-stack
machines . . . . . . . . . . . . . . . . 341--375
Pierre America and
Jan Rutten A layered semantics for a parallel
object-oriented language . . . . . . . . 376--408
Anonymous Forthcoming events . . . . . . . . . . . 409--411
Lambert Meertens Paramorphisms . . . . . . . . . . . . . 413--424
Jonathan P. Seldin Coquand's calculus of constructions: A
mathematical foundation for a proof
development system . . . . . . . . . . . 425--441
Zhiming Liu and
Mathai Joseph Transformation of programs for
fault-tolerance . . . . . . . . . . . . 442--469
J. Roger Hindley Types with intersection: An introduction 470--486
Andrew Kay and
Peter Lupton Sequential to parallel buffer refinement 487--492
M. D. Atkinson and
David Lester and
Lawrence C. Paulson Book reviews . . . . . . . . . . . . . . 493--496
Fredrik Orava and
Joachim Parrow An algebraic verification of a mobile
network . . . . . . . . . . . . . . . . 497--543
Noureddine Boudriga and
Fathi Elloumi and
Ali Mili On the lattice of specifications:
Applications to a specification
methodology . . . . . . . . . . . . . . 544--571
Eike Best and
Ludmila Cherkasova and
Jörg Desel Compositional generation of home states
in free choice nets . . . . . . . . . . 572--581
Nissim Francez and
Ralph-J. J. Back and
Reino Kurki-Suonio On equivalence-completions of fairness
assumptions . . . . . . . . . . . . . . 582--591
Heinrich Hussmann Book review . . . . . . . . . . . . . . 592--593
Cliff Jones and
John Cooke Editorial . . . . . . . . . . . . . . . 595--596
David M. Russinoff A verification system for concurrent
programs based on the Boyer--Moore
prover . . . . . . . . . . . . . . . . . 597--611
L. Pomello and
C. Simone An algebraic characterisation of
elementary net system (observable) state
space . . . . . . . . . . . . . . . . . 612--637
José Balcázar and
Joaquim Gabarró and
Miklós Sántha Deciding bisimilarity is $P$-complete 638--648
M. W. Shields Multitraces, hypertraces and partial
order semantics . . . . . . . . . . . . 649--672
Maarten M. Fokkinga Calculate categorically! . . . . . . . . 673--692
C. T. P. Burton Program morphisms . . . . . . . . . . . 693--726
Masaaki Mizuno and
David Schmidt A security flow control algorithm and
its denotational semantics correctness
proof . . . . . . . . . . . . . . . . . 727--754
William R. Bevier and
William D. Young Machine checked proofs of the design of
a fault-tolerant circuit . . . . . . . . 755--775
Jeroen Fokker The systematic construction of a
one-combinator basis for Lambda--Terms 776--780
Anonymous Forthcoming events . . . . . . . . . . . 781--782
Rance Cleaveland and
Matthew Hennessy Testing equivalence as a bisimulation
equivalence . . . . . . . . . . . . . . 1--20
P. J. A. Lentfert and
S. D. Swierstra Distributed maximum maintenance on
hierarchically divided graphs . . . . . 21--60
R. S. Bird and
O. de Moor List partitions . . . . . . . . . . . . 61--78
T. Massart and
R. Devillers Equality of agent expressions is
preserved under an extension of the
universe of actions . . . . . . . . . . 79--88
Anonymous Forthcoming events . . . . . . . . . . . 89--90
A. Bucci and
P. Inverardi and
S. Martini An ``executable'' impredicative
semantics for the Ada configuration . . 91--120
Debora Weber-Wulff Proof movie --- A proof with the
Boyer--Moore prover . . . . . . . . . . 121--151
Alan Williams The applicability of discrete
performance estimation methods to VLSI
design . . . . . . . . . . . . . . . . . 152--176
Anonymous Forthcoming events . . . . . . . . . . . 177--180
Andreas V. Hense Denotational semantics of an
object-oriented programming language
with explicit wrappers . . . . . . . . . 181--207
Olaf Owe Partial logics reconsidered: A
conservative approach . . . . . . . . . 208--223
Juan Quemada and
David de Frutos and
Arturo Azcorra TIC: A timed calculus . . . . . . . . . 224--252
Carlos Miguel and
Angel Fernández and
Leon Vidaller LOTOS extended with probabilistic
behaviours . . . . . . . . . . . . . . . 253--281
Dyckhoff Roy and
E. Moggi Book reviews . . . . . . . . . . . . . . 282--284
Anonymous Forthcoming events . . . . . . . . . . . 285--288
Bill Stoddart and
Peter J. Knaggs Type inference in stack based languages 289--298
Paul Mukherjee and
Victoria Stavridou The formal specification of safety
requirements for storing explosives . . 299--336
Esther Dennis-Jones and
David E. Rydeheard Categorical ML --- Category-theoretic
modular programming . . . . . . . . . . 337--366
P. H. B. Gardiner and
Carroll Morgan A single complete rule for data
refinement . . . . . . . . . . . . . . . 367--382
Tony Davie and
Simon Brock Book reviews . . . . . . . . . . . . . . 383--384
Anonymous Forthcoming events . . . . . . . . . . . 385--387
Cliff Jones and
John Cooke Editorial . . . . . . . . . . . . . . . 389--390
Matthias Weber Definition and basic properties of the
Deva meta-calculus . . . . . . . . . . . 391--431
M. Hennessy and
A. Ingólfsdóttir Communicating processes with
value-passing and assignments . . . . . 432--466
Gordon Brebner A CCS-based investigation of deadlock in
a multi-process electronic mail system 467--479
J. C. M. Baeten and
J. A. Bergstra Real space process algebra . . . . . . . 481--529
Jim Davies and
Steve Schneider Recursion induction for real-time
processes . . . . . . . . . . . . . . . 530--553
Wim H. Hesselink Proof rules for recursive procedures . . 554--570
Rafael D. Lins Book review . . . . . . . . . . . . . . 571--572
Anonymous Forthcoming events . . . . . . . . . . . 573--573
John Staples and
Peter J. Robinson and
Daniel Hazel A functional logic for higher level
reasoning about computation . . . . . . 1--38
Peter Nickolas The completeness of functional logic . . 39--59
J. Strother Moore A formal model of asynchronous
communication and its use in
mechanically verifying a biphase mark
protocol . . . . . . . . . . . . . . . . 60--91
Glenn Bruns and
Stuart Anderson The formalization and analysis of a
communications protocol . . . . . . . . 92--112
Cliff Jones Editorial . . . . . . . . . . . . . . . 113--114
Jan Friso Groote and
Alban Ponse Process algebra with guards: Combining
Hoare logic with process algebra . . . . 115--164
G. Boudol and
I. Castellani and
M. Hennessy and
A. Kiehn A theory of processes with localities 165--200
Luca Aceto A static view of localities . . . . . . 201--222
Grigoris Antoniou The verification of modules . . . . . . 223--244
James J. Horning Book reviews . . . . . . . . . . . . . . 245--246
Edsger W. Dijkstra Jan L. A. van de Snepscheut . . . . . . 247--249
J. C. M. Baeten and
J. A. Bergstra On sequential composition, action
prefixes and process prefix . . . . . . 250--268
Pierre America and
Frank de Boer Reasoning about dynamically evolving
process structures . . . . . . . . . . . 269--316
Bard Bloom When is partial trace equivalence
adequate? . . . . . . . . . . . . . . . 317--338
Chris Brink and
Katarina Britz and
Renate A. Schmidt Peirce algebras . . . . . . . . . . . . 339--358
David M. Russinoff A mechanically verified incremental
garbage collector . . . . . . . . . . . 359--390
Karl J. Lieberherr and
Walter L. Hürsch and
Cun Xiao Object-extending class transformations 391--416
J. P. Wray and
A. Stewart Correct translation of data parallel
assignment onto array processors . . . . 417--439
Peter Dybjer Inductive families . . . . . . . . . . . 440--465
I. S. W. B. Prasetya Error in the UNITY substitution rule for
subscripted operators . . . . . . . . . 466--470
David Pitt and
Paddy Byers The rest stays unchanged (concurrency
and state-based specification) . . . . . 471--494
A. Prasad Sistla Safety, liveness and fairness in
temporal logic . . . . . . . . . . . . . 495--511
Hans Hansson and
Bengt Jonsson A logic for reasoning about time and
reliability . . . . . . . . . . . . . . 512--535
Chris Tofts Processes with probabilities, priority
and time . . . . . . . . . . . . . . . . 536--564
Peter Gorm Larsen Response to ``The formal specification
of safety requirements for storing
explosives'' . . . . . . . . . . . . . . 565--568
Iain S. C. Houston and
Mark B. Josephs Specifying distributed CICS in Z:
Accessing local and remote resources . . 569--579
Leslie Lamport How to write a long formula . . . . . . 580--584
John Cooke Editorial . . . . . . . . . . . . . . . 585--585
Peter Gorm Larsen and
Nico Plat and
Hans Toetenel A Formal Semantics of Data Flow Diagrams 586--606
K. Mani Chandy Properties of Concurrent Programs . . . 607--619
Arnon Avron and
Nada Sasson Stability, Sequentiality and Demand
Driven Evaluation in Dataflow . . . . . 620--642
He Jifeng and
Jonathan Bowen Specification, Verification and
Prototyping of an Optimized Compiler . . 643--658
Yasuhiko Minamide Sharing Analysis Based on Type Inference 659--675
Paola Inverardi and
Corrado Priami and
Daniel Yankelevich Automatizing Parametric Reasoning on
Distributed Concurrent Systems . . . . . 676--695
Mike Stannett Infinite Concurrent Systems --- I. The
Relationship between Metric and Order
Convergence . . . . . . . . . . . . . . 696--715
F. A. Stomp and
W.-R de Roever A Principle for Sequential Reasoning
about Distributed Algorithms . . . . . . 716--737
F. S. de Boer and
E.-R. Olderog and
A. Ponse and
F.-J. de Vries Editorial . . . . . . . . . . . . . . . 741--742
Krzysztof R. Apt and
Elena Marchiori Reasoning about Prolog programs: From
modes through types to assertions . . . 743--765
Jan van Eijck Presupposition failure --- a comedy of
errors . . . . . . . . . . . . . . . . . 766--787
Marcello M. Bonsangue and
Joost N. Kok The weakest precondition calculus:
Recursion and duality . . . . . . . . . 788--800
Jozef Hooman Extending Hoare logic to real-time . . . 801--825
Michael R. Hansen Model-checking discrete duration
calculus . . . . . . . . . . . . . . . . 826--845
M. D. Atkinson and
Julian Bradfield Book reviews . . . . . . . . . . . . . . 846--848
H. Peter Hofstee On Jan L. A. van de Snepscheut's ``The
Sliding-Window Protocol Revisited'' . . 1--2
Jan L. A. van de Snepscheut The sliding-window protocol revisited 3--17
J. F. Costa and
A. Sernadas Progress assumption in concurrent
systems . . . . . . . . . . . . . . . . 18--36
Michael Butler and
Carroll Morgan Action systems, unbounded
nondeterminism, and infinite traces . . 37--53
Steve King and
Carroll Morgan Exits in the refinement calculus . . . . 54--76
Pierre Lescanne Termination of rewrite systems by
elementary interpretations . . . . . . . 77--90
J. Coenen Hoare's logic and VDM . . . . . . . . . 91--105
Joakim von Wright and
Peter Jeavons and
Julian Bradfield and
Muffy Thomas and
David Lester Book reviews . . . . . . . . . . . . . . 106--110
John Cooke Editorial . . . . . . . . . . . . . . . 111--112
Naoki Kobayashi and
Akinori Yonezawa Asynchronous communication model based
on linear logic . . . . . . . . . . . . 113--149
J. M. Spivey Unification: A case-study in data
refinement . . . . . . . . . . . . . . . 150--168
I. Rewitzky and
C. Brink Predicate transformers as power
operations . . . . . . . . . . . . . . . 169--182
Sunil Vadera Proof by analogy in mural . . . . . . . 183--206
Bryan S. Todd, FRCS and
Richard Stamper A formal model of explanation . . . . . 207--225
Paul Mukherjee and
John Stell and
Carron Kirkwood Book reviews . . . . . . . . . . . . . . 226--229
Nancy Lynch and
Roberto Segala A comparison of simulation techniques
and algebraic techniques for verifying
concurrent systems . . . . . . . . . . . 231--265
Jane Sinclair and
Jim Woodcock Event refinement in state-based
concurrent systems . . . . . . . . . . . 266--288
Graeme Smith A fully abstract semantics of classes
for Object-Z . . . . . . . . . . . . . . 289--313
Lone Leth and
Bent Thomsen Some facile chemistry . . . . . . . . . 314--328
Ian J. Hayes and
Brendan P. Mahony Using units of measurement in formal
specifications . . . . . . . . . . . . . 329--347
Toby Walsh and
K. J. Turner and
Jan Joris Vereijken Book reviews . . . . . . . . . . . . . . 348--351
Rutger M. Dijkstra DUALITY: A simple formalism for the
analysis of UNITY . . . . . . . . . . . 353--388
Wim H. Hesselink Safety and progress of recursive
procedures . . . . . . . . . . . . . . . 389--411
Simon Thompson A logic for Miranda, revisited . . . . . 412--429
I. J. Hayes and
J. W. Sanders Specification by interface separation 430--439
Antti Valmari and
Martti Tienari Compositional failure-based semantic
models for Basic LOTOS . . . . . . . . . 440--468
Simon Brock and
P. Gibson Book reviews . . . . . . . . . . . . . . 469--472
Peter B. Ladkin and
Stefan Leue Interpreting Message Flow Graphs . . . . 473--509
Zhiming Liu and
Mathai Joseph and
Tomasz Janowski Verification of schedulability for
real-time programs . . . . . . . . . . . 510--532
H. Barringer and
M. Fisher and
D. Gabbay and
G. Gough and
R. Owens MetateM: An introduction . . . . . . . . 533--549
Kai Engelhardt and
Willem-Paul de Roever Towards a practitioners' approach to
Abadi and Lamport's method . . . . . . . 550--575
K. Rustan M. Leino A method for showing progress . . . . . 576--580
W. P. R. Mitchell and
Alan Hamilton and
A. J. McIsaac and
Iain Stewart Book reviews . . . . . . . . . . . . . . 581--585
Philippe Noël A transformation-based synthesis of
temporal specifications . . . . . . . . 587--619
Ian Maung On simulation, subtyping and
substitutability in sequential object
systems . . . . . . . . . . . . . . . . 620--651
David A. Naumann Data refinement, call by value and
higher order programs . . . . . . . . . 652--662
Sergei Gorlatch and
Christian Lengauer Parallelization of divide-and-conquer in
the Bird--Meertens formalism . . . . . . 663--682
Rajit Manohar and
K. Rustan and
M. Leino Conditional composition . . . . . . . . 683--703
Paul Mukherjee and
Victoria Stavridou A theory of Orwellian specifications
with NewThink . . . . . . . . . . . . . 704--727
Manfred Broy and
Cliff Jones Editorial . . . . . . . . . . . . . . . 1--2
Paulo S. C. Alencar and
Carlos J. P. de Lucena A logical framework for evolving
software systems . . . . . . . . . . . . 3--46
Peter Gorm Larsen and
Bo Stig Hansen Semantics of under-determined
expressions . . . . . . . . . . . . . . 47--66
Karen Seidel and
Paul Gardiner Structured development of a virtual
shared memory system . . . . . . . . . . 67--85
Martin Simons and
Matthias Weber An approach to literate and structured
formal developments . . . . . . . . . . 86--107
David Billington and
R. Geoff Dromey The co-invariant generator: An aid in
deriving loop bodies . . . . . . . . . . 108--126
Ketil Stòlen and
Frank Dederichs and
Rainer Weber Specification and refinement of networks
of asynchronously communicating agents
using the assumption/commitment paradigm 127--161
Padmanabhan Krishnan Architectural CCS . . . . . . . . . . . 162--187
J. C. M. Baeten and
J. A. Bergstra Discrete time process algebra . . . . . 188--208
Geoffrey Brown and
Wayne Luk and
John O'Leary Retargeting a hardware compiler using
protocol converters . . . . . . . . . . 209--237
Walter Hussak On CCS with parametric relabelling . . . 238--244
Jonathan Bowen and
Dieter Gollmann Book reviews . . . . . . . . . . . . . . 245--246
Giuseppe Castagna Integration of parametric and ``ad hoc''
second order polymorphism in a calculus
with subtyping . . . . . . . . . . . . . 247--293
Ping Zhou and
Jozef Hooman and
Ruurd Kuiper Compositional verification of real-time
systems with Explicit Clock Temporal
Logic . . . . . . . . . . . . . . . . . 294--323
R. J. R. Back and
K. Sere Superposition refinement of reactive
systems . . . . . . . . . . . . . . . . 324--346
Roger Duke and
Cecily Bailes and
Graeme Smith A blocking model for reactive objects 347--368
Michael Spivey The consistency theorem for free type
definitions in Z . . . . . . . . . . . . 369--375
Brian Matthews and
Andrew Blyth and
J. S. Fitzgerald Book reviews . . . . . . . . . . . . . . 376--378
M. Hennessy and
H. Lin Proof systems for message-passing
process algebras . . . . . . . . . . . . 379--407
David Scholefield Real-time refinement in Manna and
Pnueli's temporal logic . . . . . . . . 408--427
Christoph Beierle and
Egon Börger Specification and correctness proof of a
WAM extension with abstract type
constraints . . . . . . . . . . . . . . 428--462
Stefan Rönn Invariants and closures in the theory of
rewrite systems . . . . . . . . . . . . 463--478
A. P. Martin and
P. H. B. Gardiner and
J. C. P. Woodcock A tactic calculus --- abridged version 479--489
Mark Harman and
Dan Simpson and
Sebastian Danicic Slicing programs in the presence of
errors . . . . . . . . . . . . . . . . . 490--497
Carron Kirkwood Book review . . . . . . . . . . . . . . 498--498
Nancy Lynch and
Frits Vaandrager Action transducers and timed automata 499--538
Christoph Beierle and
Egon Börger Refinement of a typed WAM extension by
polymorphic order-sorted types . . . . . 539--564
Michael Spivey Richer types for Z . . . . . . . . . . . 565--584
Scott A. Smolka and
Bernhard Steffen Priority as extremal probability . . . . 585--606
Susanne Graf and
Bernhard Steffen and
Gerald Lüttgen Compositional minimisation of finite
state systems using interface
specifications . . . . . . . . . . . . . 607--616
Carroll Morgan and
Annabelle McIver and
Karen Seidel and
J. W. Sanders Refinement-oriented probability for CSP 617--647
Alban Ponse Computable processes and bisimulation
equivalence . . . . . . . . . . . . . . 648--678
J. I. Zucker Transformations of normal and inverted
function tables . . . . . . . . . . . . 679--705
Ruth Breu and
Elena Zucca An algebraic semantic framework for
object oriented languages with
concurrency (extended abstract) . . . . 706--715
Murali Sitaraman Impact of performance considerations on
formal specification design . . . . . . 716--736
Marc Bezem and
Roland Bol and
Jan Friso Groote Formalizing process algebraic
verifications in the calculus of
constructions . . . . . . . . . . . . . 1--48
Jens Palsberg and
Mitchell Wand and
Patrick O'Keefe Type inference with non-structural
subtyping . . . . . . . . . . . . . . . 49--67
M. J. A. Caswell Equivalence of formal semantics
definition methods . . . . . . . . . . . 68--77
Susumu Nishimura A strict functional language with cyclic
recursive data . . . . . . . . . . . . . 78--97
Stein Krogdahl and
Olav Lysne Verifying a distributed list system: A
case history . . . . . . . . . . . . . . 98--118
Maciej Koutny and
Luigi V. Mancini and
Giuseppe Pappalardo Two implementation relations and the
correctness of communicating replicated
processes . . . . . . . . . . . . . . . 119--148
Qiwen Xu and
Willem-Paul de Roever and
Jifeng He The rely-guarantee method for verifying
shared variable concurrent programs . . 149--174
C. J. Fidge and
A. J. Wellings An action-based formal model for
concurrent real-time systems . . . . . . 175--207
Wim H. Hesselink A mechanical proof of Segall's PIF
algorithm . . . . . . . . . . . . . . . 208--226
Jeannette Wing Editorial . . . . . . . . . . . . . . . 227--228
Donald Sannella and
Andrzej Tarlecki Essential concepts of algebraic
specification and program development 229--269
Rutger M. Dijkstra and
Beverly A. Sanders A predicate transformer for the progress
property `to-always' . . . . . . . . . . 270--282
Michael R. Hansen and
Zhou Chaochen Duration calculus: Logical foundations 283--330
Brian J. Ross Running programs backwards: The logical
inversion of imperative computation . . 331--348
C. O'Halloran and
R. Arthan and
D. King Using a formal specification
contractually . . . . . . . . . . . . . 349--358
Charanjit S. Jutla and
Josyula R. Rao A methodology for designing proof rules
for fair parallel programs . . . . . . . 359--378
Ralf Kneuper Limits of formal methods . . . . . . . . 379--394
Mark B. Josephs and
Andrew M. Bailey The Use of SI--Algebra in the design of
sequencer circuits . . . . . . . . . . . 395--408
Ekkart Kindler and
Wolfgang Reisig and
Hagen Völzer and
Rolf Walter Petri net based verification of
distributed algorithms: An example . . . 409--424
Christel Baier and
Mila Majster-Cederbaum The connection between initial and
unique solutions of domain equations in
the partial order and metric approach 425--445
John Cooke Editorial . . . . . . . . . . . . . . . 447--447
Wim H. Hesselink Theories for mechanical proofs of
imperative programs . . . . . . . . . . 448--468
Ralph Back and
Jim Grundy and
Joakim von Wright Structured calculational proof . . . . . 469--483
Catherine Parent-Vigouroux Verifying programs in the calculus of
inductive constructions . . . . . . . . 484--517
Peter M. W. Knijnenburg and
Joost N. Kok The semantics of the combination of
atomized statements and parallel choice 518--536
John O'Leary and
Geoffrey Brown and
Wayne Luk Verified compilation of communicating
processes into clocked circuits . . . . 537--559
Ingrid Rewitzky and
Chris Brink Unification of Four Versions of Program
Semantics . . . . . . . . . . . . . . . 1--29
Henri Korver and
Alex Sellink A Formal Axiomatization for Alphabet
Reasoning with Parametrized Processes 30--42
Henri Korver and
Alex Sellink Example Verifications Using Alphabet
Axioms . . . . . . . . . . . . . . . . . 43--58
Gary T. Leavens and
Jeannette M. Wing Protective Interface Specifications . . 59--75
Joseph M. Morris and
Alexander Bunkenburg Partiality and Nondeterminacy in Program
Proofs . . . . . . . . . . . . . . . . . 76--96
John Derrick and
Eerke Boiten and
Howard Bowman and
Maarten Steen Specifying and Refining Internal
Operations in Z . . . . . . . . . . . . 125--159
Philippe de Groote and
Guy Perrier A Note on Kobayashi's and Yonezawa's
``Asynchronous Communication Model Based
on Linear Logic'' . . . . . . . . . . . 160--170
Tobias Nipkow Winskel is (almost) Right: Towards a
Mechanized Semantics Textbook . . . . . 171--186
Ian J. Hayes Expressive Power of Specification
Languages . . . . . . . . . . . . . . . 187--192
J. Dingel and
D. Garlan and
S. Jha and
D. Notkin Towards a Formal Treatment of Implicit
Invocation Using Rely\slash Guarantee
Reasoning . . . . . . . . . . . . . . . 193--213
Jan Eppo Jonker Knaster--Tarski Revisited . . . . . . . 214--232
Richard F. Paige Heterogeneous Notations for Pure Formal
Method Integration . . . . . . . . . . . 233--242
Martin C. Henson The Standard Logic of Z is Inconsistent 243--247
Luc Léonard and
Guy Leduc A Formal Definition of Time in LOTOS . . 248--266
Ana Cavalcanti and
Jim Woodcock ZRC --- A Refinement Calculus for Z . . 267--289
Eric C. R. Hehner Formalization of Time and Space . . . . 290--306
Anonymous Book Reviews . . . . . . . . . . . . . . 307--310
Stefania Gnesi and
Diego Latella Editorial . . . . . . . . . . . . . . . 311--312
Marco Bernardo and
Roberto Gorrieri and
Marco Roccetti Formal Performance Modelling and
Evaluation of an Adaptive Mechanism for
Packetised Audio over the Internet . . . 313--337
Arne Borälv Case Study: Formal Verification of a
Computerized Railway Interlocking . . . 338--360
A. Cimatti and
F. Giunchiglia and
G. Mongardi and
D. Romano and
F. Torielli and
P. Traverso Formal Verification of a Railway
Interlocking System using Model Checking 361--380
P. Ochsenschläger and
J. Repp and
R. Rieke and
U. Nitsche The SH-Verification Tool ---
Abstraction-Based Verification of
Co-operating Systems . . . . . . . . . . 381--404
G. P. Faconti and
M. Massink Modelling and Verification of PREMO
Synchronisable Objects . . . . . . . . . 405--434
Jan Friso Groote and
Bas Luttik and
Jos van Wamel Editorial . . . . . . . . . . . . . . . 435--435
Marie-Claude Gaudel and
Perry R. James Testing Algebraic Data Types and
Processes: A Unifying Theory . . . . . . 436--451
Stuart Anderson and
Konstantinos Tourlas Design for Proof: An Approach to the
Design of Domain--Specific Languages . . 452--468
Dennis Dams and
Rob Gerth and
Bart Knaack and
Ruurd Kuiper Partial-order Reduction Techniques for
Real-time Model Checking . . . . . . . . 469--482
Theofanis Vassiliou-Gioles and
Ina Schieferdecker Case Study in Protocol Validation:
Validating an ATM Signalling Protocol 483--508
Carron Shankland and
Mark van der Zwaag The Tree Identify Protocol of IEEE 1394
in $ \mu $CRL . . . . . . . . . . . . . 509--531
Juan Bicarregui and
Brian Matthews and
Brian Ritchie and
Sten Agerholm Investigating the Integration of two
Formal Methods . . . . . . . . . . . . . 532--549
H. Bowman and
G. Faconti and
J.-P. Katoen and
D. Latella and
M. Massink Automatic Verification of a
Lip-Synchronisation Protocol Using
Uppaal . . . . . . . . . . . . . . . . . 550--575
David Duce and
David Duke and
Giorgio Faconti and
Ivan Herman The Changing Face of Standardization: A
Place for Formal Methods? . . . . . . . 1--20
Dang Van Hung and
Zhou Chaochen Probabilistic Duration Calculus for
Continuous Time . . . . . . . . . . . . 21--44
Wim H. Hesselink The Verified Incremental Design of a
Distributed Spanning Tree Algorithm:
Extended Abstract . . . . . . . . . . . 45--55
K. Rustan M. Leino Computing Permutation Encodings . . . . 56--74
Brendan P. Mahony The Least Conjunctive Refinement and
Promotion in the Refinement Calculus . . 75--105
David Duke and
Bob Fields and
Michael D. Harrison A Case Study in the Specification and
Analysis of Design Alternatives for a
User Interface . . . . . . . . . . . . . 107--131
Howard Bowman and
Giorgio Faconti Analysing Cognitive Behaviour using
LOTOS and Mexitl . . . . . . . . . . . . 132--159
Monica Nesi Formalising a Value-Passing Calculus in
HOL . . . . . . . . . . . . . . . . . . 160--199
Richard Bird and
Ross Paterson Generalised folds for nested datatypes 200--222
Anonymous Editorial . . . . . . . . . . . . . . . 223--224
Yves Bertot The CtCoq System: Design and
Architecture . . . . . . . . . . . . . . 225--243
Richard Bornat and
Bernard Sufrin A Minimal Graphical User Interface for
the Jape Proof Calculator . . . . . . . 244--271
Joseph Goguen Social and Semiotic Analyses for Theorem
Prover User Interface Design 1 . . . . . 272--301
Andrew Ireland and
Michael Jackson and
Gordon Reid Interactive Proof Critics . . . . . . . 302--325
Jörg Siekmann and
Stephan Hess and
Christoph Benzmüller and
Lassaad Cheikhrouhou and
Armin Fiedler and
Helmut Horacek and
Michael Kohlhase and
Karsten Konrad and
Andreas Meier and
Erica Melis and
Martin Pollet and
Volker Sorge L$ \Omega $UI: Lovely $ \Omega $MEGA
User Interface . . . . . . . . . . . . . 326--342
Koichi Takahashi and
Masami Hagiya Proving as Editing HOL Tactics . . . . . 343--357
Martin C. Henson and
Steve Reeves Revising Z: Part I --- logic and
semantics . . . . . . . . . . . . . . . 359--380
Martin C. Henson and
Steve Reeves Revising Z: Part II --- logical
development . . . . . . . . . . . . . . 381--401
A. Prasad Sistla and
Viktor Gyuris Parameterized Verification of Linear
Networks using Automata as Invariants 402--425
Philippe Audebaud and
Elena Zucca Deriving Proof Rules from Continuation
Semantics . . . . . . . . . . . . . . . 426--447
Olivier Roux and
Vlad Rusu and
Franck Cassez Hybrid Verifications of Reactive
Programs . . . . . . . . . . . . . . . . 448--471
Steve King `The Standard Logic for Z': A
Clarification . . . . . . . . . . . . . 472--473
Amy Felty and
Frank Stomp Cache Coherency in SCI: Specification
and a Sketch of Correctness . . . . . . 475--497
R. Banach and
M. Poppleton Sharp Retrenchment, Modulated Refinement
and Simulation . . . . . . . . . . . . . 498--540
Thomas Kleymann Hoare Logic and Auxiliary Variables . . 541--566
D. H. Pitt and
M. W. Shields Overtaking in Asynchronous Periodic
Systems . . . . . . . . . . . . . . . . 567--590
Daniel Jackson and
Yu-Chung Ng and
Jeannette Wing A Nitpick Analysis of Mobile IPv6 . . . 591--615
Wim H. Hesselink Predicate Transformers for Recursive
Procedures with Local Variables . . . . 616--636
Diego Latella and
Istvan Majzik and
Mieke Massink Automatic Verification of a Behavioural
Subset of UML Statechart Diagrams Using
the SPIN Model-checker . . . . . . . . . 637--664
David Duke and
David Duce The Formalization of a Cognitive
Architecture and its Application to
Reasoning About Human Computer
Interaction . . . . . . . . . . . . . . 665--689
Hans-Jörg Kreowski and
Sabine Kuske Graph Transformation Units with
Interleaving Semantics . . . . . . . . . 690--723
J. A. Bergstra and
M. E. Loots Program Algebra for Component Code . . . 1--17
Ralph-Johan Back and
Anna Mikhajlova and
Joakim von Wright Class Refinement as Semantics of Correct
Object Substitutability . . . . . . . . 18--40
Martin von Mohrenschildt Algebraic Composition of Function Tables 41--51
Antonio Cau Composing and Refining Dense Temporal
Logic Specifications . . . . . . . . . . 52--70
Stephan Diehl Natural Semantics--Directed Generation
of Compilers and Abstract Machines . . . 71--99
Rajeev Joshi and
Jayadev Misra Maximally Concurrent Programs . . . . . 100--119
Stephen Paynter and
Jim Armstrong and
Jan Haveman ADL: An Activity Description Language
for Real-Time Networks . . . . . . . . . 120--144
Jeanette Wing and
Jim Woodcock The First World Congress on Formal
Methods in the Development of Computing
Systems . . . . . . . . . . . . . . . . 145--146
Heike Wehrheim Data Abstraction Techniques in the
Validation of CSP--OZ Specifications . . 147--164
Steve Schneider Abstraction and Testing in CSP . . . . . 165--181
Michael Butler csp2B: A Practical Approach to Combining
CSP and B . . . . . . . . . . . . . . . 182--198
Andrew P. Martin Relating Z and First-Order Logic . . . . 199--209
Tim Denvir and
José Oliveira and
Nico Plat The Cash-Point (ATM) `Problem' . . . . . 211--215
Peter Gorm Larsen and
Paul Mukherjee and
Kim Sunesen Using VDMTools to Model and Validate the
Cash Dispenser Example . . . . . . . . . 216--217
Anca Browne and
Bernd Finkbeiner and
Zohar Manna and
Henny Sipma The `Cash-Point' Service: A Verification
Case Study Using STeP . . . . . . . . . 218--219
Henning Dierks and
Josef Tapken Modelling and Verifying of a `Cash-Point
Service' Using MOBY\slash PLC . . . . . 220--221
Vahur Kotkas and
Peep Küngas and
Mait Harf The Cash-Point Service in NUT . . . . . 222--224
Oscar Slotosch Modelling and Validation: AUTOFOCUS and
Quest . . . . . . . . . . . . . . . . . 225--227
Sophie Dupuy and
Lydie du Bousquet A Multi-formalism Approach for the
Validation of UML Models . . . . . . . . 228--230
Timo Aaltonen and
Pertti Kellomäki and
Risto Pitkänen Specifying Cash-Point with DisCo . . . . 231--232
Sylvan Dissoubray and
Bernard Dion Design of an Automatic Teller Machine
with Esterel Studio . . . . . . . . . . 233--236
Richard Butterworth and
Ann Blandford and
David Duke Demonstrating the Cognitive Plausibility
of Interactive System Specifications . . 237--259
Gavin J. Doherty and
José C. Campos and
Michael D. Harrison Representational Reasoning and
Verification . . . . . . . . . . . . . . 260--277
Kaisa Sere and
Marina Waldén Data Refinement of Remote Procedures . . 278--297
A. C. J. Fox and
N. A. Harman Algebraic Models of Correctness for
Microprocessors . . . . . . . . . . . . 298--312
Ralph-Johan Back and
Joakim von Wright Encoding, Decoding and Data Refinement 313--349
Rachel Cardell-Oliver Conformance Tests for Real-Time Systems
with Timed Automata Specifications . . . 350--371
Mark Staples Interfaces for Refining Recursion and
Procedures . . . . . . . . . . . . . . . 372--391
C. Tofts Symbolic Approaches to Probability
Distributions in Process Algebra . . . . 392--415
Cliff Jones Editorial . . . . . . . . . . . . . . . 417--417
Mike Holcombe What are X-Machines? . . . . . . . . . . 418--422
R. M. Hierons and
M. Harman Testing Conformance to a
Quasi--Non-Deterministic Stream
X-Machine . . . . . . . . . . . . . . . 423--442
Florentin Ipate and
Mike Holcombe Generating Test Sets from
Non--Deterministic Stream X-Machines . . 443--458
Marian Gheorghe Generalised Stream X-Machines and
Cooperating Distributed Grammar Systems 459--472
Tudor B\ual\uanescu Generalised Stream X-Machines with
Output Delimited Type . . . . . . . . . 473--484
Anthony J. Cowling and
Horia Georgescu and
Cristina Vertan A Structured Way to Use Channels for
Communication in X-Machine Systems . . . 485--500
Radu Grosu and
Ketil Stòlen Stream-Based Specification of Mobile
Systems . . . . . . . . . . . . . . . . 1--31
Steven Vickers and
Gillian Hill Presheaves as Configured Specifications 32--49
José J. Pazos Arias and
Jorge García Duque SCTL-MUS: A Formal Methodology for
Software Development of Distributed
Systems. A Case Study . . . . . . . . . 50--91
John Cooke and
Tim Denvir Editorial . . . . . . . . . . . . . . . 93--93
Carsten Sühl An Overview of the Integrated Formalism
RT-Z . . . . . . . . . . . . . . . . . . 94--110
John Derrick and
Eerke Boiten Combining Component Specifications in
Object-Z and CSP . . . . . . . . . . . . 111--127
Graeme Smith and
Ian Hayes An Introduction to Real-Time Object-Z 128--141
Brendan Mahony and
Jin Song Dong Deep Semantic Links of TCSP and
Object-Z: TCOZ Approach . . . . . . . . 142--160
Martin Große-Rhode Compositional Comparison of Formal
Software Specifications Using
Transformation Systems . . . . . . . . . 161--186
David E. Rydeheard and
Donald T. Sannella A Collection of Papers and Memoirs
Celebrating the Contribution of Rod
Burstall to Advances in Computer Science 187--193
Eleanor Kerse Ode to Rod Burstall . . . . . . . . . . 194--194
Peter Landin Rod Burstall: A Personal Note . . . . . 195--195
Robin Popplestone POP, A Broad-Spectrum Programming
Language, 1967--2002 . . . . . . . . . . 196--213
David MacQueen Should ML be Object-Oriented? . . . . . 214--232
Alberto Pettorossi and
Maurizio Proietti The List Introduction Strategy for the
Derivation of Logic Programs . . . . . . 233--251
Michel Bidoit and
Donald Sannella and
Andrzej Tarlecki Architectural Specifications in CASL . . 252--273
Joseph Goguen and
Grigore Rosu Institution Morphisms . . . . . . . . . 274--307
Edmund Robinson Variations on Algebra: Monadicity and
Generalisations of Equational Theories 308--326
James J. Leifer and
Robin Milner Shallow Linear Action Graphs and their
Embeddings . . . . . . . . . . . . . . . 327--340
Murdoch J. Gabbay and
Andrew M. Pitts A New Approach to Abstract Syntax with
Variable Binding . . . . . . . . . . . . 341--363
Gordon Plotkin Three Inadequate Models . . . . . . . . 364--385
Robert Pollack Dependently Typed Records in Type Theory 386--402
Jon Whittle and
Alan Bundy and
Richard Boulton Proofs-as-Programs as a Framework for
the Design of an Analogy-Based ML Editor 403--421
Henk Barendregt The Ancient Theory of Mind . . . . . . . 422--429
Florentin Ipate and
Mike Holcombe Testing Conditions for Communicating
Stream X-machine Systems . . . . . . . . 431--446
Éric Badouel and
Beno\^\it Caillaud and
P. Darondeau Distributing Finite Automata Through
Petri Net Synthesis . . . . . . . . . . 447--470
Stein Krogdahl and
Olav Lysne On Verification of Parallel
Message-Passing Processes . . . . . . . 471--492
John Cooke Editorial . . . . . . . . . . . . . . . 1--1
Michael Butler On the Use of Data Refinement in the
Development of Secure Communications
Systems . . . . . . . . . . . . . . . . 2--34
David H. Pitt and
Michael Shields Local Invariance . . . . . . . . . . . . 35--54
Hartmann J. Genrich Dynamical Quantities in Net Systems . . 55--89
Cliff Jones Editorial . . . . . . . . . . . . . . . 91--91
Krzysztof R. Apt Edsger Wybe Dijkstra (1930--2002): A
Portrait of a Genius . . . . . . . . . . 92--98
Edsger W. Dijkstra EWD1300: The Notational Conventions I
Adopted, and Why . . . . . . . . . . . . 99--107
Yifeng Chen Generic Composition . . . . . . . . . . 108--122
J. Dingel A Refinement Calculus for
Shared-Variable Parallel and Distributed
Programming . . . . . . . . . . . . . . 123--197
John Cooke and
Savi Maharaj and
Judi Romijn and
Carron Shankland Editorial . . . . . . . . . . . . . . . 199--199
Savi Maharaj and
Judi Romijn and
Carron Shankland IEEE 1394 Tree Identify Protocol:
Introduction to the Case Study . . . . . 200--214
Jean-Raymond Abrial and
Dominique Cansell and
Dominique Méry A Mechanically Proved and Incremental
Development of IEEE 1394 Tree Identify
Protocol . . . . . . . . . . . . . . . . 215--227
Alberto Verdejo and
Isabel Pita and
Narciso Martí-Oliet Specification and Verification of the
Tree Identify Protocol of IEEE 1394 in
Rewriting Logic . . . . . . . . . . . . 228--246
M. Calder and
A. Miller Using SPIN to Analyse the Tree
Identification Phase of the IEEE 1394
High-Performance Serial Bus (FireWire)
Protocol . . . . . . . . . . . . . . . . 247--266
Viktor Schuppan and
Armin Biere Verifying the IEEE 1394 FireWire Tree
Identify Protocol with SMV . . . . . . . 267--280
Colin Fidge and
Carron Shankland But What if I Don't Want to Wait
Forever? . . . . . . . . . . . . . . . . 281--294
Marta Kwiatkowska and
Gethin Norman and
Jeremy Sproston Probabilistic Model Checking of Deadline
Properties in the IEEE 1394 FireWire
Root Contention Protocol . . . . . . . . 295--318
Judi Romijn False Loop Detection in the IEEE 1394
Tree Identify Phase . . . . . . . . . . 319--327
Mariëlle Stoelinga Fun with FireWire: A Comparative Study
of Formal Verification Methods Applied
to the IEEE 1394 Root Contention
Protocol . . . . . . . . . . . . . . . . 328--337
Anonymous Editorial . . . . . . . . . . . . . . . 339--339
Anonymous Obituary . . . . . . . . . . . . . . . . 340--341
Dimitrie O. Paun and
Marsha Chechik On Closure Under Stuttering . . . . . . 342--368
Hidetaka Kondoh Abstract Data Types Can Have Inequations 369--399
John Derrick and
Graeme Smith Structural Refinement of Systems
Specified in Object-Z and CSP . . . . . 1--27
Marcel Oliveira and
Ana Cavalcanti and
Jim Woodcock ArcAngel: a Tactic Language for
Refinement . . . . . . . . . . . . . . . 28--47
Martin C. Henson and
Steve Reeves A Logic for Schema-Based Program
Development . . . . . . . . . . . . . . 48--83
He Jifeng and
Xu Qiwen Advanced Features of Duration Calculus
and Their Applications in Sequential
Hybrid Programs . . . . . . . . . . . . 84--99
Anonymous Editorial . . . . . . . . . . . . . . . 101--102
R. J. R. Back and
J. von Wright Compositional Action System Refinement 103--117
Jim Davies and
Charles Crichton Concurrency and Refinement in the
Unified Modeling Language . . . . . . . 118--145
Ana Cavalcanti and
Augusto Sampaio and
Jim Woodcock A Refinement Strategy for Circus . . . . 146--181
John Derrick and
Eerke Boiten Relational Concurrent Refinement . . . . 182--214
Emil Sekerinski Exploring Tabular Verification and
Refinement . . . . . . . . . . . . . . . 215--236
Egon Börger The ASM Refinement Method . . . . . . . 237--257
Luke Wildman and
Colin Fidge and
David Carrington The Variety of Variables in Automated
Real-Time Refinement . . . . . . . . . . 258--279
Bernhard K. Aichernig Mutation Testing in the Refinement
Calculus . . . . . . . . . . . . . . . . 280--295
Manfred Broy and
Gerald Lüttgen and
Michael Mendler Editorial: Where Theory and Practice
Meet . . . . . . . . . . . . . . . . . . 297--298
Simon Gay and
Rajagopal Nagarajan Intensional and Extensional Semantics of
Dataflow Programs . . . . . . . . . . . 299--318
Karl Lermer and
Colin J. Fidge and
Ian J. Hayes Linear Approximation of Execution-Time
Constraints . . . . . . . . . . . . . . 319--348
Jörn W. Janneck Actors and their Composition . . . . . . 349--369
Victor Bos and
Jeroen Kleijn Redesign of a Systems Engineering
Language: Formalisation of $ \chi $ . . 370--389
Martin Fränzle and
Jürgen Niehaus and
Alexander Metzner and
Werner Damm A Semantics for Distributed Execution of
Statemate . . . . . . . . . . . . . . . 390--405
Michael J. C. Gordon Validating the PSL/Sugar Semantics Using
Automated Reasoning . . . . . . . . . . 406--421
Anonymous Content of Volume 15 --- 2003 . . . . . 422--422
Cliff Jones and
John Cooke Editorial . . . . . . . . . . . . . . . 1--1
John S. Fitzgerald Formal Methods Europe Update . . . . . . 2--3
C. B. Jones and
D. J. Cooke and
Christiane Notarmarco Online First Publication . . . . . . . . 4--4
Antónia Lopes and
José Luiz Fiadeiro Superposition: composition vs refinement
of non-deterministic, action-based
systems . . . . . . . . . . . . . . . . 5--18
Clare Martin and
Jeremy Gibbons and
Ian Bayley Disciplined, efficient, generalised
folds for nested datatypes . . . . . . . 19--35
A. Stewart and
M. Clint and
J. Gabarró Barrier synchronisation: Axiomatisation
and relaxation . . . . . . . . . . . . . 36--50
Richard F. Paige and
Jonathan S. Ostroff ERC --- An object-oriented refinement
calculus for Eiffel . . . . . . . . . . 51--79
C. T. Carr and
T. M. McGinnity and
L. J. McDaid Integration of UML and VHDL--AMS for
analogue system modelling . . . . . . . 80--94
Cliff Jones and
Michael R. Hansen Editorial . . . . . . . . . . . . . . . 95--95
Rana Barua Completeness of a combination of
neighbourhood logic and temporal logic 96--103
Henning Dierks Comparing model checking and logical
reasoning for real-time systems . . . . 104--120
Martin Fränzle Model-checking dense-time Duration
Calculus . . . . . . . . . . . . . . . . 121--139
Zhiming Liu and
Anders P. Ravn and
Xiaoshan Li Unifying proof methodologies of duration
calculus and timed linear temporal logic 140--154
Li Xuandong and
Zhao Jianhua and
Zheng Tao and
Li Yong and
Zheng Guoliang Duration-constrained regular expressions 155--163
Manfred Broy and
Gerald Lüttgen and
Michael Mendler Editorial . . . . . . . . . . . . . . . 165--165
María del Mar Gallardo and
Pedro Merino and
Ernesto Pimentel A generalized semantics of PROMELA for
abstract model checking . . . . . . . . 166--193
I. Krüger and
W. Prenninger and
R. Sandner Broadcast MSCs . . . . . . . . . . . . . 194--209
Edward A. Lee and
Yuhong Xiong A behavioral type system and its
application in Ptolemy II . . . . . . . 210--237
Natalia López and
Manuel Núñez and
Fernando Rubio An integrated framework for the
performance analysis of asynchronous
communicating stochastic processes . . . 238--262
Mirabelle Nebut Specification and analysis of
synchronous reactions . . . . . . . . . 263--291
Simone Tini Timed CCP compositionally embeds Argos
and Lustre . . . . . . . . . . . . . . . 292--312
Stefan Hallerstede and
Michael Butler Performance analysis of probabilistic
action systems . . . . . . . . . . . . . 313--331
S. E. Paynter and
N. Henderson and
J. M. Armstrong Ramifications of metastability in bit
variables explored via Simpson's
$4$-slot mechanism . . . . . . . . . . . 332--351
Solange Coupet-Grimal and
Line Jakubiec Certifying circuits in Type Theory . . . 352--373
Florentin Ipate Complete deterministic stream X-machine
testing . . . . . . . . . . . . . . . . 374--386
Wim H. Hesselink An assertional proof for a construction
of an atomic variable . . . . . . . . . 387--393
J. N. Reed and
J. E. Sinclair and
A. W. Roscoe Responsiveness of interoperating
components . . . . . . . . . . . . . . . 394--411
D. Herzberg and
M. Broy Modeling layered distributed
communication systems . . . . . . . . . 1--18
Jan Friso Groote and
François Monin and
Jan Springintveld A computer checked algebraic
verification of a distributed summation
algorithm . . . . . . . . . . . . . . . 19--37
A. Cook and
A. Ireland and
G. Michaelson and
N. Scaife Discovering applications of higher order
functions through proof planning . . . . 38--57
Sidi O. Ehmety and
Lawrence C. Paulson Mechanizing compositional reasoning for
concurrent systems: some lessons . . . . 58--68
Ralph-Johan Back and
Viorel Preoteasa An algebraic treatment of procedure
refinement to support mechanical
verification . . . . . . . . . . . . . . 69--90
Michael Leuschel Guest Editorial . . . . . . . . . . . . 91--92
A. W. Roscoe On the expressive power of CSP
refinement . . . . . . . . . . . . . . . 93--112
Michael Huth Refinement is complete for
implementations . . . . . . . . . . . . 113--137
Stefano Cattani and
Marta Kwiatkowska A refinement-based process algebra for
timed automata . . . . . . . . . . . . . 138--159
Gethin Norman and
David Parker and
Marta Kwiatkowska and
Sandeep Shukla and
Rajesh Gupta Using probabilistic model checking for
dynamic power management . . . . . . . . 160--176
Bram De Wachter and
Alexandre Genon and
Thierry Massart and
Cédric Meuter The formal design of distributed
controllers with $_d$SL and Spin . . . . 177--200
Elsa Gunter and
Doron Peled Model checking, testing and verification
working together . . . . . . . . . . . . 201--221
Roberto Bagnara and
Patricia M. Hill and
Enea Zaffanella Not necessarily closed convex polyhedra
and the double description method . . . 222--257
John Cooke Editorial . . . . . . . . . . . . . . . 259--259
S. Gürgens and
C. Rudolph Security analysis of efficient (Un-)
fair non-repudiation protocols . . . . . 260--276
Andrew D. Gordon and
Riccardo Pucella Validating a web service security
abstraction by typing . . . . . . . . . 277--318
Martin De Wulf and
Laurent Doyen and
Jean-François Raskin Almost ASAP semantics: from timed models
to timed implementations . . . . . . . . 319--341
Bahareh Badban and
Wan Fokkink and
Jan Friso Groote and
Jun Pang and
Jaco van de Pol Verification of a sliding window
protocol in $ \mu $CRL and PVS . . . . . 342--388
E. Boiten and
J. Derrick and
G. Smith Guest Editorial Integrated Formal
Methods . . . . . . . . . . . . . . . . 389--389
Steve Schneider and
Helen Treharne CSP theorems for communicating B
machines . . . . . . . . . . . . . . . . 390--422
Bernhard Beckert and
Steffen Schlager Refinement and retrenchment for
programming language data types . . . . 423--442
Jifeng He and
Dang Van Hung and
Geguang Pu and
Zongyan Qiu and
Wang Yi Exploring optimal solution to
hardware/software partitioning for
synchronous model . . . . . . . . . . . 443--460
Sagar Chaki and
Edmund Clarke and
Joël Ouaknine and
Natasha Sharygina and
Nishant Sinha Concurrent software verification with
states, events, and deadlocks . . . . . 461--483
J. Derrick and
M. Harman and
R. M. Hierons Guest Editorial . . . . . . . . . . . . 1--2
K. Bogdanov and
M. Holcombe and
F. Ipate and
L. Seed and
S. Vanak Testing methods for X-machines: a review 3--30
Mike Stannett Simulation testing of automata . . . . . 31--41
Sergiy A. Vilkomir and
Jonathan P. Bowen From MC\slash DC to RC\slash DC:
formalization and analysis of
control-flow testing criteria . . . . . 42--62
H. H. Hallal and
S. Boroday and
A. Petrenko and
A. Ulrich A formal approach to property testing in
causally consistent distributed traces 63--83
Hasan Ural and
Craig Williams Constructing checking sequences for
distributed testing . . . . . . . . . . 84--101
David W. Binkley and
Sebastian Danicic and
Mark Harman and
John Howroyd and
Lahcen Ouarbya A formal relationship between program
slicing and partial evaluation . . . . . 103--119
Steve McKeever and
Wayne Luk Provably-correct hardware compilation
tools based on pass separation
techniques . . . . . . . . . . . . . . . 120--142
J. C. Bicarregui and
C. A. R. Hoare and
J. C. P. Woodcock The verified software repository: a step
towards the verifying compiler . . . . . 143--151
K. Lermer and
C. J. Fidge Procedure compilation in the refinement
calculus . . . . . . . . . . . . . . . . 152--180
Christie Bolton and
Jim Davies A singleton failures semantics for
Communicating Sequential Processes . . . 181--210
H. Fecher and
M. Majster-Cederbaum Action Refinement Applied to Late
Decisions . . . . . . . . . . . . . . . 211--230
Regivan H. Nunes Santiago and
Benjamín R. Callejas Bedregal and
Benedito Melo Acióly Formal Aspects of Correctness and
Optimality of Interval Computations . . 231--243
Sabine Glesner Finite Integer Computations: An
Algebraic Foundation for Their
Correctness . . . . . . . . . . . . . . 244--262
Eerke Boiten and
Michael Butler Guest Editorial: Editorial for the FAC
Special Issue based on derivative papers
from ``Refine '05'' . . . . . . . . . . 263--263
Graeme Smith and
John Derrick Verifying data refinements using a model
checker . . . . . . . . . . . . . . . . 264--287
Ana Cavalcanti and
Jim Woodcock and
Steve Dunne Angelic nondeterminism in the unifying
theories of programming . . . . . . . . 288--307
Steve Schneider and
Thai Son Hoang and
Ken Robinson and
Helen Treharne Tank monitoring: a pAMN case study . . . 308--328
Moshe Deutsch and
Martin C. Henson An analysis of refinement in an abortive
paradigm . . . . . . . . . . . . . . . . 329--363
Martin C. Henson and
Moshe Deutsch and
Besnik Kajtazi The specification logic $ \nu $Z . . . . 364--395
Jennifer Tenzer and
Perdita Stevens On modelling recursive calls and
callbacks with two variants of Unified
Modelling Language state diagrams . . . 397--420
K. Subramani and
C. Tauras An approximation algorithm for state
minimization in 2-MDFAs . . . . . . . . 421--431
F. W. Vaandrager and
A. L. de Groot Analysis of a biphase mark protocol with
\sc Uppaal and PVS . . . . . . . . . . . 433--458
Howard Bowman and
Rodolfo Gómez How to stop time stopping . . . . . . . 459--493
David Pym and
Chris Tofts A Calculus and logic of resources and
processes . . . . . . . . . . . . . . . 495--517
John Cooke Editorial . . . . . . . . . . . . . . . 1--1
Jane Hillston and
Le\"\ila Kloul Formal techniques for performance
analysis: blending SAN and PEPA . . . . 3--33
Nikos Gorogiannis and
Mark Ryan Minimal refinements of specifications in
model and temporal logics . . . . . . . 35--62
David Basin and
Hironobu Kuruma and
Kunihiko Miyazaki and
Kazuo Takaragi and
Burkhart Wolff Verifying a signature architecture: a
comparative case study . . . . . . . . . 63--91
Ruggero Lanotte and
Andrea Maggiolo-Schettini and
Angelo Troina Parametric probabilistic transition
systems for system design and analysis 93--109
A. Burns and
T.-M. Lin An engineering process for the
verification of real-time systems . . . 111--136
J. Cooke Editorial (VSTTE Special Issue) . . . . 137--138
Patrice Chalin Are the Logical Foundations of Verifying
Compiler Prototypes Matching user
Expectations? . . . . . . . . . . . . . 139--158
Gary T. Leavens and
K. Rustan M. Leino and
Peter Müller Specification and verification
challenges for sequential
object-oriented programs . . . . . . . . 159--189
Bart Jacobs and
Sjaak Smetsers and
Ronny Wichers Schreur Code-carrying theories . . . . . . . . . 191--203
David A. Naumann On assertion-based encapsulation for
object invariants and simulations . . . 205--224
Egon Börger Construction and analysis of ground
models and their refinements as a
foundation for validating computer-based
systems . . . . . . . . . . . . . . . . 225--241
Aysu Betin-Can and
Tevfik Bultan Highly dependable concurrent programming
using design for verification . . . . . 243--268
Rajeev Joshi and
Gerard J. Holzmann A mini challenge: build a verifiable
filesystem . . . . . . . . . . . . . . . 269--272
Nikos Gorogiannis and
Mark Ryan Minimal refinements of specifications in
modal and temporal logics . . . . . . . 273--273
Ranko Lazic and
Rajagopal Nagarajan Guest Editorial . . . . . . . . . . . . 275--275
Neil Evans and
Helen Treharne Interactive tool support for CSP || B
consistency checking . . . . . . . . . . 277--302
J. N. Reed and
A. W. Roscoe and
J. E. Sinclair Responsiveness and stable revivals . . . 303--319
Damián Barsotti and
Leonor Prensa Nieto and
Alwen Tiu Verification of clock synchronization
algorithms: experiments on a combination
of deductive tools . . . . . . . . . . . 321--341
Konrad Slind and
Scott Owens and
Juliano Iyoda and
Mike Gordon Proof producing synthesis of arithmetic
and cryptographic hardware . . . . . . . 343--362
Milan \vCe\vska and
Pavel Erlebach and
Tomá\vs Vojnar Generalised multi-pattern-based
verification of programs with linear
linked structures . . . . . . . . . . . 363--374
Nathaniel Charlton Program verification with interacting
analysis plugins . . . . . . . . . . . . 375--399
Eun-Young Kang and
Stephan Merz Predicate diagrams for the verification
of real-time systems . . . . . . . . . . 401--413
Cliff Jones and
Jim Woodcock Editorial . . . . . . . . . . . . . . . 415--416
Nikos Gorogiannis and
Mark Ryan Minimal refinements of specifications in
modal and temporal logics . . . . . . . 417--444
J. A. Bergstra and
C. A. Middelburg Thread algebra for strategic
interleaving . . . . . . . . . . . . . . 445--474
Thuy Duong Vu Deciding orthogonal bisimulation . . . . 475--485
Phillip J. Brooke and
Richard F. Paige and
Jeremy L. Jacob A CSP model of Eiffel's SCOOP . . . . . 487--512
Paul Curzon and
Rimvydas Ruk\vs\.enas and
Ann Blandford An approach to formal verification of
human---computer interaction . . . . . . 513--550
Matthew Collinson and
David Pym and
Chris Tofts Errata for \booktitleFormal Aspects of
Computing (2006) 18:495--517 and their
consequences . . . . . . . . . . . . . . 551--554
Cliff Jones and
Jim Woodcock Editorial . . . . . . . . . . . . . . . 1--3
Jim Woodcock and
Susan Stepney and
David Cooper and
John Clark and
Jeremy Jacob The certification of the Mondex
electronic purse to ITSEC Level E6 . . . 5--19
Tahina Ramananandro Mondex, an electronic purse:
specification and refinement checks with
the Alloy model-finding method . . . . . 21--39
Dominik Haneberg and
Gerhard Schellhorn and
Holger Grandy and
Wolfgang Reif Verification of Mondex electronic purses
with KIV: from transactions to a
security protocol . . . . . . . . . . . 41--59
Michael Butler and
Divakar Yadav An incremental development of the Mondex
system in Event-B . . . . . . . . . . . 61--77
Mirco Kuhlmann and
Martin Gogolla Modeling and validating Mondex scenarios
described in UML and OCL with USE . . . 79--100
Chris George and
Anne E. Haxthausen Specification, proof, and model checking
of the Mondex electronic purse using
RAISE . . . . . . . . . . . . . . . . . 101--116
Leo Freitas and
Jim Woodcock Mechanising Mondex with Z/Eves . . . . . 117--139
Brijesh Dongol and
Arjan J. Mooij Streamlining progress-based derivations
of concurrent programs . . . . . . . . . 141--160
Michael Möller and
Ernst-Rüdiger Olderog and
Holger Rasch and
Heike Wehrheim Integrating a formal method into a
software engineering process with UML
and Java . . . . . . . . . . . . . . . . 161--204
Purandar Bhaduri and
S. Ramesh Interface synthesis and protocol
conversion . . . . . . . . . . . . . . . 205--224
Hanifa Boucheneb Interval timed coloured Petri net:
efficient construction of its state
class space preserving linear properties 225--238
Dines Bjòrner John Warner Backus: 3 Dec 1924--17 March
2007 . . . . . . . . . . . . . . . . . . 239--240
Julien Schmaltz and
Dominique Borrione A functional formalization of on chip
communications . . . . . . . . . . . . . 241--258
Florian Kammüller Formalizing non-interference for a
simple bytecode language in Coq . . . . 259--275
Gavin Lowe Specification of communicating
processes: temporal logic versus
refusals-based refinement . . . . . . . 277--294
Steve Reeves and
David Streader Data refinement and singleton failures
refinement are not equivalent . . . . . 295--301
Ivan Cibrario Bertolotti and
Luca Durante and
Riccardo Sisto and
Adriano Valenzano Efficient representation of the
attacker's knowledge in cryptographic
protocols analysis . . . . . . . . . . . 303--348
Kamel Barkaoui and
Manfred Broy and
Ana Cavalcanti and
Antonio Cerone Guest Editorial . . . . . . . . . . . . 349--350
Roberto Barbuti and
Andrea Maggiolo-Schettini and
Paolo Milazzo and
Angelo Troina Bisimulations in calculi modelling
membranes . . . . . . . . . . . . . . . 351--377
Aaron R. Bradley and
Zohar Manna Property-directed incremental invariant
generation . . . . . . . . . . . . . . . 379--405
Giorgio Delzanno and
Roberto Montagna Reachability analysis of fragments of
mobile ambients in AC term rewriting . . 407--428
Raymond Devillers and
Hanna Klaudel and
Maciej Koutny A compositional Petri net translation of
general $ \pi $-calculus terms . . . . . 429--450
Murdoch J. Gabbay and
Aad Mathijssen Capture-avoiding substitution as a
nominal algebra . . . . . . . . . . . . 451--479
Roland Meyer and
Johannes Faber and
Jochen Hoenicke and
Andrey Rybalchenko Model checking Duration Calculus: a
practical approach . . . . . . . . . . . 481--505
Matteo Slanina and
Henny B. Sipma and
Zohar Manna Deductive verification of alternating
systems . . . . . . . . . . . . . . . . 507--560
Cliff Jones Valediction . . . . . . . . . . . . . . 561--561
Sébastien Labbé and
Jean-Pierre Gallois Slicing communicating automata
specifications: polynomial algorithms
for model reduction . . . . . . . . . . 563--595
Robert M. Hierons and
Florentin Ipate Testing a deterministic implementation
against a non-controllable
non-deterministic stream X-machine . . . 597--617
Olga Grinchtein and
Martin Leucker Network invariants for real-time systems 619--635
Jewgenij Botaschanjan and
Manfred Broy and
Alexander Gruler and
Alexander Harhurin and
Steffen Knapp and
Leonid Kof and
Wolfgang Paul and
Maria Spichkova On the correctness of upper layers of
automotive systems . . . . . . . . . . . 637--662
Eerke Boiten Editorial . . . . . . . . . . . . . . . 1--1
Marcel Oliveira and
Ana Cavalcanti and
Jim Woodcock A UTP semantics for Circus . . . . . . . 3--32
Bernhard K. Aichernig and
He Jifeng Mutation testing in UTP . . . . . . . . 33--64
Eerke Boiten and
John Derrick and
Gerhard Schellhorn Relational concurrent refinement part
II: Internal operations and outputs . . 65--102
Liang Zhao and
Xiaojian Liu and
Zhiming Liu and
Zongyan Qiu Graph transformations for
object-oriented refinement . . . . . . . 103--131
Leo Freitas and
Jim Woodcock FDR Explorer . . . . . . . . . . . . . . 133--154
Graeme Smith and
Kirsten Winter Model checking action system refinements 155--186
Lindsay Groves and
Robert Colvin Trace-based derivation of a scalable
lock-free stack algorithm . . . . . . . 187--223
Paul Boca and
Raymond Boute and
David Duce and
José Oliveira Editorial . . . . . . . . . . . . . . . 225--225
Ralph-Johan Back Invariant based programming: basic
approach and teaching experiences . . . 227--244
Peter Gorm Larsen and
John S. Fitzgerald and
Steve Riddle Practice-oriented courses in formal
methods using VDM$^{++}$ . . . . . . . . 245--257
Yih-Kuen Tsay and
Yu-Fang Chen and
Ming-Hsien Tsai and
Kang-Nien Wu and
Wen-Chin Chan and
Chi-Jian Luo and
Jinn-Shu Chang Tool support for learning Büchi automata
and linear temporal logic . . . . . . . 259--275
Wolfgang Schreiner The RISC ProofNavigator: a proving
assistant for program verification in
the classroom . . . . . . . . . . . . . 277--291
Ingo Feinerer and
Gernot Salzer A comparison of tools for teaching
formal software verification . . . . . . 293--301
Richard F. Paige and
Phillip J. Brooke Editorial . . . . . . . . . . . . . . . 303--303
Piotr Nienaltowski and
Bertrand Meyer and
Jonathan S. Ostroff Contracts for concurrency . . . . . . . 305--318
Jonathan S. Ostroff and
Faraz Ahmadi Torshizi and
Hai Feng Huang and
Bernd Schoeller Beyond contracts for concurrency . . . . 319--346
Piotr Nienaltowski Flexible access control policy for SCOOP 347--362
Phillip J. Brooke and
Richard F. Paige Cameo: an alternative model of
concurrency for Eiffel . . . . . . . . . 363--391
Richard Bornat Peter Landin: a computer scientist who
inspired a generation, 5th June
1930--3rd June 2009 . . . . . . . . . . 393--395
Soon-Kyeong Kim and
David Carrington A formalism to describe design patterns
based on role concepts . . . . . . . . . 397--420
Paul Howells and
Mark d'Inverno A CSP model with flexible parallel
termination semantics . . . . . . . . . 421--449
Chunqing Chen and
Jin Song Dong and
Jun Sun A formal framework for modeling and
validating Simulink diagrams . . . . . . 451--483
Daniel Kroening and
Ofer Strichman A framework for Satisfiability Modulo
Theories . . . . . . . . . . . . . . . . 485--494
Cristian Masalagiu and
Wei-Ngan Chin and
\cStefan Andrei and
Vasile Alaiba A rigorous methodology for specification
and verification of business processes 495--510
Antonio Cerone and
Paul Curzon and
David Duce Editorial . . . . . . . . . . . . . . . 511--512
Li Su and
Howard Bowman and
Philip Barnard and
Brad Wyble Process algebraic modelling of
attentional capture and human
electrophysiology in interactive systems 513--539
Rimvydas Ruksenas and
Jonathan Back and
Paul Curzon and
Ann Blandford Verification-guided modelling of
salience and cognitive load . . . . . . 541--569
Thomas Anung Basuki and
Antonio Cerone and
Andreas Griesmayer and
Rudolf Schlatte Model-checking user behaviour using
interacting components . . . . . . . . . 571--588
Judy Bowen and
Steve Reeves Refinement for user interface designs 589--612
Alan Dix and
Masitah Ghazali and
Steve Gill and
Joanna Hare and
Devina Ramduny-Ellis Physigrams: modelling devices for
natural interaction . . . . . . . . . . 613--641
Eerke Boiten and
Michael Butler and
John Derrick and
Graeme Smith Editorial . . . . . . . . . . . . . . . 1--1
Larissa Meinicke and
Kim Solin Refinement algebra for probabilistic
programs . . . . . . . . . . . . . . . . 3--31
Richard Banach and
Gerhard Schellhorn Atomic actions, and their refinements to
isolated protocols . . . . . . . . . . . 33--61
Arjan J. Mooij Invariant-based reasoning about
parameterized security protocols . . . . 63--81
Matthew Collinson and
David Pym Algebra and logic for access control . . 83--104
Daniel Kroening and
Georg Weissenbacher Verification and falsification of
programs with loops using predicate
abstraction . . . . . . . . . . . . . . 105--128
Pascal Mathis and
Simon E. B. Thierry A formalization of geometric constraint
systems and their decomposition . . . . 129--151
Adnan Sherif and
Ana Cavalcanti and
He Jifeng and
Augusto Sampaio A process algebraic framework for
specification and validation of
real-time systems . . . . . . . . . . . 153--191
Jesús Aransay and
Clemens Ballarin and
Julio Rubio Generating certified code from formal
proofs: a case study in homological
algebra . . . . . . . . . . . . . . . . 193--213
J. L. Fiadeiro Editorial . . . . . . . . . . . . . . . 215--216
D. Alrajeh and
J. Kramer and
A. Russo and
S. Uchitel Deriving non-Zeno behaviour models from
goal models using ILP . . . . . . . . . 217--241
Laura Bocchi and
Stephen Gorton and
Stephan Reiff-Marganiec From StPowla processes to SRML models 243--268
Artur Boronat and
José Meseguer An algebraic semantics for MOF . . . . . 269--296
Juan de Lara and
Hans Vangheluwe Automating the transformation-based
analysis of visual languages . . . . . . 297--326
Hartmut Ehrig and
Karsten Ehrig and
Claudia Ermel and
Ulrike Prange Consistent integration of models based
on views of meta models . . . . . . . . 327--344
Naouel Moha and
Yann-Gaël Guéhéneuc and
Anne-Françoise Le Meur and
Laurence Duchien and
Alban Tiberghien From a domain analysis to the
specification and detection of code and
design smells . . . . . . . . . . . . . 345--361
Till Mossakowski and
Lutz Schröder and
Sergey Goncharov A generic complete dynamic logic for
reasoning about purity and effects . . . 363--384
Fernando Orejas and
Hartmut Ehrig and
Ulrike Prange Reasoning with graph constraints . . . . 385--422
Jan Smans and
Bart Jacobs and
Frank Piessens and
Wolfram Schulte Automatic verification of Java programs
with dynamic frames . . . . . . . . . . 423--457
Wil M. P. van der Aalst and
Marlon Dumas and
Florian Gottschalk and
Arthur H. M. ter Hofstede and
Marcello La Rosa and
Jan Mendling Preserving correctness during business
process model configuration . . . . . . 459--482
Matthew Collinson and
David Pym Erratum to: Algebra and logic for access
control . . . . . . . . . . . . . . . . 483--484
Anonymous Robin Milner: 13 January 1934---20 March
2010 . . . . . . . . . . . . . . . . . . 485--487
Adolfo Duran and
Ana Cavalcanti and
Augusto Sampaio An algebraic approach to the design of
compilers for object-oriented languages 489--535
Wim H. Hesselink Solutions of equations in languages . . 537--545
Ivana Filipovi\'c and
Peter O'Hearn and
Noah Torp-Smith and
Hongseok Yang Blaming the client: on data refinement
in the presence of pointers . . . . . . 547--583
Mohamed Saleh and
Mourad Debbabi A game-theoretic framework for
specification and verification of
cryptographic protocols . . . . . . . . 585--609
Jaime A. Bohórquez V. An elementary and unified approach to
program correctness . . . . . . . . . . 611--627
Ralph-Johan Back Structured derivations: a unified proof
style for teaching mathematics . . . . . 629--661
David Harel Amir Pnueli: A Gentle Giant: Lord of the
$ \phi $'s and the $ \psi $'s . . . . . 663--665
Guy-Vincent Jourdan and
Hasan Ural and
Hüsnü Yenigün and
Ji Chao Zhang Lower bounds on lengths of checking
sequences . . . . . . . . . . . . . . . 667--679
Frédéric Lang and
Gwen Salaün and
Rémi Hérilier and
Jeff Kramer and
Jeff Magee Translating FSP into LOTOS and networks
of automata . . . . . . . . . . . . . . 681--711
Thomas Wahl and
Vijay D'Silva A lazy approach to symmetry reduction 713--733
Richard Bornat and
Hasan Amjad Inter-process buffers in separation
logic with rely-guarantee . . . . . . . 735--772
Egon Börger Editorial . . . . . . . . . . . . . . . 1--2
Jacques Julliand and
Pierre-Alain Masson and
Régis Tissot and
Pierre-Christophe Bué Generating tests from B specifications
and dynamic selection criteria . . . . . 3--19
Alessandra Cavarra A data-flow approach to test multi-agent
ASMs . . . . . . . . . . . . . . . . . . 21--41
John Derrick and
Siobhán North and
Anthony J. H. Simons Z2SAL: a translation-based model checker
for Z . . . . . . . . . . . . . . . . . 43--71
Stephen Wright and
Kerstin Eder Using Event-B to construct instruction
set architectures . . . . . . . . . . . 73--89
Simon Bäumler and
Gerhard Schellhorn and
Bogdan Tofan and
Wolfgang Reif Proving linearizability with temporal
logic . . . . . . . . . . . . . . . . . 91--112
Richard Banach Retrenchment for Event-B: UseCase-wise
development and Rodin integration . . . 113--131
Stefan Hallerstede On the purpose of Event-B proof
obligations . . . . . . . . . . . . . . 133--150
Zhiming Liu and
Jim Woodcock Editorial . . . . . . . . . . . . . . . 151--151
Andrew Butterfield A denotational semantics for Handel-C 153--170
Bican Xia and
Lu Yang and
Naijun Zhan and
Zhihai Zhang Symbolic decision procedure for
termination of linear programs . . . . . 171--190
Anne E. Haxthausen and
Jan Peleska and
Sebastian Kinder A formal approach for the construction
and verification of railway control
systems . . . . . . . . . . . . . . . . 191--219
Peter D. Mosses VDM semantics of programming languages:
combinators and monads . . . . . . . . . 221--238
Axel van Lamsweerde The Humble Humorous Researcher: A
Tribute to Michel Sintzoff . . . . . . . 239--242
Geoffrey M. Brown and
Lee Pike Automated verification and refinement
for physical-layer protocols . . . . . . 243--266
I. T. Kassios The dynamic frames theory . . . . . . . 267--288
Cliff B. Jones and
Ken G. Pierce Elucidating concurrent algorithms via
layers of abstraction and reification 289--306
Daniel Sinnig and
Ferhat Khendek and
Patrice Chalin Partial order semantics for use case and
task models . . . . . . . . . . . . . . 307--332
W. M. P. van der Aalst and
K. M. van Hee and
A. H. M. ter Hofstede and
N. Sidorova and
H. M. W. Verbeek and
M. Voorhoeve and
M. T. Wynn Soundness of workflow nets:
classification, decidability, and
analysis . . . . . . . . . . . . . . . . 333--363
Gerard J. Holzmann and
Mihai Florian Model checking with bounded context
switching . . . . . . . . . . . . . . . 365--389
Eric C. R. Hehner A probability perspective . . . . . . . 391--419
Alan Stewart A programming model for BSP with
partitioned synchronisation . . . . . . 421--432
José Luiz Fiadeiro and
Antónia Lopes and
Laura Bocchi An abstract model of service discovery
and binding . . . . . . . . . . . . . . 433--463
Ana Cavalcanti and
Phil Clayton and
Colin O'Halloran From control law diagrams to Ada via
Circus . . . . . . . . . . . . . . . . . 465--512
Linmin Yang and
Zhe Dang and
Thomas R. Fischer Information gain of black-box testing 513--539
Han Gao and
Flemming Nielson and
Hanne Riis Nielson CaPiTo: protocol stacks for services . . 541--565
J. A. Bergstra and
C. A. Middelburg Thread algebra for poly-threading . . . 567--583
Daniel Kroening and
Tiziana Margaria and
Jim Woodcock Editorial . . . . . . . . . . . . . . . 585--588
Sven Jörges and
Tiziana Margaria and
Bernhard Steffen Assuring property conformance of code
generators via model checking . . . . . 589--606
Murali Sitaraman and
Bruce Adcock and
Jeremy Avigad and
Derek Bronish and
Paolo Bucci and
David Frazier and
Harvey M. Friedman and
Heather Harton and
Wayne Heym and
Jason Kirschenbaum and
Joan Krone and
Hampton Smith and
Bruce W. Weide Building a push-button RESOLVE verifier:
Progress and challenges . . . . . . . . 607--626
Chiara Braghin and
Natasha Sharygina and
Katerina Barone-Adesi A model checking-based approach for
security policy verification of mobile
systems . . . . . . . . . . . . . . . . 627--648
K. Mani Chandy and
Brian Go and
Sayan Mitra and
Concetta Pilotto and
Jerome White Verification of distributed systems with
local---global predicates . . . . . . . 649--679
Ana Cavalcanti and
Dennis Dams and
Marie-Claude Gaudel Editorial . . . . . . . . . . . . . . . 681--681
Michael Leuschel and
Jérôme Falampin and
Fabian Fritz and
Daniel Plagge Automated property verification for
large scale B models with ProB . . . . . 683--709
A. K. McIver and
C. C. Morgan Compositional refinement in agent-based
security protocols . . . . . . . . . . . 711--737
Mark Reynolds A tableau-based decision procedure for
CTL* . . . . . . . . . . . . . . . . . . 739--779
Chao Wang and
Sudipta Kundu and
Rhishikesh Limaye and
Malay Ganai and
Aarti Gupta Symbolic predictive analysis for
concurrent programs . . . . . . . . . . 781--805
Eerke Boiten and
John Derrick and
Jin Song Dong and
Steve Reeves Editorial . . . . . . . . . . . . . . . 1--1
Carroll Morgan Compositional noninterference from first
principles . . . . . . . . . . . . . . . 3--26
Wim H. Hesselink and
Muhammad Ikram Lali Formalizing a hierarchical file system 27--44
J. W. Sanders and
Graeme Smith Emergence and refinement . . . . . . . . 45--65
Viorel Preoteasa and
Ralph-Johan Back Invariant diagrams with data refinement 67--95
Stefan Hallerstede and
Michael Leuschel Experiments in program verification
using Event-B . . . . . . . . . . . . . 97--125
Frank Zeyda and
Marcel Oliveira and
Ana Cavalcanti Mechanised support for sound refinement
tactics . . . . . . . . . . . . . . . . 127--160
J. L. Fiadeiro and
S. Gnesi and
T. Maibaum Editorial . . . . . . . . . . . . . . . 161--162
Antonio Filieri and
Carlo Ghezzi and
Giordano Tamburrelli A formal approach to adaptive software:
continuous assurance of non-functional
requirements . . . . . . . . . . . . . . 163--186
Natallia Kokash and
Christian Krause and
Erik de Vink Reo + mCRL2: A framework for
model-checking dataflow in service
compositions . . . . . . . . . . . . . . 187--216
José Bernardo Barros and
Daniela da Cruz and
Pedro Rangel Henriques and
Jorge Sousa Pinto Assertion-based slicing and slice graphs 217--248
Peter A. Lindsay and
Nisansala Yatapanage and
Kirsten Winter Cut Set Analysis using Behavior Trees
and model checking . . . . . . . . . . . 249--266
M. Massink and
D. Latella and
A. Bracciali and
M. D. Harrison and
J. Hillston Scalable context-dependent analysis of
emergency egress models . . . . . . . . 267--302
Jim Woodcock Editorial . . . . . . . . . . . . . . . 303--303
Cliff B. Jones John McCarthy (1927---2011) . . . . . . 305--306
Michele Risi and
Giuseppe Scanniello and
Genoveffa Tortora Using fold-in and fold-out in the
architecture recovery of software
systems . . . . . . . . . . . . . . . . 307--330
Wilkerson L. Andrade and
Patrícia D. L. Machado Testing interruptions in reactive
systems . . . . . . . . . . . . . . . . 331--353
Moonzoo Kim and
Yunho Kim and
Yunja Choi Concolic testing of the multi-sector
read operation for flash storage
platform software . . . . . . . . . . . 355--374
Jan Tobias Mühlberg and
Gerald Lüttgen Verifying compiled file system code . . 375--391
John Derrick and
Graeme Smith Temporal-logic property preservation
under Z refinement . . . . . . . . . . . 393--416
P. Höfner Preface . . . . . . . . . . . . . . . . 417--422
Tony Hoare and
Stephan van Staden In praise of algebra . . . . . . . . . . 423--431
José N. Oliveira Towards a linear algebra of programming 433--458
Peter Höfner and
Bernhard Möller Dijkstra, Floyd and Warshall meet Kleene 459--476
Mani Swaminathan and
Joost-Pieter Katoen and
Ernst-Rüdiger Olderog Layered reasoning for randomized
distributed algorithms . . . . . . . . . 477--496
J. Markovski and
P. R. D'Argenio and
J. C. M. Baeten and
E. P. de Vink Reconciling real and stochastic time:
the need for probabilistic refinement 497--518
K. Rustan M. Leino and
Kuat Yessenov Stepwise refinement of heap-manipulating
code in Chalice . . . . . . . . . . . . 519--535
Bengt Jonsson Using refinement calculus techniques to
prove linearizability . . . . . . . . . 537--554
Michael Butler External and internal choice with event
groups in Event-B . . . . . . . . . . . 555--567
Alberto Pettorossi and
Maurizio Proietti and
Valerio Senni Constraint-based correctness proofs for
logic program transformations . . . . . 569--594
Patricia Bouyer and
Nicolas Markey and
Joël Ouaknine and
Philippe Schnoebelen and
James Worrell On termination and invariance for faulty
channel machines . . . . . . . . . . . . 595--607
Richard S. Bird On building cyclic and shared structures
in Haskell . . . . . . . . . . . . . . . 609--621
Kento Emoto and
Sebastian Fischer and
Zhenjiang Hu Filter-embedding semiring fusion for
programming with MapReduce . . . . . . . 623--645
Glynn Winskel Deterministic concurrent strategies . . 647--660
Marta Kwiatkowska and
Gethin Norman and
David Parker Probabilistic verification of Herman's
self-stabilisation algorithm . . . . . . 661--670
Stefan Kiefer and
Andrzej S. Murawski and
Joël Ouaknine and
Björn Wachter and
James Worrell Three tokens in Herman's algorithm . . . 671--678
Robert M. Hierons and
Manuel Núñez Using schedulers to test probabilistic
distributed systems . . . . . . . . . . 679--699
Yuxin Deng and
Alwen Tiu Characterisations of testing preorders
for a finite probabilistic $ \pi
$-calculus . . . . . . . . . . . . . . . 701--726
Sonja Georgievska and
Suzana Andova Probabilistic may/must testing:
retaining probabilities by restricted
schedulers . . . . . . . . . . . . . . . 727--748
Matthew Hennessy Exploring probabilistic bisimulations,
part I . . . . . . . . . . . . . . . . . 749--768
Ron van der Meyden Architectural refinement and notions of
intransitive noninterference . . . . . . 769--792
Jayadev Misra A secure voting scheme based on rational
self-interest . . . . . . . . . . . . . 793--805
Anonymous Preface . . . . . . . . . . . . . . . . 1--2
A. W. Roscoe and
Jian Huang Checking noninterference in Timed CSP 3--35
Ana Cavalcanti and
Andy Wellings and
Jim Woodcock The Safety-Critical Java memory model
formalised . . . . . . . . . . . . . . . 37--57
Thai Son Hoang Security invariants in discrete
transition systems . . . . . . . . . . . 59--87
Yifeng Chen Semantic inheritance in unifying
theories of programming . . . . . . . . 89--106
Bill Stoddart and
Frank Zeyda A unification of probabilistic choice
within a design-based model of
reversible computation . . . . . . . . . 107--131
Marcel Oliveira and
Ana Cavalcanti and
Jim Woodcock Unifying theories in ProofPower-Z . . . 133--158
Ragnhild Kobro Runde and
Atle Refsdal and
Ketil Stòlen Relating computer systems to sequence
diagrams: the impact of
underspecification and inherent
nondeterminism . . . . . . . . . . . . . 159--187
Kenneth Johnson and
John V. Tucker The data type of spatial objects . . . . 189--218
Toby Murray On the limits of refinement-testing for
model-checking CSP . . . . . . . . . . . 219--256
Troels C. Damgaard and
Arne J. Glenstrup and
Lars Birkedal and
Robin Milner An inductive characterization of
matching in binding bigraphs . . . . . . 257--288
Rodolfo Gómez Model-checking timed automata with
deadlines with Uppaal . . . . . . . . . 289--318
K. Subramani and
Matthew Williamson and
Xiaofeng Gu Improved algorithms for optimal length
resolution refutation in difference
constraint systems . . . . . . . . . . . 319--341
Jonathan P. Bowen and
Michael Butler and
Steve Reeves and
Mike Hinchey Editorial . . . . . . . . . . . . . . . 343--343
Rob Arthan and
Ursula Martin and
Paulo Oliva A Hoare logic for linear systems . . . . 345--363
Juan I. Perna and
Chris George Model checking RAISE applicative
specifications . . . . . . . . . . . . . 365--388
Domagoj Babi\'c and
Byron Cook and
Alan J. Hu and
Zvonimir Rakamari\'c Proving termination of nonlinear command
sequences . . . . . . . . . . . . . . . 389--403
Bernhard Beckert and
Vladimir Klebanov A Dynamic Logic for deductive
verification of multi-threaded programs 405--437
Richard Banach and
Czeslaw Jeske and
Anthony Hall and
Susan Stepney Atomicity failure and the retrenchment
atomicity pattern . . . . . . . . . . . 439--464
Yongjian Li and
Jun Pang An inductive approach to strand spaces 465--501
Vashti Galpin and
Luca Bortolussi and
Jane Hillston HYPE: Hybrid modelling by composition of
flows . . . . . . . . . . . . . . . . . 503--541
Tomás Poch and
Ondrej Serý and
Frantisek Plásil and
Jan Kofron Threaded behavior protocols . . . . . . 543--572
Richard Banach and
Marco Bozzano The mechanical generation of fault trees
for reactive systems via retrenchment I:
combinational circuits . . . . . . . . . 573--607
Richard Banach and
Marco Bozzano The mechanical generation of fault trees
for reactive systems via retrenchment
II: clocked and feedback circuits . . . 609--657
Rik Eshuis Statechartable Petri nets . . . . . . . 659--681
Achim D. Brucker and
Burkhart Wolff On theorem prover-based testing . . . . 683--721
Mathias John and
Hans-Jörg Schulz and
Heidrun Schumann and
Adelinde M. Uhrmacher and
Andrea Unger Constructing and visualizing chemical
reaction networks from pi-calculus
models . . . . . . . . . . . . . . . . . 723--742
Pablo Rabanal and
Ismael Rodríguez and
Fernando Rubio Testing restorable systems: formal
definition and heuristic solution based
on river formation dynamics . . . . . . 743--768
Simon Doherty and
Lindsay Groves and
Victor Luchangco and
Mark Moir Towards formally specifying and
verifying transactional memory . . . . . 769--799
Massimo Merro and
Eleonora Sibilio A calculus of trustworthy ad hoc
networks . . . . . . . . . . . . . . . . 801--832
Alan Stewart and
Joaquim Gabarro and
Anthony Keenan Reasoning about orchestrations of web
services using partial correctness . . . 833--846
Xiang Fu and
Michael C. Powell and
Michael Bantegui and
Chung-Chih Li Simple linear string constraints . . . . 847--891
Richard Bornat and
Hasan Amjad Explanation of two non-blocking
shared-variable communication algorithms 893--931
Paolo Bientinesi and
John A. Gunnels and
Margaret E. Myers and
Enrique S. Quintana-Ortí and
Tyler Rhodes and
Robert A. van de Geijn and
Field G. Van Zee Deriving dense linear algebra libraries 933--945
Wim H. Hesselink and
Mark IJbema Starvation-free mutual exclusion with
semaphores . . . . . . . . . . . . . . . 947--969
Sa'ed Abed and
Otmane Ait Mohamed and
Ghiath Al Sammane Automatic verification of reduction
techniques in Higher Order Logic . . . . 971--991
Hanne Gottliebsen and
Ruth Hardy and
Olga Lightfoot and
Ursula Martin Applications of real number theorem
proving in PVS . . . . . . . . . . . . . 993--1016
Eerke Boiten and
Steve Schneider Editorial . . . . . . . . . . . . . . . 1--2
Giampaolo Bella Inductive study of confidentiality: for
everyone . . . . . . . . . . . . . . . . 3--36
James Heather and
Steve Schneider and
Vanessa Teague Cryptographic protocols with everyday
objects . . . . . . . . . . . . . . . . 37--62
Murat Moran and
James Heather and
Steve Schneider Verifying anonymity in voting systems
using CSP . . . . . . . . . . . . . . . 63--98
Matteo Avalle and
Alfredo Pironti and
Riccardo Sisto Formal verification of security protocol
implementations: a survey . . . . . . . 99--123
Alfredo Pironti and
Riccardo Sisto Safe abstractions of data encodings in
formal security protocol models . . . . 125--167
T. S. Hoang and
A. K. McIver and
L. Meinicke and
C. C. Morgan and
A. Sloane and
E. Susatyo Abstractions of non-interference
security: probabilistic versus
possibilistic . . . . . . . . . . . . . 169--194
Eerke A. Boiten and
John Derrick and
Steve Reeves Editorial . . . . . . . . . . . . . . . 195--195
Luigia Petre and
Elena Troubitsyna and
Marina Waldén Kaisa Sere: In Memoriam . . . . . . . . 197--201
Maria Teresa Llano and
Andrew Ireland and
Alison Pease Discovery of invariants through
automated theory formation . . . . . . . 203--249
Steve Schneider and
Helen Treharne and
Heike Wehrheim The behavioural semantics of Event-B
refinement . . . . . . . . . . . . . . . 251--280
Pontus Boström and
Fredrik Degerlund and
Kaisa Sere and
Marina Waldén Derivation of concurrent programs by
stepwise scheduling of Event-B models 281--303
Eerke A. Boiten Introducing extra operations in
refinement . . . . . . . . . . . . . . . 305--317
Richard Banach and
Huibiao Zhu and
Wen Su and
Runlei Huang Continuous KAOS, ASM, and formal control
system design across the
continuous/discrete modeling interface:
a simple train stopping application . . 319--366
Alvaro Miyazawa and
Ana Cavalcanti Refinement-based verification of
implementations of Stateflow charts . . 367--405
John Derrick and
Eerke Boiten Relational concurrent refinement part
III: traces, partial relations and
automata . . . . . . . . . . . . . . . . 407--432
C. B. Jones Editorial . . . . . . . . . . . . . . . 433--433
Stephen Brookes and
Peter W. O'Hearn and
Uday Reddy The Essence of Reynolds . . . . . . . . 435--439
Sidney Nogueira and
Augusto Sampaio and
Alexandre Mota Test generation from state based use
case models . . . . . . . . . . . . . . 441--490
Robert J. Colvin An operational semantics for
object-oriented concepts based on the
class hierarchy . . . . . . . . . . . . 491--535
Muffy Calder and
Michele Sevegnani Modelling IEEE 802.11 CSMA/CA RTS/CTS
with stochastic bigraphs with sharing 537--561
Brijesh Dongol and
Ian J. Hayes and
Peter J. Robinson Reasoning about goal-directed real-time
teleo-reactive programs . . . . . . . . 563--589
Manoj G. Dixit and
S. Ramesh and
Pallab Dasgupta Time-budgeting: a component based
development methodology for real-time
embedded systems . . . . . . . . . . . . 591--621
Xi Liu and
Shaofa Yang and
J. W. Sanders Compensation by design . . . . . . . . . 623--676
Savas Konur and
Michael Fisher and
Simon Dobson and
Stephen Knox Formal verification of a pervasive
messaging system . . . . . . . . . . . . 677--694
Prahladavaradan Sampath An elementary theory of product-line
variations . . . . . . . . . . . . . . . 695--727
Jin Song Dong and
Yang Liu and
Jun Sun and
Xian Zhang Towards verification of computation
orchestration . . . . . . . . . . . . . 729--759
Ferruccio Damiani and
Johan Dovland and
Einar Broch Johnsen and
Ina Schaefer Verifying traits: an incremental proof
system for fine-grained reuse . . . . . 761--793
Ana Cavalcanti and
Steve King and
Colin O'Halloran and
Jim Woodcock Test-data generation for control
coverage by proof . . . . . . . . . . . 795--823
Krishnendu Chatterjee and
Vishwanath Raman Assume-guarantee synthesis for digital
contract signing . . . . . . . . . . . . 825--859
Cliff B. Jones Editorial . . . . . . . . . . . . . . . 861--861
Andrzej Tarlecki W\ladys\law Marek Turski (1938---2013) 863--864
Luís Cruz-Filipe and
Ivan Lanese and
Francisco Martins and
António Ravara and
Vasco Thudichum Vasconcelos The stream-based service-centred
calculus: a foundation for
service-oriented programming . . . . . . 865--918
Marc Frappier and
Frédéric Gervais and
Régine Laleau and
Jérémy Milhau Refinement patterns for ASTDs . . . . . 919--941
Yoriyuki Yamagata and
Weiqiang Kong and
Akira Fukuda and
Nguyen Van Tang and
Hitoshi Ohsaki and
Kenji Taguchi A formal semantics of extended
hierarchical state transition matrices
using CSP# . . . . . . . . . . . . . . . 943--962
Michael J. Banks and
Jeremy L. Jacob On integrating confidentiality and
functionality in a formal method . . . . 963--992
Martin Ward and
Hussein Zedan Provably correct derivation of
algorithms using FermaT . . . . . . . . 993--1031
Rimvydas Ruk\vs\.enas and
Paul Curzon and
Ann Blandford and
Jonathan Back Combining human error verification and
timing analysis: a case study on an
infusion pump . . . . . . . . . . . . . 1033--1076
Elvinia Riccobene and
Patrizia Scandurra A formal framework for service modeling
and prototyping . . . . . . . . . . . . 1077--1113
Alessandro Rossini and
Juan de Lara and
Esther Guerra and
Adrian Rutle and
Uwe Wolter A formalisation of deep metamodelling 1115--1152
Canan Güniçen and
Kemal \.Inan and
Uraz Cengiz Türker and
Hüsnü Yenigün The relation between preset
distinguishing sequences and
synchronizing sequences . . . . . . . . 1153--1167
Li Su and
Rodolfo Gomez and
Howard Bowman Analysing neurobiological models using
communicating automata . . . . . . . . . 1169--1204
Matthias Daum and
Nelson Billing and
Gerwin Klein Concerned with the unprivileged: user
programs in kernel refinement . . . . . 1205--1229
Nicolas Wu and
Andrew Simpson Formal relational database design: an
exercise in extending the formal
template language . . . . . . . . . . . 1231--1269
Borzoo Bonakdarpour and
Sandeep S. Kulkarni Synthesizing bounded-time $2$-phase
fault recovery . . . . . . . . . . . . . 1--31
Mohand Yazid and
Djamil A\"\issani and
Louiza Bouallouche-Medjkoune and
Nassim Amrouche and
Kamel Bakli Modeling and enhancement of the IEEE
802.11 RTS/CTS scheme in an error-prone
channel . . . . . . . . . . . . . . . . 33--52
Anton Tarasyuk and
Elena Troubitsyna and
Linas Laibinis Integrating stochastic reasoning into
Event-B development . . . . . . . . . . 53--77
Maissa Elleuch and
Osman Hasan and
Sofi\`ene Tahar and
Mohamed Abid Formal probabilistic analysis of
detection properties in wireless sensor
networks . . . . . . . . . . . . . . . . 79--102
Qian Ma and
Zhenhua Duan and
Nan Zhang and
Xiaobing Wang Verification of distributed systems with
the axiomatic system of MSVL . . . . . . 103--131
H. Zhu and
Jifeng He and
Shengchao Qin and
Phillip J. Brooke Denotational semantics and its algebraic
derivation for an event-driven
system-level language . . . . . . . . . 133--166
Shu Cheng and
Jim Woodcock and
Deepak D'Souza Using formal reasoning on a model of
tasks for FreeRTOS . . . . . . . . . . . 167--192
Kevin Lano and
T. Clark and
S. Kolahdouz-Rahimi A framework for model transformation
verification . . . . . . . . . . . . . . 193--235
Cliff B. Jones In memoriam: Professor Heinz Zemanek
(1920--2014) . . . . . . . . . . . . . . 237--237
P. Zave A practical comparison of Alloy and Spin 239--253
Yongjian Li and
Jun Pang Formalizing provable anonymity in
Isabelle/HOL . . . . . . . . . . . . . . 255--282
Hugo Daniel Macedo and
José Nuno Oliveira A linear algebra approach to OLAP . . . 283--307
Gholamreza Sotudeh and
Ali Movaghar Abstraction and approximation in fuzzy
temporal logics and models . . . . . . . 309--334
Amel Mammar and
Marc Frappier Proof-based verification approaches for
dynamic properties: application to the
information system domain . . . . . . . 335--374
Alexandre Madeira and
Manuel A. Martins and
Luís S. Barbosa and
Rolf Hennicker Refinement in hybridised institutions 375--395
Fu Song and
Tayssir Touili Model checking dynamic pushdown networks 397--421
Frank Zeyda and
Ana Cavalcanti Laws of mission-based programming . . . 423--472
George Eleftherakis and
Michael Butler and
Mike Hinchey Editorial . . . . . . . . . . . . . . . 473--473
Cliff B. Jones and
Ian J. Hayes and
Robert J. Colvin Balancing expressiveness in formal
approaches to concurrency . . . . . . . 475--497
Asieh Salehi Fathabadi and
Michael Butler and
Abdolbaghi Rezazadeh Language and tool support for event
refinement structures in Event-B . . . . 499--523
Gabriel Ciobanu and
Maciej Koutny and
Jason Steggles Strategy based semantics for mobility
with time and access permissions . . . . 525--549
Crystal Chang Din and
Olaf Owe Compositional reasoning about active
objects with shared futures . . . . . . 551--572
Florent Kirchner and
Nikolai Kosmatov and
Virgile Prevosto and
Julien Signoles and
Boris Yakobowski Frama-C: A software analysis perspective 573--609
Michael Butler and
Einar Broch Johnsen and
Luigia Petre Editorial . . . . . . . . . . . . . . . 611--612
Cosimo Laneve and
Luca Padovani An algebraic theory for web service
contracts . . . . . . . . . . . . . . . 613--640
Safouan Taha and
Jacques Julliand and
Frédéric Dadeau and
Kalou Cabrera Castillos and
Bilal Kanso A compositional automata-based semantics
and preserving transformation rules for
testing property patterns . . . . . . . 641--664
Elvira Albert and
Jesús Correas and
Germán Puebla and
Guillermo Román-Díez Quantified abstract configurations of
distributed systems . . . . . . . . . . 665--699
Dorel Lucanu and
Vlad Rusu Program equivalence by circular
reasoning . . . . . . . . . . . . . . . 701--726
Ernst-Rüdiger Olderog and
Mani Swaminathan Structural transformations for
data-enriched real-time systems . . . . 727--750
Jim Woodcock and
Cliff Jones Editorial . . . . . . . . . . . . . . . 751--752
Artem Polyvyanyy and
Marcello La Rosa and
Chun Ouyang and
Arthur H. M. ter Hofstede Untanglings: a novel approach to
analyzing concurrent systems . . . . . . 753--788
Maryam Dabaghchian and
Mohammad Abdollahi Azgomi Model checking the observational
determinism security property using
PROMELA and SPIN . . . . . . . . . . . . 789--804
Rachid Rebiha and
Arnaldo Vieira Moura and
Nadir Matringe Generating invariants for non-linear
loops by linear algebraic methods . . . 805--829
Pablo F. Castro and
Nazareno Aguirre and
Carlos L. Pombo and
T. S. E. Maibaum Categorical foundations for structured
specifications in $ \mathsf {Z} $ . . . 831--865
Domenico Rosaci Finding semantic associations in
hierarchically structured groups of Web
data . . . . . . . . . . . . . . . . . . 867--884
Douglas Pereira Pasqualin and
Juliana Kaizer Vizzotto and
Eduardo Kessler Piveta Typed context awareness Ambient Calculus
for pervasive applications . . . . . . . 885--916
Omar Al-Bataineh and
Mark Reynolds and
Tim French Accelerating worst case execution time
analysis of timed automata models with
cyclic behaviour . . . . . . . . . . . . 917--949
Messaouda Bouneb and
Djamel Eddine Saidouni and
Jean Michel Ilie A reduced maximality labeled transition
system generation for recursive Petri
nets . . . . . . . . . . . . . . . . . . 951--973
A. Mota and
A. Farias and
J. Woodcock and
P. G. Larsen Model checking CML: tool development and
industrial applications . . . . . . . . 975--1001
Florentin Ipate and
Dimitris Dranidis A unified integration and component
testing approach from deterministic
stream X-machine specifications . . . . 1--20
Narges Khakpour and
Farhad Arbab and
Eric Rutten Synthesizing structural and behavioral
control for reconfigurations in
component-based systems . . . . . . . . 21--43
Jirí Barnat and
Petr Bauch and
Nikola Benes and
Lubos Brim and
Jan Beran and
Tomás Kratochvíla Analysing sanity of requirements for
avionics systems . . . . . . . . . . . . 45--63
Sofia Costa Paiva and
Adenilso Simao Generation of complete test suites from
mealy input/output transition systems 65--78
Jonatan Wiik and
Pontus Boström Contract-based verification of
MATLAB-style matrix programs . . . . . . 79--107
Luis María Ferrer Fioriti and
Vahid Hashemi and
Holger Hermanns and
Andrea Turrini Deciding probabilistic automata weak
bisimulation: theory and practice . . . 109--143
Dimitris Vekris and
Frédéric Lang and
Catalin Dima and
Radu Mateescu Verification of EB$^3$ specifications
using CADP . . . . . . . . . . . . . . . 145--178
Dimitris Vekris and
Frédéric Lang and
Catalin Dima and
Radu Mateescu Verification of $ E B^3 $ specifications
using CADP . . . . . . . . . . . . . . . 145--178
Michael Butler Editorial . . . . . . . . . . . . . . . 179--180
Dimitra Giannakopoulou and
Gwen Salaün and
Michael Butler Editorial . . . . . . . . . . . . . . . 179--180
Sarmen Keshishzadeh and
Arjan J. Mooij Formalizing and testing the consistency
of DSL transformations . . . . . . . . . 181--206
Paul Attie and
Eduard Baranov and
Simon Bliudze and
Mohamad Jaber and
Joseph Sifakis A general framework for architecture
composability . . . . . . . . . . . . . 207--231
Sofia Cassel and
Falk Howar and
Bengt Jonsson and
Bernhard Steffen Active learning for extended finite
state machines . . . . . . . . . . . . . 233--263
Alasdair Armstrong and
Victor B. F. Gomes and
Georg Struth Building program construction and
verification tools from algebraic
principles . . . . . . . . . . . . . . . 265--293
Ivaylo Dobrikov and
Michael Leuschel Optimising the ProB model checker for B
using partial order reduction . . . . . 295--323
Wim H. Hesselink Correctness and concurrent complexity of
the Black--White Bakery Algorithm . . . 325--341
Stephan Merz and
Jun Pang and
Jin Song Dong Editorial . . . . . . . . . . . . . . . 343--344
Stephan Merz and
Jun Pang and
Jin Song Dong Editorial . . . . . . . . . . . . . . . 343--344
Vince Molnár and
András Vörös and
Dániel Darvas and
Tamás Bartha and
István Majzik Component-wise incremental LTL model
checking . . . . . . . . . . . . . . . . 345--379
Alexandre Boulgakov and
Thomas Gibson-Robinson and
A. W. Roscoe Computing maximal weak and other
bisimulations . . . . . . . . . . . . . 381--407
Mounira Kezadri Hamiaz and
Marc Pantel and
Xavier Thirioux and
Benoit Combemale Correct-by-construction model driven
engineering composition operators . . . 409--440
Hamid Bagheri and
Kevin Sullivan Model-driven synthesis of formally
precise, stylized software architectures 441--467
Stefan Ciobâca and
Dorel Lucanu and
Vlad Rusu and
Grigore Rosu A language-independent proof system for
full program equivalence . . . . . . . . 469--497
Sergio Feo-Arenis and
Bernd Westphal and
Daniel Dietsch and
Marco Muñiz and
Siyar Andisha and
Andreas Podelski Ready for testing: ensuring conformance
to industrial standards through formal
verification . . . . . . . . . . . . . . 499--527
Marco Carbone and
Thomas Hildebrandt and
Joachim Parrow and
Matthias Weidlich Editorial . . . . . . . . . . . . . . . 529--530
Cinzia Di Giusto and
Jorge A. Pérez Event-based run-time adaptation in
communication-centric systems . . . . . 531--566
Paolo Arcaini and
Roxana-Maria Holom and
Elvinia Riccobene ASM-based formal design of an adaptivity
component for a Cloud system . . . . . . 567--595
Artem Polyvyanyy and
Abel Armas-Cervantes and
Marlon Dumas and
Luciano García-Bañuelos On the expressive power of behavioral
profiles . . . . . . . . . . . . . . . . 597--613
Marco Montali and
Andrey Rivkin Model checking Petri nets with names
using data-centric dynamic systems . . . 615--641
Silvia Ghilezan and
Svetlana Jaksi\'c and
Jovanka Pantovi\'c and
Jorge A. Pérez and
Hugo Torres Vieira Dynamic role authorization in multiparty
conversations . . . . . . . . . . . . . 643--667
Ilaria Castellani and
Mariangiola Dezani-Ciancaglini and
Jorge A. Pérez Self-adaptation and secure information
flow in multiparty communications . . . 669--696
Franco Barbanera and
Mariangiola Dezani-Ciancaglini and
Ugo de'Liguoro Reversible client/server interactions 697--722
Stephan Merz and
Jun Pang and
Jin Song Dong Editorial . . . . . . . . . . . . . . . 723--724
Gustavo Carvalho and
Ana Cavalcanti and
Augusto Sampaio Modelling timed reactive systems from
natural-language requirements . . . . . 725--765
Fatma Jebali and
Frédéric Lang and
Radu Mateescu Formal modelling and verification of
GALS systems using GRL and CADP . . . . 767--804
Étienne André and
Mohamed Mahdi Benmoussa and
Christine Choppy Formalising concurrent UML state
machines using coloured Petri nets . . . 805--845
Florent Chevrou and
Aurélie Hurault and
Philippe Quéinnec On the diversity of asynchronous
communication . . . . . . . . . . . . . 847--879
Umair Siddique and
Sofi\`ene Tahar On the formal analysis of Gaussian
optical systems in HOL . . . . . . . . . 881--907
Thai Son Hoang and
Steve Schneider and
Helen Treharne and
David M. Williams Foundations for using linear temporal
logic in Event-B refinement . . . . . . 909--935
M. V. M. Oliveira and
P. Antonino and
R. Ramos and
A. Sampaio and
A. Mota and
A. W. Roscoe Rigorous development of component-based
systems using component metadata and
patterns . . . . . . . . . . . . . . . . 937--1004
Jesús Aransay and
Jose Divasón Formalisation of the computation of the
echelon form of a matrix in Isabelle/HOL 1005--1026
Ryan Kirwan and
Alice Miller and
Bernd Porr Model checking learning agent systems
using Promela with embedded C code and
abstraction . . . . . . . . . . . . . . 1027--1056
Ian J. Hayes Generalised rely-guarantee concurrency:
an algebraic foundation . . . . . . . . 1057--1078
Maurizio Proietti and
Hirohisa Seki and
Jim Woodcock Editorial . . . . . . . . . . . . . . . 1--2
Roberto Giacobazzi and
Isabella Mastroeni and
Mila Dalla Preda Maximal incompleteness as obfuscation
potency . . . . . . . . . . . . . . . . 3--31
Aziem Chawdhary and
Ranjeet Singh and
Andy King Partial evaluation of string
obfuscations for Java malware detection 33--55
Henning Christiansen and
Maja H. Kirkeby On proving confluence modulo equivalence
for Constraint Handling Rules . . . . . 57--95
Emilio Jesús Gallego Arias and
James Lipton and
Julio Mariño Constraint logic programming with a
relational machine . . . . . . . . . . . 97--124
Vincent Nys and
Danny De Schreye Abstract conjunctive partial deduction
for the analysis and compilation of
coroutines . . . . . . . . . . . . . . . 125--153
W\lodzimierz Drabent Proving completeness of logic programs
with the cut . . . . . . . . . . . . . . 155--172
Anonymous [Obituary:] Amílcar Sernadas . . . . . . 173--173
Dines Bjòrner Manifest domains: analysis and
description . . . . . . . . . . . . . . 175--225
Qin Li and
Graeme Smith Refining autonomous agents with
declarative beliefs and desires . . . . 227--249
Anirban Bhattacharyya and
Andrey Mokhov and
Ken Pierce An empirical comparison of formalisms
for modelling and analysis of dynamic
reconfiguration of dependable systems 251--307
Adrián Riesco and
Kazuhiro Ogata and
Kokichi Futatsugi A Maude environment for CafeOBJ . . . . 309--334
Wen-ling Huang and
Jan Peleska Complete model-based equivalence class
testing for nondeterministic systems . . 335--364
Kunal Banerjee and
Dipankar Sarkar and
Chittaranjan Mandal Deriving bisimulation relations from
path based equivalence checkers . . . . 365--379
Moreno Falaschi and
Augusto Sampaio Editorial . . . . . . . . . . . . . . . 381--382
Dale Miller Proof checking and logic programming . . 383--399
Hirohisa Seki On dual programs in co-logic programming
and the Horn $ \mu $-calculus . . . . . 401--421
José Meseguer and
Stephen Skeirik Equational formulas and pattern
operations in initial order-sorted
algebras . . . . . . . . . . . . . . . . 423--452
Peng Fu and
Ekaterina Komendantskaya Operational semantics of resolution and
productivity in Horn clause logic . . . 453--474
Sergio Antoy and
Michael Hanus Transforming Boolean equalities into
constraints . . . . . . . . . . . . . . 475--494
Dipak L. Chaudhari and
Om Damani Assumption propagation through annotated
programs . . . . . . . . . . . . . . . . 495--530
Marco Comini and
María-del-Mar Gallardo and
Laura Titolo and
Alicia Villanueva A program analysis framework for tccp
based on abstract interpretation . . . . 531--557
Michael Codish and
Luís Cruz-Filipe and
Markus Nebel and
Peter Schneider-Kamp Optimizing sorting algorithms by using
sorting networks . . . . . . . . . . . . 559--579
Xuandong Li and
Zhiming Liu Editorial . . . . . . . . . . . . . . . 581--582
Gregor V. Bochmann and
Martin Hilscher and
Sven Linker and
Ernst-Rüdiger Olderog Synthesizing and verifying controllers
for multi-lane traffic maneuvers . . . . 583--600
David Faitelson and
Shmuel Tyszberowicz Improving design decomposition (extended
version) . . . . . . . . . . . . . . . . 601--627
Hassan Hatefi and
Ralf Wimmer and
Bettina Braitling and
Luis María Ferrer Fioriti and
Bernd Becker and
Holger Hermanns Cost vs. time in stochastic games and
Markov automata . . . . . . . . . . . . 629--649
Sebastian Junges and
Dennis Guck and
Joost-Pieter Katoen and
Arend Rensink and
Mariëlle Stoelinga Fault trees on a diet: automated
reduction by graph rewriting . . . . . . 651--703
Ben Moszkowski and
Dimitar P. Guelev An application of temporal projection to
interleaving concurrency . . . . . . . . 705--750
Shuling Wang and
Naijun Zhan and
Lijun Zhang A Compositional Modelling and
Verification Framework for Stochastic
Hybrid Systems . . . . . . . . . . . . . 751--775
Pavel Jancík and
Jan Kofron On partial state matching . . . . . . . 777--803
Daniel Gaina Birkhoff style calculi for hybrid logics 805--832
Wim H. Hesselink Tournaments for mutual exclusion:
verification and concurrent complexity 833--852
Robert J. Colvin and
Ian J. Hayes and
Larissa A. Meinicke Designing a semantic model for a
wide-spectrum language with concurrency 853--875
Rumyana Neykova and
Laura Bocchi and
Nobuko Yoshida Timed runtime monitoring for multiparty
conversations . . . . . . . . . . . . . 877--910
Peter Schrammel and
Daniel Kroening and
Martin Brain and
Ruben Martins and
Tino Teige and
Tom Bienmüller Incremental bounded model checking for
embedded software . . . . . . . . . . . 911--931
Anonymous Michael J. C. Gordon, FRS, Professor of
Computer Assisted Reasoning (28 February
1948--22 August 2017) . . . . . . . . . 933--933
Graeme Smith and
Kirsten Winter Relating trace refinement and
linearizability . . . . . . . . . . . . 935--950
Hosein Nazarpour and
Yli\`es Falcone and
Saddek Bensalem and
Marius Bozga Concurrency-preserving and sound
monitoring of multi-threaded
component-based systems: theory,
algorithms, implementation, and
evaluation . . . . . . . . . . . . . . . 951--986
Mohamed Graiet and
Lazhar Hamel and
Amel Mammar and
Samir Tata A verification and deployment approach
for elastic component-based applications 987--1011
Ramiro Demasi and
Pablo F. Castro and
Thomas S. E. Maibaum and
Nazareno Aguirre Simulation relations for fault-tolerance 1013--1050
Behnaz Yousefi and
Fatemeh Ghassemi and
Ramtin Khosravi Modeling and efficient verification of
wireless ad hoc networks . . . . . . . . 1051--1086
Sebastian Eggert and
Ron van der Meyden Dynamic intransitive noninterference
revisited . . . . . . . . . . . . . . . 1087--1120
Cliff B. Jones Book Review: \booktitleThe Turing Guide,
By Jack Copeland, Jonathan Bowen, Mark
Sprevak, Robin Wilson and others. Oxford
University Press, Oxford, UK, 26 January
2017, xv + 576 pp, 246 $ \times $ 189
mm, ISBN: 978-0-19-874782-6 (Hardback,
\$75.00), ISBN: 978-0-19-874783-3
(Paperback, \$19.99) . . . . . . . . . . 1121--1122
Ewen Denney and
Perdita Stevens and
Andrzej Wasowski Editorial . . . . . . . . . . . . . . . 1--1
Sander de Putter and
Anton Wijs A formal verification technique for
behavioural model-to-model
transformations . . . . . . . . . . . . 3--43
Philipp Chrszon and
Clemens Dubslaff and
Sascha Klüppelholz and
Christel Baier ProFeat: feature-oriented engineering
for family-based probabilistic model
checking . . . . . . . . . . . . . . . . 45--75
Marcus Gerhold and
Mariëlle Stoelinga Model-based testing of probabilistic
systems . . . . . . . . . . . . . . . . 77--106
Jean-Christophe Léchenet and
Nikolai Kosmatov and
Pascale Le Gall Cut branches before looking for bugs:
certifiably sound verification on
relaxed slices . . . . . . . . . . . . . 107--131
D. Strüber and
J. Rubin and
T. Arendt and
M. Chechik and
G. Taentzer and
J. Plöger Variability-based model transformation:
formal foundation and application . . . 133--162
Claudio Corrodi and
Alexander Heußner and
Christopher M. Poskitt A semantics comparison workbench for a
concurrent, asynchronous, distributed
programming language . . . . . . . . . . 163--192
Jianwen Li and
Lijun Zhang and
Shufang Zhu and
Geguang Pu and
Moshe Y. Vardi and
Jifeng He An explicit transition system
construction approach to LTL
satisfiability checking . . . . . . . . 193--217
Hui Zhang and
Jinzhao Wu Formal verification and quantitative
metrics of MPSoC data dynamics . . . . . 219--237
Jan B. Pedersen and
Peter H. Welch The symbiosis of concurrency and
verification: teaching and case studies 239--277
Riccardo Sisto and
Piergiuseppe Bettassa Copet and
Matteo Avalle and
Alfredo Pironti Formally sound implementations of
security protocols with JavaSPI . . . . 279--317
Khaled El-Fakih and
Nina Yevtushenko and
Natalia Kushik Adaptive distinguishing test cases of
nondeterministic finite state machines:
test case derivation and length
estimation . . . . . . . . . . . . . . . 319--332
Filipe Santos and
Krystian Kwiecinski and
Ana de Almeida and
Sara Eloy and
Bruno Taborda Alternative shaper: a model for
automatic design generation . . . . . . 333--349
Ling Shi and
Yongxin Zhao and
Yang Liu and
Jun Sun and
Jin Song Dong and
Shengchao Qin A UTP semantics for communicating
processes with shared variables and its
formal encoding in PVS . . . . . . . . . 351--380
Yuyan Bao and
Gary T. Leavens and
Gidon Ernst Unifying separation logic and region
logic to allow interoperability . . . . 381--441
Yaping Jing and
Andrew S. Miner Computation tree measurement language
(CTML) . . . . . . . . . . . . . . . . . 443--462
Raphaël Chane-Yack-Fa and
Marc Frappier and
Amel Mammar and
Alain Finkel Parameterized verification of monotone
information systems . . . . . . . . . . 463--489
Stefan Hallerstede Book Review: Tobias Nipkow and Gerwin
Klein: \booktitleConcrete Semantics with
Isabelle/HOL, Springer Verlag, 2014, x +
289 pp, EUR 63,29 (Hardback), ISBN
978-3-319-10542-0,
http://www.concrete-semantics.org/ . . . 491--492
Nikolaj Bjòrner and
Frank de Boer and
Andrew Butterfield Editorial . . . . . . . . . . . . . . . 493--494
Nadia Polikarpova and
Julian Tschannen and
Carlo A. Furia A fully verified container library . . . 495--523
Hamid Bagheri and
Eunsuk Kang and
Sam Malek and
Daniel Jackson A formal approach for detection of
security flaws in the Android permission
system . . . . . . . . . . . . . . . . . 525--544
David Schneider and
Michael Leuschel and
Tobias Witt Model-based problem solving for
university timetable validation and
improvement . . . . . . . . . . . . . . 545--569
Karam Abd Elkader and
Orna Grumberg and
Corina S. P\uas\uareanu and
Sharon Shoham Automated circular assume-guarantee
reasoning . . . . . . . . . . . . . . . 571--595
John Derrick and
Simon Doherty and
Brijesh Dongol and
Gerhard Schellhorn and
Oleg Travkin and
Heike Wehrheim Mechanized proofs of opacity: a
comparison of two techniques . . . . . . 597--625
Bernhard K. Aichernig and
Carlo A. Furia and
Marie-Claude Gaudel and
Rob Hierons Special section of Tests and Proofs 2016 627--628
Guillaume Petiot and
Nikolai Kosmatov and
Bernard Botella and
Alain Giorgetti and
Jacques Julliand How testing helps to diagnose proof
failures . . . . . . . . . . . . . . . . 629--657
Catherine Dubois and
Alain Giorgetti Tests and proofs for custom data
generators . . . . . . . . . . . . . . . 659--684
Roberto Bruni and
Roberto Giacobazzi and
Roberta Gori Code obfuscation against abstraction
refinement attacks . . . . . . . . . . . 685--711
Wanling Xie and
Shuangqing Xiang and
Huibiao Zhu A UTP approach for rTiMo . . . . . . . . 713--738
Zhiping Shi and
Aixuan Wu and
Xiumei Yang and
Yong Guan and
Yongdong Li and
Xiaoyu Song Formal analysis of the kinematic
Jacobian in screw theory . . . . . . . . 739--757
Rosemary Monahan Book Review: Daniel Kroening and Ofer
Strichman: \booktitleDecision
procedures, Springer Verlag, 2016, xxi +
356 pp. ISBN 978-3-662-50496-3
(hardback, EUR 69,67),
http://www.decision-procedures.org/ . . 759--759
Jonathan P. Bowen Book Review: Egon Börger and Alexander
Raschke: \booktitleModeling companion
for software practitioners, Springer,
2018, xxi + 349 pp, ISBN:
978-3-662-56639-8 (Paperback, \pounds
46.99), eISBN: 978-3-662-56641-1 (eBook,
\pounds 36.99),
https://doi.org/10.1007/978-3-662-56641-1 761--762
Martin Fränzle and
Deepak Kapur and
Heike Wehrheim and
Naijun Zhan Editorial . . . . . . . . . . . . . . . 1--1
Mingsheng Ying Toward automatic verification of quantum
programs . . . . . . . . . . . . . . . . 3--25
Andrzej Mizera and
Jun Pang and
Qixia Yuan GPU-accelerated steady-state computation
of large probabilistic Boolean networks 27--46
Xiaoju Dong and
Yuxi Fu and
Daniele Varacca Extensional Petri net . . . . . . . . . 47--58
Marco Bozzano and
Alessandro Cimatti and
Cristian Mattarei Formal reliability analysis of
redundancy architectures . . . . . . . . 59--94
Yuhui Lin and
Alan Bundy and
Gudmund Grov and
Ewen Maclean Automating Event-B invariant proofs by
rippling and proof patching . . . . . . 95--129
Stefania Gnesi and
Ana Cavalcanti and
John Fitzgerald and
Constance Heitmeyer Editorial . . . . . . . . . . . . . . . 131--132
Ian J. Hayes and
Larissa A. Meinicke and
Kirsten Winter and
Robert J. Colvin A synchronous program algebra: a basis
for reasoning about shared-memory and
event-based concurrency . . . . . . . . 133--163
Fabrizio Biondi and
Yusuke Kawamoto and
Axel Legay and
Louis-Marie Traonouez Hybrid statistical estimation of mutual
information and its application to
information flow . . . . . . . . . . . . 165--206
Quang-Trung Ta and
Ton Chanh Le and
Siau-Cheng Khoo and
Wei-Ngan Chin Automated mutual induction proof in
separation logic . . . . . . . . . . . . 207--230
Aleksandar S. Dimovski and
Claus Brabrand and
Andrzej Wasowski Finding suitable variability
abstractions for lifted analysis . . . . 231--259
Morten Bisgaard and
David Gerhardt and
Holger Hermanns and
Jan Kr\vcál and
Gilles Nies and
Marvin Stenger Battery-aware scheduling in low orbit:
the GomX-3 case . . . . . . . . . . . . 261--285
Tsutomu Kobayashi and
Fuyuki Ishikawa and
Shinichi Honiden Consistency-preserving refactoring of
refinement structures in Event-B models 287--320
Sidi Mohamed Beillahi and
Mohamed Yousri Mahmoud and
Sofi\`ene Tahar A modeling and verification framework
for optical quantum circuits . . . . . . 321--351
Cliff B. Jones and
Nisansala Yatapanage Investigating the limits of
rely/guarantee relations based on a
concurrent garbage collector example . . 353--374
Pedro Antonino and
Thomas Gibson-Robinson and
A. W. Roscoe Efficient verification of concurrent
systems using local-analysis-based
approximations and SAT solving . . . . . 375--409
Gavin Lowe Discovering and correcting a deadlock in
a channel implementation . . . . . . . . 411--419
Antonio Brogi and
Andrea Corradini and
Jacopo Soldani Estimating costs of multi-component
enterprise applications . . . . . . . . 421--451
Richard Banach Book Review: John Fitzgerald, Peter Gorm
Larsen, Marcel Verhoef (eds):
\booktitleCollaborative design for
embedded systems, Springer, Berlin
Heidelberg, 2014, xxii + 385 pp, $ 6
\times 2 $ mm, ISBN: 978-3-642-54117-9
(hardback, \$119.99), ISBN:
978-3-662-52444-2 (softcover, \$129.00) 453--454
Igor Konnov Book Review: Edmund M. Clarke, Thomas A.
Henzinger, Helmut Veith, and Roderick
Bloem (eds): \booktitleHandbook of model
checking . . . . . . . . . . . . . . . . 455--456
Alessandra Russo and
Andy Schürr and
Heike Wehrheim Editorial . . . . . . . . . . . . . . . 457--458
Claudio Menghi and
Paola Spoletini and
Marsha Chechik and
Carlo Ghezzi A verification-driven framework for
iterative design of controllers . . . . 459--502
Si Liu and
Peter Csaba Ölveczky and
Qi Wang and
Indranil Gupta and
José Meseguer Read atomic transactions with prevention
of lost updates: ROLA and its formal
analysis . . . . . . . . . . . . . . . . 503--540
Diego Marmsoler and
Habtom Kashay Gidey Interactive verification of
architectural design patterns in FACTum 541--610
Zinovy Diskin and
Harald König and
Mark Lawford Multiple model synchronization with
multiary delta lenses with amendment and
K-Putput . . . . . . . . . . . . . . . . 611--640
Greg Michaelson Book Review: Bernhard Steffen, Oliver
Rüthing, and Michael Huth:
\booktitleMathematical Foundations of
Advanced Informatics --- Volume 1:
Inductive Approaches . . . . . . . . . . 641--642
Nachum Dershowitz and
Richard Waldinger Zohar Manna (1939--2018) . . . . . . . . 643--660
Cliff Jones and
José Oliveira Editorial . . . . . . . . . . . . . . . 661--661
Thomas Haigh Assembling a prehistory for formal
methods: a personal view . . . . . . . . 663--674
Lawrence C. Paulson and
Tobias Nipkow and
Makarius Wenzel From LCF to Isabelle/HOL . . . . . . . . 675--698
J. Strother Moore Milestones from the Pure Lisp theorem
prover to ACL2 . . . . . . . . . . . . . 699--732
Damien Pous and
Davide Sangiorgi Bisimulation and Coinduction
Enhancements: A Historical Perspective 733--749
Krzysztof R. Apt and
Ernst-Rüdiger Olderog Fifty years of Hoare's logic . . . . . . 751--807
Graeme Smith and
Kirsten Winter and
Robert J. Colvin Linearizability on hardware weak memory
models . . . . . . . . . . . . . . . . . 1--32
L. Baresi and
M. M. Bersani and
F. Marconi and
G. Quattrocchi and
M. Rossi Using formal verification to evaluate
the execution time of Spark applications 33--70
Waqar Ahmad and
Osman Hasan and
Sofi\`ene Tahar Formal reliability and failure analysis
of Ethernet based communication networks
in a smart grid substation . . . . . . . 71--111
Yanhong Huang and
Haiping Pang and
Jianqi Shi Modeling and Verification of a Timing
Protection Mechanism in the OSEK/VDX OS
using CSP . . . . . . . . . . . . . . . 113--145
Jonathan P. Bowen Book Review: Gerard O'Regan:
\booktitleConcise Guide to Formal
Methods: Theory, Fundamentals and
Industry Applications . . . . . . . . . 147--148
Alexander Knapp and
Markus Roggenbach Book Review: André Platzer:
\booktitleLogical foundations of
cyber-physical systems . . . . . . . . . 149--151
Zinovy Diskin and
Harald König and
Mark Lawford Correction to: Multiple model
synchronization with multiary delta
lenses with amendment and K-Putput . . . 153--153
Ana Cavalcanti and
Pedro Ribeiro Editorial . . . . . . . . . . . . . . . 155--155
Douglas Fraser and
Ruben Giaquinta and
Gethin Norman Collaborative models for autonomous
systems controller synthesis . . . . . . 157--186
Marcello M. Bersani and
Matteo Soldo and
Matteo Rossi PuRSUE --- from specification of robotic
environments to synthesis of controllers 187--227
Adnan Rashid and
Osman Hasan Formal Verification of Robotic Cell
Injection systems up to $4$-DOF using
HOL Light . . . . . . . . . . . . . . . 229--250
David M. Williams and
Salaheddin Darwish and
David R. Michael Legislation-driven development of a Gift
Aid system using Event-B . . . . . . . . 251--273
Feng Sheng and
Huibiao Zhu and
Jonathan P. Bowen Theoretical and Practical Approaches to
the Denotational Semantics for MDESL
based on UTP . . . . . . . . . . . . . . 275--314
Matthieu Renard and
Antoine Rollet and
Yli\`es Falcone Runtime enforcement of timed properties
using games . . . . . . . . . . . . . . 315--360
Aida Lahouij and
Lazhar Hamel and
Béchir el Ayeb An Event-B based approach for cloud
composite services verification . . . . 361--393
Xilong Zhuo and
Chenyi Zhang TFA: an efficient and precise virtual
method call resolution for Java . . . . 395--416
Shanyan Chen and
Guohui Wang and
Yong Guan Formalization of Camera Pose Estimation
Algorithm based on Rodrigues Formula . . 417--437
Erik de Vink and
Ana Cavalcanti Editorial . . . . . . . . . . . . . . . 1--2
Giovanni Bacci and
Patricia Bouyer and
Pierre-Alain Reynier Optimal and robust controller synthesis
using energy timed automata with
uncertainty . . . . . . . . . . . . . . 3--25
Davide G. Cavezza and
Dalal Alrajeh and
András György A Weakness Measure for GR(1) Formulae 27--63
Aaron Dutle and
Mariano Moscato and
François Bobot Formal analysis of the compact position
reporting algorithm . . . . . . . . . . 65--86
S. Geisler and
A. E. Haxthausen Stepwise development and model checking
of a distributed interlocking system
using RAISE . . . . . . . . . . . . . . 87--125
Thomas Letan and
Yann Régis-Gianas and
Guillaume Hiet Modular verification of programs with
effects and effects handlers . . . . . . 127--150
Wenbo Zhang and
Xian Xu and
Huan Long On the Interactive Power of Higher-order
Processes Extended with Parameterization 151--183
Wim H. Hesselink UNITY and Büchi automata . . . . . . . . 185--205
Wanling Xie and
Huibiao Zhu and
Qiwen Xu A process calculus BigrTiMo of mobile
systems and its formal semantics . . . . 207--249
Marco Bozzano and
Alessandro Cimatti and
Cristian Mattarei Model-based Safety Assessment of a
Triple Modular Generator with xSAP . . . 251--295
Matteo Rossi Modeling and analysis of communicating
systems . . . . . . . . . . . . . . . . 297--298
Xiaoping Chen and
Zhiming Liu and
Jim Woodcock Editorial . . . . . . . . . . . . . . . 299--300
Lei Bu and
Yongjuan Liang and
Xuandong Li Machine learning steered symbolic
execution framework for complex software
code . . . . . . . . . . . . . . . . . . 301--323
Huihui Wu and
Deyun Lv and
Weiqiang Kong SDLV: Verification of Steering Angle
Safety for Self-Driving Cars . . . . . . 325--341
Zhibin Yang and
Yang Bao and
Zonghua Gu Exploiting augmented intelligence in the
modeling of safety-critical autonomous
systems . . . . . . . . . . . . . . . . 343--384
Xiangyu Jin and
Jie An and
Miaomiao Zhang Inferring Switched Nonlinear Dynamical
Systems . . . . . . . . . . . . . . . . 385--406
Pengfei Yang and
Jianlin Li and
Lijun Zhang Enhancing Robustness Verification for
Deep Neural Networks via Symbolic
Propagation . . . . . . . . . . . . . . 407--435
Hengjun Zhao and
Xia Zeng and
Jim Woodcock Learning safe neural network controllers
with barrier certificates . . . . . . . 437--455
Michele Loreti Semantics of the probabilistic Lambda
Calculus By Dirk Draheim . . . . . . . . 457--458
Annabelle McIver and
Maurice H ter Beek Editorial . . . . . . . . . . . . . . . 459--460
Yong Kiam Tan and
André Platzer An axiomatic approach to existence and
liveness for differential equations . . 461--518
Hoang-Dung Tran and
Neelanjana Pal and
Taylor T. Johnson Verification of piecewise deep neural
networks: a star set approach with
zonotope pre-filter . . . . . . . . . . 519--545
John Derrick and
Simon Doherty and
Heike Wehrheim Verifying correctness of persistent
concurrent data structures: a sound and
complete method . . . . . . . . . . . . 547--573
Martin Tappler and
Bernhard K. Aichernig and
Kim G. Larsen $ L^* $-based learning of Markov
decision processes (extended version) 575--615
Frank S. de Boer and
Marcello Bonsangue Symbolic execution formally explained 617--636
Milan Ceska and
Christian Hensel and
Joost-Pieter Katoen Counterexample-guided inductive
synthesis for probabilistic systems . . 637--667
Alexandros Evangelidis and
David Parker Quantitative verification of Kalman
filters . . . . . . . . . . . . . . . . 669--693
Thorsten Wißmann and
Hans-Peter Deifel and
Lutz Schröder From generic partition refinement to
weighted tree automata minimization . . 695--727
Gal Amram and
Shahar Maoz and
Or Pistiner GR(1)*: GR(1) specifications extended
with existential guarantees . . . . . . 729--761
Mario Gleirscher and
Radu Calinescu and
Jim Woodcock RiskStructures : A design algebra for
risk-aware machines . . . . . . . . . . 763--802
Gerard Ekembe Ngondi Denotational semantics of channel
mobility in UTP-CSP . . . . . . . . . . 803--826
Wolfgang Ahrendt and
Silvia Lizeth Tapia Tarifa and
Heike Wehrheim Editorial . . . . . . . . . . . . . . . 827--827
Bjòrnar Luteberget and
Christian Johansen Drawing with SAT: four methods and A
tool for producing railway
infrastructure schematics . . . . . . . 829--854
Simon Foster and
Yakoub Nemouchi and
Tim Kelly Integration of Formal Proof into Unified
Assurance Cases with Isabelle/SACM . . . 855--884
Clemens Dubslaff and
Patrick Koopmann and
Anni-Yasmin Turhan Enhancing Probabilistic Model Checking
with Ontologies . . . . . . . . . . . . 885--921
Alessandro Fantechi and
Anne E. Haxthausen and
Jim Woodcock Editorial . . . . . . . . . . . . . . . 923--924
Jan Peleska and
Niklas Krafczyk and
Ralf Pinger Efficient data validation for
geographical interlocking systems . . . 925--955
Davide Basile and
Alessandro Fantechi and
Gianluca Mand\`o Analysing an autonomous tramway
positioning system with the Uppaal
Statistical Model Checker . . . . . . . 957--987
Francesco Flammini and
Stefano Marrone and
Valeria Vittorini Compositional modeling of railway
Virtual Coupling with Stochastic
Activity Networks . . . . . . . . . . . 989--1007
Paulius Stankaitis and
Alexei Iliasov and
Alexander Romanovsky A refinement-based development of a
distributed signalling system . . . . . 1009--1036
Jordi Cabot and
Heike Wehrheim and
Eerke Boiten Editorial . . . . . . . . . . . . . . . 1037--1037
Claudio Menghi and
Alessandro Maria Rizzi and
Paola Spoletini TOrPEDO: witnessing model correctness
with topological proofs . . . . . . . . 1039--1066
Patrick Stünkel and
Harald König and
Adrian Rutle Comprehensive Systems: A formal
foundation for Multi-Model Consistency
Management . . . . . . . . . . . . . . . 1067--1114
Nils Weidmann and
Anthony Anjorin Schema Compliant Consistency Management
via Triple Graph Grammars and Integer
Linear Programming . . . . . . . . . . . 1115--1145
Maxime Cordy and
Sami Lazreg and
Axel Legay Statistical model checking for
variability-intensive systems:
applications to bug detection and
minimization . . . . . . . . . . . . . . 1147--1172
Juan de Lara and
Esther Guerra Language Family Engineering with Product
Lines of Multi-level Models . . . . . . 1173--1208
Rolf Hennicker and
Alexander Knapp and
Alexandre Madeira Hybrid dynamic logic institutions for
event/data-based systems . . . . . . . . 1209--1248
Blair Archibald and
Géza Kulcsár and
Michele Sevegnani A tale of two graph models: a case study
in wireless sensor networks . . . . . . 1249--1277
Reinhard Wilhelm Foundations of programming languages . . 1279--1280