Logo - springer
Slogan - springer

Computer Science - Theoretical Computer Science | Formal Aspects of Computing-incl. option to publish open access (Editorial Board)

Formal Aspects of Computing

Formal Aspects of Computing

Applicable Formal Methods

Chief Editor: James Woodcock

ISSN: 0934-5043 (print version)
ISSN: 1433-299X (electronic version)

Journal no. 165

$99.00 Personal Rate e-only for the Americas
Get Subscription

Online subscription, valid from January through December of current calendar year

Immediate access to this year's issues via SpringerLink

1 Volume(-s) with 6 issue(-s) per annual subscription

Automatic annual renewal

More information: >> FAQs // >> Policy


Prof. J. C. P. Woodcock
Department of Computer Science,
University of York,
Heslington, York,
YO10 5GH, UK
email: jim.woodcock@york.ac.uk

Associate Editor

Dr. D. J. Cooke
Department of Computer Science,
Loughborough University,
Loughborough, LE11 3TU, UK
email: D.J.Cooke@lboro.ac.uk

North American Editor

Prof. J. M. Wing
Microsoft Research
One Microsoft Way
Redmond, WA  98052
email: wing@microsoft.com

Founding Editor

Prof. C. B. Jones
Department of Computing Science,
University of Newcastle Upon Tyne,
email: Cliff.Jones@ncl.ac.uk

Editorial Advisor

Prof. M. Broy
Institut für Informatik, Technische Universität München, Lehrstuhl IV, Boltzmannst. 3, Garching bei München, Germany
email: broy@in.tum.de

Editorial Board

Prof. D. Bjorner
Technical Univ. of Denmark, Denmark
email: bjorner@gmail.com
(Domain modelling techniques; Domain-based requirements modelling techniques)

Prof. E. Boiten
School of Computer Science and Informatics, De Montfort University, The Gateway, Leicester, LE1 9BH, UK
email: eerke.boiten@dmu.ac.uk
(State-based specification languages (Z, B, ...); Refinement; Integrated formal methods; Formal methods in security; Formal methods in cryptography; Viewpoint specification)

Prof. M. J. Butler
School of Electronics and Computer Science, University of Southampton, SO17 1BJ, UK
email: mjb@ecs.soton.ac.uk
(Requirements; Formal specification; Refinement, Design verification; Theorem proving, Model checking; Formal tools; Semantics)

Dr. A. Butterfield
School of Computer Science and Statistics O'Reilly Institute Trinity College, Dublin 2, Ireland
email: Andrew.Butterfield@scss.tcd.ie
(Unifying theories of programming (esp. CSP/Circus related matters, including priority,
probability); Formal aspects of the hardware/software interface; Theorem Prover development;
Developing expertise/interest in formal verification of separation kernels, and potential tools
(Isabelle/HOL, Frama-C, ...); Semantics and use of functional programming languages)

Prof. Ana Cavalcanti
Department of Computer Science, University of York, Heslington, York, YO10 5DD, UK
email: Ana.Cavalcanti@york.ac.uk
(Refinement, Integrated formal methods, Process algebra, Real-time programming, Cyber-physical systems, Formal testing)

Dr. E. Denney
m/s 269-2, NASA Ames Research Center, Moffett Field, CA 94035, USA
email: ewen.w.denney@nasa.gov
(Safety cases; Program generation; Theorem proving, Semantics; Refinement)

Dr. Jin Song Dong
Department of Computer Science, School of Computing, National University of Singapore, 3 Science Drive 2, Singapore 117543
email: dongjs@comp.nus.edu.sg
(Model checking; Real-time system verification; probabilistic reasoning; Z; Alloy; CSP)

Prof. D.J. Duke
School of Computing, University of Leeds, Woodhouse Lane, Leeds, LS2 9JT, UK
email: D.J.Duke@leeds.ac.uk
(Formal methods in human-computer interaction; Visualization; Graphics; Functional programming)

Prof. E. A. Emerson
Department of Computer Science, University of Texas at Austin, Austin, TX 7812, USA
email: emerson@cs.utexas.edu
(Model checking; Program synthesis; Program repair; Formal specification; Automata-based reasoning; Concurrency)

Prof. X. Feng
University of Science and Technology of China, PO Box 4, Hefei, Anhui 230027, China
email:  xinyu.feng@gmail.com
(Formal program verification; Hoare logic; Separation logic; Rely-Guarantee reasoning; Shared-Memory concurrency; Proof assistants and mechanized verification; Proof-Carrying code; Semantics of programming languages)

Prof. M.-C. Gaudel
LRI, University Paris-Sud PCRI , Batiment 650 91405, Orsay cedex, France
email: mcg@lri.fr
(Formal methods; Software specification; Specification-based testing; Testing strategies)

Prof. A. Haxthausen
Department of Applied Mathematics and Computer Science, Technical University of Denmark, Richard Petersens Plads, Building 324,  DK-2800 Lyngby, Denmark
email: aeha@dtu.dk
(Specification languages and their semantics, formal modelling and verification of railway control systems; Model checking)

