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 2021-03-01 to 2025-03-01.)
ArticleCitations
Compositional Verification of Railway Interlocking Systems29
Introduction to the Special Collection from FM 202322
A compositional simulation framework for Abstract State Machine models of Discrete Event Systems21
In Memoriam: Ernest Allen Emerson II18
Machine learning steered symbolic execution framework for complex software code15
Algebra-Based Reasoning for Loop Synthesis12
Probabilistic Bigraphs11
RoboWorld: Verification of Robotic Systems with Environment in the Loop9
JMLKelinci+: Detecting Semantic Bugs and Covering Branches with Valid Inputs Using Coverage-guided Fuzzing and Runtime Assertion Checking8
Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies8
Review on Theories of Programming: The Life and Works of Tony Hoare8
TOrPEDO: witnessing model correctness with topological proofs8
The Universality of Functions in the Sciences at Large and in Computing7
Introduction to the Special Collection from the International Conference on Tests and Proofs (TAP) 2020 and 20217
An SMT-Based Approach to the Verification of Knowledge-Based Programs7
Comprehensive Systems: A formal foundation for Multi-Model Consistency Management6
A Refinement-based Formal Development of Cyber-physical Railway Signalling Systems6
Introduction to the Special Collection from PRDC 20236
Verification of Crashsafe Caching in a Virtual File System Switch6
Does Every Computer Scientist Need to Know Formal Methods?6
Sound Runtime Assertion Checking for Memory Properties via Program Transformation5
iStar Goal Model to Z Formal Model Translation and Model Checking of CBTC Moving Block Interlocking System5
FuSeBMC v4: Improving Code Coverage with Smart Seeds via BMC, Fuzzing and Static Analysis5
Refinement-based Specification and Analysis of Multi-core ARINC 653 Using Event-B5
On the Interactive Power of Higher-order Processes Extended with Parameterization5
Specification and Verification of Multi-Clock Systems Using a Temporal Logic with Clock Constraints5
ω-Regular Energy Problems5
Parameterized Hardware Verification Through A Term-level Generalized Symbolic Trajectory Evaluation And Its Linkage With Concrete Hardware Verification At Netlist Level5
Fast Automated Abstract Machine Repair Using Simultaneous Modifications and Refactoring4
Feature-Oriented Modelling and Analysis of a Self-Adaptive Robotic System4
A Case in Point: Verification and Testing of a EULYNX Interface4
Introduction to the Special Section on iFM 20204
Validation of CHC Satisfiability with ATHENA4
Learning safe neural network controllers with barrier certificates3
Statistical model checking for variability-intensive systems: applications to bug detection and minimization3
Schema Compliant Consistency Management via Triple Graph Grammars and Integer Linear Programming3
Formal Specification and Verification of JDK’s Identity Hash Map Implementation3
Kaki: Efficient Concurrent Update Synthesis for SDN3
Modelling and Analysing Routing Protocols Diagrammatically with Bigraphs3
UNITY and Büchi automata3
RNA: R1CS Normalization Algorithm Based on Data Flow Graphs for Zero-Knowledge Proofs3
Editorial3
Internal and External Performance Fuzzing of Well-Defined Constraints for the B Method2
Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers (Extended Version)2
Verifying correctness of persistent concurrent data structures: a sound and complete method2
Enhancing Probabilistic Model Checking with Ontologies2
Review of Logical Analysis of Hybrid Systems2
Theoretical and Practical Approach to the Soundness and Completeness of Operational Semantics based on Denotational Semantics for MDESL2
Editorial2
Embeddings Between State and Action Based Probabilistic Logics2
FVF-AKA: A Formal Verification Framework of AKA Protocols for Multi-server IoT2
Bit-Vector Typestate Analysis1
SecCT: Secure and Scalable Count Query Models on Encrypted Genomic Data1
Compositional modeling of railway Virtual Coupling with Stochastic Activity Networks1
OMAHA: Opportunistic Message Aggregation for pHase-based Algorithms1
On Formal Methods Thinking in Computer Science Education1
Introduction to the Special Section on Reliability, Safety, and Security of Railway Systems1
Isabelle/Solidity: A deep embedding of Solidity in Isabelle/HOL1
Foundations of programming languages1
Measurement-Noise Filtering for Automatic Discovery of Flow Splitting Ratios in ISP Networks1
Compositional Reasoning for Non-multicopy Atomic Architectures1
RiskStructures : A design algebra for risk-aware machines1
Review onModelling and Verification of Secure Exams1
A process calculus BigrTiMo of mobile systemsand its formal semantics1
Polymorphic dynamic programming by algebraic shortcut fusion1
State Machines for Large Scale Computer Software and Systems1
Model-based Safety Assessment of a Triple Modular Generator with xSAP0
A Debugging Game for Probabilistic Models0
Tight Error Analysis in Fixed-point Arithmetic0
PoTR: Accurate and Efficient Proof of Timely-Retrievability for Storage Systems0
Trace Semantics for C++11 Memory Model0
A refinement-based development of a distributed signalling system0
Formalization of Android Activity-Fragment Multitasking Mechanism and Static Analysis of Mobile Apps0
Rooted Divergence-Preserving Branching Bisimilarity is a Congruence for Guarded CCS0
Introduction to the Special Section on FM 20210
Integration of Formal Proof into Unified Assurance Cases with Isabelle/SACM0
Multi-objective ω-Regular Reinforcement Learning0
Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter0
From generic partition refinement to weighted tree automata minimization0
From Non-punctuality to Non-adjacency: A Quest for Decidability of Timed Temporal Logics with Quantifiers0
Introduction to the Special Collection from FASE 20210
Exploring Scalability of BFT Blockchain Protocols through Network Simulations0
Using Multi-dimensional Quorums for Optimal Resilience in Multi-resource Blockchains0
Explanatory Denotational Semantics for Complex Event Patterns0
Footprint Logic for Object-Oriented Components (extended paper)0
Hybrid dynamic logic institutions for event/data-based systems0
Principles of Abstract Interpretation0
Denotational semantics of channel mobility in UTP-CSP0
Language Family Engineering with Product Lines of Multi-level Models0
Analysing an autonomous tramway positioning system with the Uppaal Statistical Model Checker0
Benchmarking Combinations of Learning and Testing Algorithms for Automata Learning0
Review of Formal Methods: An Appetizer0
A Deep Reinforcement Learning Framework with Formal Verification0
Efficient data validation for geographical interlocking systems0
A Survey of Practical Formal Methods for Security0
Compositional Analysis of Probabilistic Timed Graph Transformation Systems0
Formal Methods in Industry0
Review on Functional Algorithms, Verified!0
Editorial0
On Lexicographic Proof Rules for Probabilistic Termination0
Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover0
Introduction to the Special Collection from iFM 20220
L∗-based learning of Markov decision processes (extended version)0
Editorial0
An axiomatic approach to existence and liveness for differential equations0
Celebrating Rance. Walter Rance Cleaveland II: July 18, 1961 - March 27, 2024. An Obituary0
A Calculus for the Specification, Design, and Verification of Distributed Concurrent Systems0
Empirical Architecture Comparison of Two-input Machine Learning Systems for Vision Tasks0
Counterexample-guided inductive synthesis for probabilistic systems0
Drawing with SAT: four methods and A tool for producing railway infrastructure schematics0
Practical Modelling with Bigraphs0
Special Collection on Computer Science Education0
Review of Understanding Programming Languages0
Termination and Expressiveness of Execution Strategies for Networks of Bidirectional Model Transformations0
Modeling and Verification of Natural Language Requirements based on States and Modes0
The Concept of Class Invariant in Object-oriented Programming0
Automated Generation of Modular Assurance Cases with the System Assurance Reference Model0
A tale of two graph models: a case study in wireless sensor networks0
Review on Verified Functional Programming in Agda0
Reasoning About Exceptional Behavior At the Level of Java Bytecode with ByteBack0
Mechanised Safety Verification for a Distributed Autonomous Railway Control System0
SDLV: Verification of Steering Angle Safety for Self-Driving Cars0
Symbolic execution formally explained0
Inferring Switched Nonlinear DynamicalSystems0
Modeling and analysis of communicating systems0
The Development and Deployment of Formal Methods in the UK0
Editorial0
Quantitative verification of Kalman filters0
Enhancing Robustness Verification for Deep Neural Networks via Symbolic Propagation0
SMT based parameter identifiable combination detection for non-linear continuous and hybrid dynamics0
Toward Verifying Cooperatively Scheduled Runtimes Using CSP0
GR(1)*: GR(1) specifications extended withexistential guarantees0
Canonical Automata for Persistent Linearizability - A Corrigendum0
Semantics of the probabilistic Lambda CalculusBy Dirk Draheim0
Exploiting augmented intelligence in the modeling of safety-critical autonomous systems0
0.039446115493774