Formal Aspects of Computing

Papers
(The median citation count of Formal Aspects of Computing is 0. The table below lists those papers that are above that threshold based on CrossRef citation counts [max. 250 papers]. The publications cover those that have been published in the past four years, i.e., from 2022-08-01 to 2026-08-01.)
ArticleCitations
Introduction to the Special Collection from FM 202338
The Universality of Functions in the Sciences at Large and in Computing23
OLTL: An Optimization Extension of Linear Temporal Logic21
Modelling and Analysing Routing Protocols Diagrammatically with Bigraphs17
A Theory of Probabilistic Contracts14
Validation of CHC Satisfiability with ATHENA11
Review on Formal Methods for Software Engineering: Languages, Methods, Application Domains10
Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers (Extended Version)9
Embeddings Between State and Action Based Probabilistic Logics8
Review of Logical Analysis of Hybrid Systems8
A Calculus for the Specification, Design, and Verification of Distributed Concurrent Systems6
Rod Burstall: In Memoriam6
Compositional Analysis of Probabilistic Timed Graph Transformation Systems6
SecCT: Secure and Scalable Count Query Models on Encrypted Genomic Data6
Trace Semantics for C++11 Memory Model6
On Inductive Characterization for Divergence-sensitive Probabilistic Branching Bisimilarity5
Celebrating Rance. Walter Rance Cleaveland II: July 18, 1961 - March 27, 2024. An Obituary5
Memory Consistency and Program Transformations5
Introduction to the Special Section on FM 20215
Introduction to the Special Collection from PRDC 20234
Formal Methods—My 50+ Years as an Engineer, Researcher and Scientist4
Mechanised Safety Verification for a Distributed Autonomous Railway Control System4
Introduction to the Special Collection from iFM 20233
iStar Goal Model to Z Formal Model Translation and Model Checking of CBTC Moving Block Interlocking System3
Refinement-based Specification and Analysis of Multi-core ARINC 653 Using Event-B3
Decidability of Liveness on the TSO Memory Model3
An Introduction to Input/Output Automata2
Review of Understanding Programming Languages2
Automated Generation of Modular Assurance Cases with the System Assurance Reference Model2
Waitfree Linearization of an Arbitrary Data Object2
FVF-AKA: A Formal Verification Framework of AKA Protocols for Multi-server IoT2
State Machines for Large Scale Computer Software and Systems2
The Concept of Class Invariant in Object-oriented Programming2
Towards Formal Verification of a TPM Software Stack: Achievements and Opportunities2
Tony Hoare: his path to the ACM Turing Award2
SMT based parameter identifiable combination detection for non-linear continuous and hybrid dynamics2
PoTR: Accurate and Efficient Proof of Timely-Retrievability for Storage Systems2
Review on Theories of Programming: The Life and Works of Tony Hoare1
Exploring Scalability of BFT Blockchain Protocols through Network Simulations1
Assurance Case Development for Evolving Software Product Lines: A Formal Approach1
CUBES: A Parallel Synthesizer for SQL Using Examples1
Termination and Expressiveness of Execution Strategies for Networks of Bidirectional Model Transformations1
Measurement-Noise Filtering for Automatic Discovery of Flow Splitting Ratios in ISP Networks1
Theoretical and Practical Approach to the Soundness and Completeness of Operational Semantics based on Denotational Semantics for MDESL1
Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies1
Remembering Jean-Raymond Abrial1
A Deep Reinforcement Learning Framework with Formal Verification1
Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis1
On Lexicographic Proof Rules for Probabilistic Termination1
Introduction to the Special Collection from FASE 20211
Benchmarking Combinations of Learning and Testing Algorithms for Automata Learning1
Review on : Domain Science and Engineering - A Foundation for Software Development1
Specification and Verification of Multi-Clock Systems Using a Temporal Logic with Clock Constraints1
Efficient Runtime Verification of Real-Time Systems under Parametric Communication Delays1
Multi-objective ω-Regular Reinforcement Learning1
A Refinement-based Formal Development of Cyber-physical Railway Signalling Systems1
Rooted Divergence-Preserving Branching Bisimilarity is a Congruence for Guarded CCS1
Canonical Automata for Persistent Linearizability - A Corrigendum1
Obituary for Niklaus Wirth1
JMLKelinci+: Detecting Semantic Bugs and Covering Branches with Valid Inputs Using Coverage-guided Fuzzing and Runtime Assertion Checking1
Improving Bigraph Rewriting with GrGen.NET to Enable Efficient System Simulation0
Compositional Reasoning for Non-multicopy Atomic Architectures0
Formal Specification and Verification of JDK’s Identity Hash Map Implementation0
Farewell Editorial0
Footprint Logic for Object-Oriented Components (extended paper)0
Toward Verifying Cooperatively Scheduled Runtimes Using CSP0
ω-Regular Energy Problems0
from Predicative Programming to aPToP0
Jean-Raymond Abrial (1938 – 2025) Pioneer of Formal Methods and Inventor of the B Method. An Obituary0
FuSeBMC v4: Improving Code Coverage with Smart Seeds via BMC, Fuzzing and Static Analysis0
Alfonso Caracciolo di Forino and Generalized Markov Algorithms0
Sound Runtime Assertion Checking for Memory Properties via Program Transformation0
LeanMachines: State-based Modeling with Refinement (a Lean4 Framework)0
Bit-Vector Typestate Analysis0
Editorial Introducing the New Editors-in-Chief0
Introduction to the Special Collection on the History of Formal Methods0
A Brief History of Formal Methods in China0
BPPChecker: An SMT-based Model Checker on Basic Parallel Processes0
PyQBF: A Python Framework for Solving Quantified Boolean Formulas0
Malware Analysis through Behavior Formalization0
Development and Validation of a Formal Model and Prototype for an Air Traffic Control System0
Foundations for Change-driven Query-based Runtime Monitoring of Temporal Properties0
Parameterized Hardware Verification Through A Term-level Generalized Symbolic Trajectory Evaluation And Its Linkage With Concrete Hardware Verification At Netlist Level0
RNA: R1CS Normalization Algorithm Based on Data Flow Graphs for Zero-Knowledge Proofs0
Introduction to the Special Collection from FACS 20220
The dynamics of belief: continuously monitoring and visualising complex systems0
Does Every Computer Scientist Need to Know Formal Methods?0
Internal and External Performance Fuzzing of Well-Defined Constraints for the B Method0
Introduction to the Special Collection on iFM 20240
Empirical Architecture Comparison of Two-input Machine Learning Systems for Vision Tasks0
Practical Modelling with Bigraphs0
OMAHA: Opportunistic Message Aggregation for pHase-based Algorithms0
Reasoning about expression evaluation under interference0
Reasoning About Exceptional Behavior At the Level of Java Bytecode with ByteBack0
Transition‑Based Acceptance for ω‑Regular Expression Synthesis0
Formalization of Android Activity-Fragment Multitasking Mechanism and Static Analysis of Mobile Apps0
In Memoriam: Ernest Allen Emerson II0
An SMT-Based Approach to the Verification of Knowledge-Based Programs0
RoboWorld: Verification of Robotic Systems with Environment in the Loop0
AC4: Algebraic Computation Checker for Circuit Constraints in Zero-Knowledge Proofs0
The Abstract State Machines Method0
On Formal Methods Thinking in Computer Science Education0
Experiences from the European ProCoS Projects: Provably Correct Systems0
Review on Functional Algorithms, Verified!0
A History of Formal Methods in Railways0
Special Collection on Computer Science Education0
Tony Hoare: In Memoriam0
Feature-Oriented Modelling and Analysis of a Self-Adaptive Robotic System0
Polymorphic dynamic programming by algebraic shortcut fusion0
Analysing a Library of Concurrency Primitives using CSP0
Modeling and Verification of Natural Language Requirements based on States and Modes0
Explanatory Denotational Semantics for Complex Event Patterns0
Kaki: Efficient Concurrent Update Synthesis for SDN0
Introduction to the Special Collection from iFM 20220
Review on Verified Functional Programming in Agda0
Communicating Cooperatively Scheduled Processes: On the Unlikelihood of Implementing a Pure CSP Channel0
Compositional Verification of Railway Interlocking Systems0
Denotational and Algebraic Semantics for the SMrCaIT calculus Based on UTP0
A Case in Point: Verification and Testing of a EULYNX Interface0
Introduction to the Special Section on Reliability, Safety, and Security of Railway Systems0
Introduction to the Special Collection from the International Conference on Tests and Proofs (TAP) 2020 and 20210
Isabelle/Solidity: A deep embedding of Solidity in Isabelle/HOL0
Specification and Verification of the Alpha Swarm Algorithm using NuXMV and GROOVE0
Using Multi-dimensional Quorums for Optimal Resilience in Multi-resource Blockchains0
Enhancing Context Awareness with Model Checking-based Uncertainty Representation in Decision Support Systems0
Formal Methods in Industry: A Critical Evaluation of Their Use at Amazon Web Services0
Formal Methods in Industry0
From Non-punctuality to Non-adjacency: A Quest for Decidability of Timed Temporal Logics with Quantifiers0
In Memoriam: Peter H. G. Aczel (1941-2023)0
A Compositional Simulation Framework for Abstract State Machine Models of Discrete Event Systems0
0.036098003387451