Prof. I. J. Hayes
Department of Computer Science, University of Queensland, Brisbane, Queensland 4072, Australia
email: Ian.Hayes@itee.uq.edu.au
(Reasoning about concurrent and real-time programs; Program derivation and refinement; Model-based specification)

Prof. R. M. Hierons
Department of Computer Science, Brunel University London, Uxbridge, Middlesex, UB8 3PH, UK
email: Rob.Hierons@brunel.ac.uk
(Testing from formal specifications; Model-based testing; Program slicing)

Prof. S. Honiden
National Institute of Informatics (NII), 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 1018430, Japan
email: honiden@nii.ac.jp
(Software engineering for self-adaptive systems)

Prof. He Jifeng
Software Engineering Institue, East China Normal University, 3663 Zhongshan Road (North), Shanghai, 200062, China
email: jifeng@sei.ecnu.edu.cn
(Cyber physical systems; Hybrid modeling techniques​; Simulation and verification of design stage, Coordination and collaboration of distributed systems)

Prof. G. Klein
NICTA and University of South Wales, Locked Bag 6016, Sydney NSW 1466, Australia
email: gerwin.klein@nicta.com.au
(Interactive theorem proving; Program verification; C code verification; Programming language semantics; Proof engineering; Formal methods)

Prof. D. Kroening
Department of Computer Science, University of Oxford Parks Road, Oxford, OX1 3QD, UK
email: kroening@cs.ox.ac.uk
(Automated verification of hardware and software; Semantics of programming languages; Concurrency)

Dr. C. J. P. de Lucena
Pontifica Universidade Catholica do Rio de Janeiro, PUCRJ, Departmento de Informatica, Rue Marques de Sao Vicente 225, Gavea, Rio de Janeiro CEP, 22453, Brazil
email: lucena@inf.puc-rio.br
(Formal specification of software systems; Model checking; Foundations of software design; Formal aspects of software engineering of multiagent systems)

Prof. U. H. M. Martin
Department of Computer Science, University of Oxford Wolfson Building Parks Road OXFORD, OX1 3QD, UK
email: Ursula.Martin@cs.ox.ac.uk
(Computational logic; Applied formal methods; Computer algebra)

Prof. D. Mery
LORIA, Université de Lorraine, Campus Scientifique, BP 70239, F-54506 Vandoeuvre-lès-Nancy, France
email:  dominique.mery@loria.fr
(Well-founded notations for the description of systems like B, Event B , TLA+, Temporal logic
based method, state-based methods; Verifiable design methods: refinement, abstract interpretation; State-exploration tools: model checking; Semantics of programming languages, fixed-point theory; Design by contract; Applications: distributed algorithms; Security and safety properties; System engineering)

Prof. D. A. Naumann
Department of Computer Science, Stevens Institute of Technology, Hoboken NJ 07030, USA
email: naumann@cs.stevens.edu
(Formal semantics; Logics of programming; Refinement; Information flow analysis)

Prof. J. Nuno Oliveira
Departmento de Informática/HASLab, Universidade do Minho/INESC TEC, 4710-057 Braga, Portugal
email: jno@di.uminho.pt
(Relational specification methods; Quantitative formal methods; Program calculation)

Prof. J. Parrow
Department of Information Technology, University of Uppsala, Box 337, 751 05 Uppsala, Sweden
email: joachim.parrow@it.uu.se
(Process calculi; Concurrency; Bisimulation)

Prof. A. Sampaio
Centro de Informática, Universidade Federal de Pernambuco, Av. Jornalista Anibal Fernandes, s/n - Cidade Universitária, 50.740-560 - Recife - PE, Brazil
email: acas@cin.ufpe.br
(Process algebras (particularly, CSP); Compositional analysis techniques; Formal (and semi-formal) methods integration; Formal approaches to software testing; Algebraic approaches to model and program transformation)

Dr. G. Schellhorn
University of Augsburg, Institute for Software and Systems Engineering (ISSE), Universitaetsstrasse 6a, 86159 Augsburg, Germany
email: schellhorn@informatik.uni-augsburg.de
(Refinement theory; Software correctness; Interactive verification; Logics for programs; Verification of concurrent algorithms)

Prof. J. V. Tucker

Department of Computer Science, Swansea University, Singleton Park, Swansea SA2 8PP, UK
email: J.V.Tucker@swansea.ac.uk
(Modelling data types; Computability; Algebraic specifications; Formal methods for surveillance, trust and privacy; Specifying physical systems; History of formal methods)

Prof. H. Wehrheim
Department of Computer Science, University of Paderborn, Warburger Str. 100. D-33098, Paderborn, Germany
email: wehrheim@uni-paderborn.de
(Z, B, process algebras; Refinement; Simulation; Verification; Program analysis; Concurrency)

Prof. N. Zhan
State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, No. 4, South Fourth Street, Zhong Guan Cun, Beijing, 100190, P.R. China
email:  znj@ios.ac.cn
(Formal techniques for the design of real-time ,hybrid and embedded systems; Program verification; Modal and temporal logics; Concurrent computation models; Semantic foundations of component and object systems)

Read this Journal on Springerlink

