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

Article	Citations
Preface of the special issue on the conference on Computer-Aided Verification 2020 and 2021	14
Abstraction Modulo Stability	7
Reachability of Koopman linearized systems using explicit kernel approximation and polynomial zonotope refinement	7
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
Symbolic encoding of LL(1) parsing and its applications	6
Verification modulo theories	6
The probabilistic termination tool amber	5
Preface for the Formal Methods in System Design special issue on ‘FASE 2022’	4
On monitoring linear temporal properties	4
Towards neural-network-guided program synthesis and verification	4
Divider verification using symbolic computer algebra and delayed don’t care optimization: theory and practical implementation	4
Synbit: synthesizing bidirectional programs using unidirectional sketches	3
Round- and context-bounded control of dynamic pushdown systems	3
Partial bounding for recursive function synthesis	3
Enhancing active model learning with equivalence checking using simulation relations	3
Memory-efficient fixpoint computation	3
Bounded-memory runtime enforcement with probabilistic and performance analysis	2
Mining of extended signal temporal logic specifications with ParetoLib 2.0	2
Stratified guarded first-order transition systems	2
Formalization of robot collision detection method based on conformal geometric algebra	2
(Un)Solvable loop analysis	2
Termination of triangular polynomial loops	2
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
Certified SAT solving with GPU accelerated inprocessing	1
Preface for the formal methods in system design special issue on ‘Formal Methods 2021’	1
Hashing-based approximate counting of minimal unsatisfiable subsets	1
Mining definitions in Kissat with Kittens	1
Runtime verification of partially-synchronous distributed system	1
Symbolic computer algebra for multipliers revisited - demonstrating the significance of order and phase optimization	1
SAT solving for variants of first-order subsumption	1
SMT-based verification of program changes through summary repair	1
Construction of verifier combinations from off-the-shelf components	1
Porous invariants for linear systems	1
Preserving provability over GPU program optimizations with annotation-aware transformations	1
Dynamic dependability analysis of shuffle-exchange networks	1
Concise outlines for a complex logic: a proof outline checker for TaDA	1
Formal methods for mobile ad hoc networks: a survey	1
Compositional verification of priority systems using sharp bisimulation	1
Information-flow interfaces	1
Dissecting ltlsynt	1
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification	0
A program instrumentation framework for automatic verification	0
An input–output relational domain for algebraic data types and functional arrays	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
Partial program analysis for staged compilation systems	0
Variable automata over infinite alphabets	0
The hexatope and octatope abstract domains for neural network verification	0
Rounding meets approximate model counting	0
Stochastic games with lexicographic objectives	0
Finite-trace and generalized-reactivity specifications in temporal synthesis	0
Edmund Melson Clarke, Jr. (1945–2020)	0
Formally understanding Rust’s ownership and borrowing system at the memory level	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
Automatic assume-guarantee reasoning for safety and liveness using passive learning	0
A scalable anytime algorithm for learning fragments of linear temporal logic	0
Correction: Hypercontracts	0
Correction: Parameterized verification of leader/follower systems via first-order temporal logic	0
Bounded satisfiability checking of $$\hbox {FOL}^*$$ formulas with aggregations	0
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)	0
Church synthesis on register automata over linearly ordered data domains	0
Machine learning and logic: a new frontier in artificial intelligence	0
Preface for the formal methods in system design special issue on SYNT 2021	0
Correction: (Un)Solvable loop analysis	0
Search and explore: symbiotic policy synthesis in POMDPs	0
Memory access protocols: certified data-race freedom for GPU kernels	0
Hypercontracts	0
Integrating ADTs in KeY and their application to history-based reasoning about collection	0
Predicate abstraction for hyperliveness verification	0
Verifying hybrid automata networks guided by task scenarios	0

Software doping analysis for human oversight	0
Runtime verification of real-time event streams using the tool HStriver	0
PAC statistical model checking of mean payoff in discrete- and continuous-time MDP	0
Modular analysis of distributed hybrid systems using post-regions	0
Extending rely-guarantee thinking to handle real-time scheduling	0
A verified durable transactional mutex lock for persistent x86-TSO	0
Data-driven invariant learning for probabilistic programs	0
Introducing robust reachability	0
Fingerprinting and analysis of Bluetooth devices with automata learning	0
Awaiting for Godot: stateless model checking that avoids executions where nothing happens	0
A scalable entropy estimator	0
Golem: a flexible and efficient solver for constrained Horn clauses	0
On multi-language abstraction: Towards a static analysis of multi-language programs	0