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

Article	Citations
Reachability of Koopman linearized systems using explicit kernel approximation and polynomial zonotope refinement	29
Preface of the special issue on the conference on Computer-Aided Verification 2020 and 2021	9
Verification modulo theories	6
Abstraction Modulo Stability	6
Extended bounded response LTL: a new safety fragment for efficient reactive synthesis	5
Parameterized verification of leader/follower systems via first-order temporal logic	5
The complexity gap in the static analysis of cache accesses grows if procedure calls are added	4
Symbolic encoding of LL(1) parsing and its applications	4
Divider verification using symbolic computer algebra and delayed don’t care optimization: theory and practical implementation	4
The probabilistic termination tool amber	4
Distributed bounded model checking	4
On monitoring linear temporal properties	3
2018 CAV award	3
Synbit: synthesizing bidirectional programs using unidirectional sketches	3
Partial bounding for recursive function synthesis	3
Preface for the Formal Methods in System Design special issue on ‘FASE 2022’	3
Towards neural-network-guided program synthesis and verification	3
Round- and context-bounded control of dynamic pushdown systems	2
Bounded-memory runtime enforcement with probabilistic and performance analysis	2
Mining of extended signal temporal logic specifications with ParetoLib 2.0	2
Enhancing active model learning with equivalence checking using simulation relations	2
Cut-off theorems for the PV-model	2
Automatic proofs of memory deallocation for a Whiley-to-C Compiler	2
Preface of the special issue on the conference on formal methods in computer aided design 2018	2
Automatic WSTS-based repair and deadlock detection of parameterized systems	2

Memory-efficient fixpoint computation	2
Stratified guarded first-order transition systems	2
Information-flow control on ARM and POWER multicore processors	2
Dynamic dependability analysis of shuffle-exchange networks	2
LTL model checking of self modifying code	2
Termination of triangular polynomial loops	2
(Un)Solvable loop analysis	1
Concise outlines for a complex logic: a proof outline checker for TaDA	1
SMT-based verification of program changes through summary repair	1
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
Dissecting ltlsynt	1
Certified SAT solving with GPU accelerated inprocessing	1
Preface for the formal methods in system design special issue on ‘Formal Methods 2021’	1
From LTL to rLTL monitoring: improved monitorability through robust semantics	1
Compositional runtime enforcement revisited	1
Assumption-based Runtime Verification	1
Preface of the special issue on the static analysis symposium 2020 and 2022	1
SAT solving for variants of first-order subsumption	1
Specifiable robustness in reactive synthesis	1
Incremental design-space model checking via reusable reachable state approximations	1
Construction of verifier combinations from off-the-shelf components	1
A scalable entropy estimator	0
Temporal prophecy for proving temporal properties of infinite-state systems	0
On multi-language abstraction: Towards a static analysis of multi-language programs	0
Machine learning and logic: a new frontier in artificial intelligence	0
Formally understanding Rust’s ownership and borrowing system at the memory level	0
Control strategies for off-line testing of timed systems	0
Golem: a flexible and efficient solver for constrained Horn clauses	0
Mining definitions in Kissat with Kittens	0
Fingerprinting and analysis of Bluetooth devices with automata learning	0
Introducing robust reachability	0
Achieving high coverage in hardware equivalence checking via concolic verification	0
PAC statistical model checking of mean payoff in discrete- and continuous-time MDP	0
Extending rely-guarantee thinking to handle real-time scheduling	0
Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations	0
The hexatope and octatope abstract domains for neural network verification	0
Preface for the formal methods in system design special issue on SYNT 2021	0
Data-driven invariant learning for probabilistic programs	0
Equivalence checking and intersection of deterministic timed finite state machines	0
Correction: (Un)Solvable loop analysis	0
Edmund Melson Clarke, Jr. (1945–2020)	0
A verified durable transactional mutex lock for persistent x86-TSO	0
Integrating ADTs in KeY and their application to history-based reasoning about collection	0
Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic	0
Debug-localize-repair: a symbiotic construction for heap manipulations	0
Parameter synthesis for Markov models: covering the parameter space	0
Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker	0
Porous invariants for linear systems	0

Software doping analysis for human oversight	0
Colored nested words	0
Formal methods: practical applications and foundations	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
Distributed parametric model checking timed automata under non-Zenoness assumption	0
Certifying proofs for SAT-based model checking	0
Church synthesis on register automata over linearly ordered data domains	0
Stochastic games with lexicographic objectives	0
Runtime verification of real-time event streams using the tool HStriver	0
Reluplex: a calculus for reasoning about deep neural networks	0
Vacuity in synthesis	0
Functional synthesis via input–output separation	0
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification	0
Global guidance for local generalization in model checking	0
Special Issue on Syntax-Guided Synthesis Preface	0
From LTL to unambiguous Büchi automata via disambiguation of alternating automata	0
Information-flow interfaces	0
An input–output relational domain for algebraic data types and functional arrays	0
Partial program analysis for staged compilation systems	0
Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking	0
Relational abstract interpretation of arrays in assembly code	0
Correction: Parameterized verification of leader/follower systems via first-order temporal logic	0
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)	0
Finite-trace and generalized-reactivity specifications in temporal synthesis	0
Automated repair for timed systems	0
Bridging the gap between single- and multi-model predictive runtime verification	0