For authors and editors

  • Journal Citation Reports®
    2016 Impact Factor
  • 1.041
  • Aims and Scope

    Aims and Scope


    This journal aims to publish contributions at the junction of theory and practice.  The objective is to disseminate applicable research.  Thus new theoretical contributions are welcome where they are motivated by potential application; applications of existing formalisms are of interest if they show something novel about the approach or application.

    The term "formal methods" has been applied to a range of notations, theories and tools.  There is no doubt that some of these have already had a significant impact on practical applications of computing.  Indeed, it is interesting to note that once something is adopted into practical use it is no longer thought of as a formal method.  Apart from widely used notations such as those for syntax and state machines, there have been significant applications of specification notations, development methods and tools both for proving general results and for searching for specific conditions.  However, the most profound and lasting influence of the formal approach is the way it has illuminated fundamental concepts like those of communication.

    In this spirit, the principal aim of this journal is to promote the growth of computing science, to show its relation to practice and to stimulate applications of apposite formalisms to practical problems.  One significant challenge is to show how a range of formal models can be related to each other.

    In particular, the scope of Formal Aspects of Computing includes,
    • well-founded notations for the description of systems
    • verifiable design methods
    • elucidation of fundamental computational concepts
    • approaches to fault-tolerant design
    • theorem-proving support
    • state-exploration tools
    • formal underpinning of widely used notations and methods
    • formal approaches to requirements analysis

    Normal scientific standards are expected of all contributors: papers must be soundly based, place their contribution in context and provide adequate references.  Material which is already widely available (e.g. as conference proceedings) will not normally be considered unless the work has been further developed and refined.


  • Submit Online
  • Open Choice - Your Way to Open Access
  • Instructions for Authors

    Instructions for Authors


  • Author Academy: Training for Authors
  • English Language Editing

    English Language Editing


  • Copyright Information

    Copyright Information


    Submission of a manuscript implies: that the work described has not been published before (except in the form of an abstract or as part of a published lecture, review, or thesis); that it is not under consideration for publication elsewhere; that its publication has been approved by all co-authors, if any, as well as - tacitly and explicitly - by the responsible authorities at the institution where the work was carried out. Transfer of copyright to BCS becomes effective if and when the article is accepted for publication. The copyright covers the exclusive right (for U.S. government employees: to the extent transferable) to reproduce and distribute the article, including reprints, translations, photographic reproductions, microform, electronic form (offline, online) or other reproductions of similar nature.

    All articles published in this journal are protected by copyright, which covers the exclusive rights to reproduce and distribute the article (e. g., as offprints), as well as all translation rights. No material published in this journal may be reproduced photographically or stored on microfilm, in electronic data bases, video disks, etc., without first obtaining written permission from the publisher. The use of general descriptive names, trade names, trademarks, etc., in this publication, even if not specifically identified, does not imply that these names are not protected by the relevant laws and regulations.

    An author may make his/her article published by Springer-Verlag London available on his/her personal home page, provided the source of the published article is cited and BCS is mentioned as the copyright owner. Authors are requested to create a link to the published article in Springer´s internet service. The link must be accompanied by the following text: "The original publication is available at springerlink.com".

    Please use the appropriate URL and/or DOI for the article. Articles disseminated via SpringerLink are indexed, abstracted and referenced by many abstracting and information services, bibliographic networks, subscription agencies, library networks, and consortia.

    The author warrants that this contribution is original and that he/she has full power to make this grant. The author signs for and accepts responsibility for releasing this material on behalf of any and all co-authors.

    After submission of this agreement signed by the corresponding author, changes of authorship or in the order of the authors listed will not be accepted by Springer-Verlag.

    While the advice and information in this journal is believed to be true and accurate at the date of its publication, neither the authors, the editors, nor the publisher can accept any legal responsibility for any errors or omissions that may be made. The publisher makes no warranty, express or implied, with respect to the material contained herein.

    Special regulations for photocopies in the USA. Photocopies may be made to personal or in-house use beyond the limitations stipulated under Section 107 or 108 of U. S. Copyright Law, provided a fee is paid. All fees should be paid to the Copyright Clearance Center, Inc., 222 Rosewood Drive, Danvers, MA 01923, USA, Tel: +1-978-7508400, Fax: +1-978-6468600, http://www.copyright.com, stating the ISSN 0934-5043, the volume, and the first and last page numbers of each article copied. The copyright owner's consent does not include copying for general distribution, promotion, new works, or resale. In these cases specific written permission must first be obtained from the publisher.

    The Canada Institute for Scientific and Technical Infomation (CISTI) provides a comprehensive, world-wide document delivery service for all Springer-Verlag journals. For more information, or to place an order for a copyright-cleared Springer-Verlag document, please contact Client Assistant, Document Delivery, CISTI, Ottowa K1A 0S2, Canada (Tel: +1-613-993-9251; Fax: 613-952-8243; e-mail: cisti.docdel@nrc.ca).

    Springer-Verlag London Limited
    is a part of Springer Science+Business Media


    Ownership and Copyright
    © British Computer Society

Alerts for this journal


Get the table of contents of every new issue published in Formal Aspects of Computing.