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 2022-01-01 to 2026-01-01.)

Article	Citations
Preface of the special issue on the conference on Computer-Aided Verification 2020 and 2021	14
Abstraction Modulo Stability	7
Verification modulo theories	6
Linearization, model reduction and reachability in nonlinear odes	6
Editorial: Special issue on formal methods in computer-aided design	6
Bounded verification for finite-field-blasting in a compiler for zero knowledge proofs	6
Reachability of Koopman linearized systems using explicit kernel approximation and polynomial zonotope refinement	6
Distributed bounded model checking	5
The probabilistic termination tool amber	4
Preface for the Formal Methods in System Design special issue on ‘FASE 2022’	4
Divider verification using symbolic computer algebra and delayed don’t care optimization: theory and practical implementation	4
On monitoring linear temporal properties	4
Symbolic encoding of LL(1) parsing and its applications	4
Towards neural-network-guided program synthesis and verification	3
Synbit: synthesizing bidirectional programs using unidirectional sketches	3
Stratified guarded first-order transition systems	3
Enhancing active model learning with equivalence checking using simulation relations	3
Memory-efficient fixpoint computation	3
Termination of triangular polynomial loops	3
Partial bounding for recursive function synthesis	3
Round- and context-bounded control of dynamic pushdown systems	3
LTL model checking of self modifying code	3
Preface of the special issue on the static analysis symposium 2020 and 2022	2
Automatic WSTS-based repair and deadlock detection of parameterized systems	2
(Un)Solvable loop analysis	2

Dynamic dependability analysis of shuffle-exchange networks	2
Bounded-memory runtime enforcement with probabilistic and performance analysis	2
Preserving provability over GPU program optimizations with annotation-aware transformations	2
Formalization of robot collision detection method based on conformal geometric algebra	2
Mining of extended signal temporal logic specifications with ParetoLib 2.0	2
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
Formal methods for mobile ad hoc networks: a survey	1
Specifiable robustness in reactive synthesis	1
Dissecting ltlsynt	1
Concise outlines for a complex logic: a proof outline checker for TaDA	1
Hashing-based approximate counting of minimal unsatisfiable subsets	1
Certified SAT solving with GPU accelerated inprocessing	1
SMT-based verification of program changes through summary repair	1
Runtime verification of partially-synchronous distributed system	1
Assumption-based Runtime Verification	1
SAT solving for variants of first-order subsumption	1
Compositional verification of priority systems using sharp bisimulation	0
Mining definitions in Kissat with Kittens	0
Achieving high coverage in hardware equivalence checking via concolic verification	0
Correction: Parameterized verification of leader/follower systems via first-order temporal logic	0
Bounded satisfiability checking of $$\hbox {FOL}^*$$ formulas with aggregations	0
Data-driven invariant learning for probabilistic programs	0
Finite-trace and generalized-reactivity specifications in temporal synthesis	0
Golem: a flexible and efficient solver for constrained Horn clauses	0
Fingerprinting and analysis of Bluetooth devices with automata learning	0
Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker	0
Timed causal fanin analysis for symbolic simulation	0
Correction: Hypercontracts	0
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)	0
Parameter synthesis for Markov models: covering the parameter space	0
Control strategies for off-line testing of timed systems	0
Information-flow interfaces	0
On multi-language abstraction: Towards a static analysis of multi-language programs	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
Preface of the special issue on the Conference on Computer-Aided Verification 2022	0
Memory access protocols: certified data-race freedom for GPU kernels	0
Church synthesis on register automata over linearly ordered data domains	0
Variable automata over infinite alphabets	0
Stochastic games with lexicographic objectives	0
Awaiting for Godot: stateless model checking that avoids executions where nothing happens	0
Edmund Melson Clarke, Jr. (1945–2020)	0
Formally understanding Rust’s ownership and borrowing system at the memory level	0
Machine learning and logic: a new frontier in artificial intelligence	0
Introducing robust reachability	0
Predicate abstraction for hyperliveness verification	0
Automatic assume-guarantee reasoning for safety and liveness using passive learning	0
Porous invariants for linear systems	0
Extending rely-guarantee thinking to handle real-time scheduling	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
Rounding meets approximate model counting	0
Software doping analysis for human oversight	0
A verified durable transactional mutex lock for persistent x86-TSO	0
Hypercontracts	0
Correction: (Un)Solvable loop analysis	0
Global guidance for local generalization in model checking	0
A scalable entropy estimator	0
Functional synthesis via input–output separation	0
Partial program analysis for staged compilation systems	0
Integrating ADTs in KeY and their application to history-based reasoning about collection	0
Preface for the formal methods in system design special issue on SYNT 2021	0
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification	0
An input–output relational domain for algebraic data types and functional arrays	0