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

Article	Citations
Preface for the formal methods in system design special issue on SYNT 2021	23
Special Issue on Syntax-Guided Synthesis Preface	9
An input–output relational domain for algebraic data types and functional arrays	6
Specifiable robustness in reactive synthesis	6
Finite-trace and generalized-reactivity specifications in temporal synthesis	5
Dissecting ltlsynt	5
Bridging the gap between single- and multi-model predictive runtime verification	4
Certifying proofs for SAT-based model checking	4
Automated repair for timed systems	4
SMT-based verification of program changes through summary repair	3
Preface of the special issue on the conference on Computer-Aided Verification 2020 and 2021	3
Partial bounding for recursive function synthesis	3
Data-driven invariant learning for probabilistic programs	3
Synbit: synthesizing bidirectional programs using unidirectional sketches	3
A verified durable transactional mutex lock for persistent x86-TSO	3
Abstraction Modulo Stability	3
Assumption-based Runtime Verification	2
Verification modulo theories	2
Church synthesis on register automata over linearly ordered data domains	2
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification	2
The hexatope and octatope abstract domains for neural network verification	2
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)	2
Automatic proofs of memory deallocation for a Whiley-to-C Compiler	2
Control strategies for off-line testing of timed systems	2
Runtime verification of partially-synchronous distributed system	2

Reachability of Koopman linearized systems using explicit kernel approximation and polynomial zonotope refinement	2
2018 CAV award	2
LTL model checking of self modifying code	2
Extending rely-guarantee thinking to handle real-time scheduling	2
Enhancing active model learning with equivalence checking using simulation relations	2
Preface for the formal methods in system design special issue on ‘Formal Methods 2021’	2
Software doping analysis for human oversight	1
Memory access protocols: certified data-race freedom for GPU kernels	1
A relational shape abstract domain	1
Preface of the special issue on the conference on computer-aided verification 2018	1
On multi-language abstraction: Towards a static analysis of multi-language programs	1
Termination of triangular polynomial loops	1
Stratified guarded first-order transition systems	1
Parameterized verification of leader/follower systems via first-order temporal logic	1
Machine learning and logic: a new frontier in artificial intelligence	1
Extended bounded response LTL: a new safety fragment for efficient reactive synthesis	1
Introducing robust reachability	1
Integrating ADTs in KeY and their application to history-based reasoning about collection	1
Incremental design-space model checking via reusable reachable state approximations	1
Cut-off theorems for the PV-model	1
Distributed parametric model checking timed automata under non-Zenoness assumption	1
Parameter synthesis for Markov models: covering the parameter space	1
Round- and context-bounded control of dynamic pushdown systems	1
Colored nested words	1
Runtime verification of real-time event streams using the tool HStriver	1
Equivalence checking and intersection of deterministic timed finite state machines	1
Formally understanding Rust’s ownership and borrowing system at the memory level	0
Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic	0
Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations	0
Fingerprinting and analysis of Bluetooth devices with automata learning	0
Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking	0
Bounded-memory runtime enforcement with probabilistic and performance analysis	0
Preface for the Formal Methods in System Design special issue on ‘FASE 2022’	0
Correction: (Un)Solvable loop analysis	0
Towards efficient verification of population protocols	0
Divider verification using symbolic computer algebra and delayed don’t care optimization: theory and practical implementation	0
Construction of verifier combinations from off-the-shelf components	0
Distributed bounded model checking	0
Dynamic dependability analysis of shuffle-exchange networks	0
Formal methods: practical applications and foundations	0
Concise outlines for a complex logic: a proof outline checker for TaDA	0
From LTL to unambiguous Büchi automata via disambiguation of alternating automata	0
Global guidance for local generalization in model checking	0
Mining of extended signal temporal logic specifications with ParetoLib 2.0	0
Golem: a flexibile and efficient solver for constrained Horn clauses	0
PAC statistical model checking of mean payoff in discrete- and continuous-time MDP	0
The complexity gap in the static analysis of cache accesses grows if procedure calls are added	0
Debug-localize-repair: a symbiotic construction for heap manipulations	0
Partial program analysis for staged compilation systems	0
Rely-guarantee bound analysis of parameterized concurrent shared-memory programs	0

Hashing-based approximate counting of minimal unsatisfiable subsets	0
SAT solving for variants of first-order subsumption	0
A scalable entropy estimator	0
Symbolic encoding of LL(1) parsing and its applications	0
Faster algorithms for quantitative verification in bounded treewidth graphs	0
Correction: Parameterized verification of leader/follower systems via first-order temporal logic	0
Functional synthesis via input–output separation	0
The probabilistic termination tool amber	0
On monitoring linear temporal properties	0
Compositional verification of priority systems using sharp bisimulation	0
Certified SAT solving with GPU accelerated inprocessing	0
Porous invariants for linear systems	0
Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker	0
Vacuity in synthesis	0
Preface of the special issue on the Conference on Computer-Aided Verification 2022	0
Compositional runtime enforcement revisited	0
Information-flow control on ARM and POWER multicore processors	0
Achieving high coverage in hardware equivalence checking via concolic verification	0
(Un)Solvable loop analysis	0
Reluplex: a calculus for reasoning about deep neural networks	0
Preface of the special issue on the conference on formal methods in computer aided design 2018	0
From LTL to rLTL monitoring: improved monitorability through robust semantics	0
Edmund Melson Clarke, Jr. (1945–2020)	0
Temporal prophecy for proving temporal properties of infinite-state systems	0
Towards neural-network-guided program synthesis and verification	0
Mining definitions in Kissat with Kittens	0
Stochastic games with lexicographic objectives	0
Information-flow interfaces	0
Relational abstract interpretation of arrays in assembly code	0