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-08-01 to 2025-08-01.)

Article	Citations
Reachability of Koopman linearized systems using explicit kernel approximation and polynomial zonotope refinement	10
Preface of the special issue on the conference on Computer-Aided Verification 2020 and 2021	6
Abstraction Modulo Stability	6
Verification modulo theories	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	5
Linearization, model reduction and reachability in nonlinear odes	4
Symbolic encoding of LL(1) parsing and its applications	4
Extended bounded response LTL: a new safety fragment for efficient reactive synthesis	4
Distributed bounded model checking	4
Partial bounding for recursive function synthesis	3
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
Round- and context-bounded control of dynamic pushdown systems	2
Automatic WSTS-based repair and deadlock detection of parameterized systems	2
Dynamic dependability analysis of shuffle-exchange networks	2
(Un)Solvable loop analysis	2
Memory-efficient fixpoint computation	2

Stratified guarded first-order transition systems	2
Automatic proofs of memory deallocation for a Whiley-to-C Compiler	2
Mining of extended signal temporal logic specifications with ParetoLib 2.0	2
Bounded-memory runtime enforcement with probabilistic and performance analysis	2
Cut-off theorems for the PV-model	2
Termination of triangular polynomial loops	2
Preface of the special issue on the conference on formal methods in computer aided design 2018	2
Preface of the special issue on the static analysis symposium 2020 and 2022	2
Runtime verification of partially-synchronous distributed system	1
Hashing-based approximate counting of minimal unsatisfiable subsets	1
Compositional verification of priority systems using sharp bisimulation	1
From LTL to rLTL monitoring: improved monitorability through robust semantics	1
SMT-based verification of program changes through summary repair	1
Assumption-based Runtime Verification	1
Dissecting ltlsynt	1
Compositional runtime enforcement revisited	1
Porous invariants for linear systems	1
Preface for the formal methods in system design special issue on ‘Formal Methods 2021’	1
Certified SAT solving with GPU accelerated inprocessing	1
Concise outlines for a complex logic: a proof outline checker for TaDA	1
Incremental design-space model checking via reusable reachable state approximations	1
Construction of verifier combinations from off-the-shelf components	1
Information-flow interfaces	1
Specifiable robustness in reactive synthesis	1
SAT solving for variants of first-order subsumption	1
Introducing robust reachability	0
Achieving high coverage in hardware equivalence checking via concolic verification	0
Preface of the special issue on the Conference on Computer-Aided Verification 2022	0
Software doping analysis for human oversight	0
Variable automata over infinite alphabets	0
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)	0
A verified durable transactional mutex lock for persistent x86-TSO	0
Data-driven invariant learning for probabilistic programs	0
Edmund Melson Clarke, Jr. (1945–2020)	0
Bridging the gap between single- and multi-model predictive runtime verification	0
Correction: (Un)Solvable loop analysis	0
Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker	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
Functional synthesis via input–output separation	0
An input–output relational domain for algebraic data types and functional arrays	0
Equivalence checking and intersection of deterministic timed finite state machines	0
Runtime verification of real-time event streams using the tool HStriver	0
Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking	0
Partial program analysis for staged compilation systems	0
Correction: Parameterized verification of leader/follower systems via first-order temporal logic	0
Machine learning and logic: a new frontier in artificial intelligence	0
Church synthesis on register automata over linearly ordered data domains	0
The hexatope and octatope abstract domains for neural network verification	0

Stochastic games with lexicographic objectives	0
Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations	0
Colored nested words	0
From LTL to unambiguous Büchi automata via disambiguation of alternating automata	0
Timed causal fanin analysis for symbolic simulation	0
Golem: a flexible and efficient solver for constrained Horn clauses	0
Parameter synthesis for Markov models: covering the parameter space	0
Finite-trace and generalized-reactivity specifications in temporal synthesis	0
Control strategies for off-line testing of timed systems	0
Mining definitions in Kissat with Kittens	0
Special Issue on Syntax-Guided Synthesis Preface	0
Relational abstract interpretation of arrays in assembly code	0
PAC statistical model checking of mean payoff in discrete- and continuous-time MDP	0
Memory access protocols: certified data-race freedom for GPU kernels	0
Rounding meets approximate model counting	0
Extending rely-guarantee thinking to handle real-time scheduling	0
Distributed parametric model checking timed automata under non-Zenoness assumption	0
Automated repair for timed systems	0
A scalable entropy estimator	0
Preface for the formal methods in system design special issue on SYNT 2021	0
Vacuity in synthesis	0
Hypercontracts	0
On multi-language abstraction: Towards a static analysis of multi-language programs	0
Global guidance for local generalization in model checking	0
Predicate abstraction for hyperliveness verification	0
Debug-localize-repair: a symbiotic construction for heap manipulations	0
Automatic assume-guarantee reasoning for safety and liveness using passive learning	0
Fingerprinting and analysis of Bluetooth devices with automata learning	0