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. 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.
这本杂志旨在发表理论与实践结合的贡献。目的是传播可应用的研究成果。因此,新的理论贡献是受欢迎的,如果他们的动机是潜在的应用;如果现有形式体系的应用显示了一些关于方法或应用的新颖之处,则它们是令人感兴趣的。2特别地,计算的形式方面的范围包括:用于描述系统的有根据的符号;可验证的设计方法;基本计算概念的阐明;容错设计方法定理证明支持;状态探测工具;广泛使用的符号和方法的形式基础;需求分析的正式方法。
Fifty years of Hoare’s logic
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00501-3
Milestones from the Pure Lisp theorem prover to ACL2
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00490-3
Multiple model synchronization with multiary delta lenses with amendment and K-Putput
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00493-0
From LCF to Isabelle/HOL
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00492-1
Finding suitable variability abstractions for lifted analysis
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00479-y
Interactive verification of architectural design patterns in FACTum
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00488-x
A verification-driven framework for iterative design of controllers
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00484-1
Read atomic transactions with prevention of lost updates: ROLA and its formal analysis
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00489-w
Bisimulation and Coinduction Enhancements: A Historical Perspective
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00497-w
Consistency-preserving refactoring of refinement structures in Event-B models
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00478-z
A modeling and verification framework for optical quantum circuits
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00480-5
Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00482-3
Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00483-2
Zohar Manna (1939–2018)
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00500-4
Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds): Handbook of model checking
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00486-z
Linearizability on hardware weak memory models
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00499-8
Estimating costs of multi-component enterprise applications
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00491-2
Discovering and correcting a deadlock in a channel implementation
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00487-y
Assembling a prehistory for formal methods: a personal view
来源期刊:Formal Aspects of ComputingDOI:10.1007/s00165-019-00494-z