OOIR: Observatory of International Research

Papers

(The median citation count of Formal Methods in System Design 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-09-01 to 2025-09-01.)

Article	Citations
Preface of the special issue on the conference on Computer-Aided Verification 2020 and 2021	11
Verification modulo theories	6
Reachability of Koopman linearized systems using explicit kernel approximation and polynomial zonotope refinement	6
Parameterized verification of leader/follower systems via first-order temporal logic	6
Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs	6
Abstraction Modulo Stability	6
Linearization, model reduction and reachability in nonlinear odes	5
Symbolic encoding of LL(1) parsing and its applications	4
Distributed bounded model checking	4
Extended bounded response LTL: a new safety fragment for efficient reactive synthesis	4
The complexity gap in the static analysis of cache accesses grows if procedure calls are added	3
Preface for the Formal Methods in System Design special issue on ‘FASE 2022’	3
LTL model checking of self modifying code	3
The probabilistic termination tool amber	3
Towards neural-network-guided program synthesis and verification	3
Enhancing active model learning with equivalence checking using simulation relations	3
Divider verification using symbolic computer algebra and delayed don’t care optimization: theory and practical implementation	3
On monitoring linear temporal properties	3
Synbit: synthesizing bidirectional programs using unidirectional sketches	3
Partial bounding for recursive function synthesis	3
Preface of the special issue on the static analysis symposium 2020 and 2022	2
SAT solving for variants of first-order subsumption	2
Cut-off theorems for the PV-model	2
Termination of triangular polynomial loops	2
Memory-efficient fixpoint computation	2

(Un)Solvable loop analysis	2
Dynamic dependability analysis of shuffle-exchange networks	2
Round- and context-bounded control of dynamic pushdown systems	2
Automatic WSTS-based repair and deadlock detection of parameterized systems	2
Mining of extended signal temporal logic specifications with ParetoLib 2.0	2
Certified SAT solving with GPU accelerated inprocessing	2
Stratified guarded first-order transition systems	2
Bounded-memory runtime enforcement with probabilistic and performance analysis	2
Concise outlines for a complex logic: a proof outline checker for TaDA	1
Dissecting ltlsynt	1
From LTL to rLTL monitoring: improved monitorability through robust semantics	1
Compositional runtime enforcement revisited	1
Porous invariants for linear systems	1
Runtime verification of partially-synchronous distributed system	1
Specifiable robustness in reactive synthesis	1
Preface for the formal methods in system design special issue on ‘Formal Methods 2021’	1
Construction of verifier combinations from off-the-shelf components	1
Information-flow interfaces	1
SMT-based verification of program changes through summary repair	1
Assumption-based Runtime Verification	1
Hashing-based approximate counting of minimal unsatisfiable subsets	1
Compositional verification of priority systems using sharp bisimulation	1
Incremental design-space model checking via reusable reachable state approximations	1
Debug-localize-repair: a symbiotic construction for heap manipulations	0
On multi-language abstraction: Towards a static analysis of multi-language programs	0
Golem: a flexible and efficient solver for constrained Horn clauses	0
Predicate abstraction for hyperliveness verification	0
Awaiting for Godot: stateless model checking that avoids executions where nothing happens	0
Automatic assume-guarantee reasoning for safety and liveness using passive learning	0
Vacuity in synthesis	0
Introducing robust reachability	0
Extending rely-guarantee thinking to handle real-time scheduling	0
Achieving high coverage in hardware equivalence checking via concolic verification	0
Memory access protocols: certified data-race freedom for GPU kernels	0
Preface of the special issue on the Conference on Computer-Aided Verification 2022	0
Automated repair for timed systems	0
A scalable entropy estimator	0
Variable automata over infinite alphabets	0
Finite-trace and generalized-reactivity specifications in temporal synthesis	0
Correction: Hypercontracts	0
Correction: (Un)Solvable loop analysis	0
Bridging the gap between single- and multi-model predictive runtime verification	0
Integrating ADTs in KeY and their application to history-based reasoning about collection	0
Formally understanding Rust’s ownership and borrowing system at the memory level	0
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification	0
Hypercontracts	0
Special Issue on Syntax-Guided Synthesis Preface	0
Equivalence checking and intersection of deterministic timed finite state machines	0
Partial program analysis for staged compilation systems	0
Runtime verification of real-time event streams using the tool HStriver	0

Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)	0
Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking	0
Software doping analysis for human oversight	0
Stochastic games with lexicographic objectives	0
Correction: Parameterized verification of leader/follower systems via first-order temporal logic	0
Colored nested words	0
Distributed parametric model checking timed automata under non-Zenoness assumption	0
Church synthesis on register automata over linearly ordered data domains	0
Functional synthesis via input–output separation	0
Timed causal fanin analysis for symbolic simulation	0
Global guidance for local generalization in model checking	0
Parameter synthesis for Markov models: covering the parameter space	0
From LTL to unambiguous Büchi automata via disambiguation of alternating automata	0
Control strategies for off-line testing of timed systems	0
Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker	0
Mining definitions in Kissat with Kittens	0
An input–output relational domain for algebraic data types and functional arrays	0
Machine learning and logic: a new frontier in artificial intelligence	0
Relational abstract interpretation of arrays in assembly code	0
The hexatope and octatope abstract domains for neural network verification	0
PAC statistical model checking of mean payoff in discrete- and continuous-time MDP	0
Data-driven invariant learning for probabilistic programs	0
Fingerprinting and analysis of Bluetooth devices with automata learning	0
Rounding meets approximate model counting	0
Edmund Melson Clarke, Jr. (1945–2020)	0
A verified durable transactional mutex lock for persistent x86-TSO	0
Preface for the formal methods in system design special issue on SYNT 2021	0