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 2020-03-01 to 2024-03-01.)

Article	Citations
Reluplex: a calculus for reasoning about deep neural networks	18
Automatic verification of concurrent stochastic systems	11
Boolean functional synthesis: hardness and practical algorithms	6
Debug-localize-repair: a symbiotic construction for heap manipulations	5
Distributed bounded model checking	5
SAT modulo discrete event simulation applied to railway design capacity analysis	5
Gray-box monitoring of hyperproperties with an application to privacy	4
Abstraction and subsumption in modular verification of C programs	4
Integrating formal specifications into applications: the ProB Java API	4
Temporal prophecy for proving temporal properties of infinite-state systems	3
On solving quantified bit-vector constraints using invertibility conditions	3
Compositional verification of concurrent systems by combining bisimulations	3
Multi-scale verification of distributed synchronisation	3
Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker	2
Faster algorithms for quantitative verification in bounded treewidth graphs	2
Learning inductive invariants by sampling from frequency distributions	2
A relational shape abstract domain	2
Bridging the gap between single- and multi-model predictive runtime verification	2
Pegasus: sound continuous invariant generation	2
Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic	2
Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations	2
Static detection of uncoalesced accesses in GPU programs	2
Model checking boot code from AWS data centers	2
Mining definitions in Kissat with Kittens	2
Rely-guarantee bound analysis of parameterized concurrent shared-memory programs	2

Symbolic encoding of LL(1) parsing and its applications	2
Equivalence checking and intersection of deterministic timed finite state machines	2
Certifying proofs for SAT-based model checking	2
Stochastic games with lexicographic objectives	1
Quasi-optimal partial order reduction	1
Integrating ADTs in KeY and their application to history-based reasoning about collection	1
Stratified guarded first-order transition systems	1
Control strategies for off-line testing of timed systems	1
SMT-based verification of program changes through summary repair	1
Preface of the special issue on the conference on formal methods in computer aided design 2018	1
The complexity gap in the static analysis of cache accesses grows if procedure calls are added	1
Introducing robust reachability	1
Markov automata with multiple objectives	1
LTL model checking of self modifying code	1
Compositional runtime enforcement revisited	1
Vacuity in synthesis	1
Exact quantitative probabilistic model checking through rational search	1
Extended bounded response LTL: a new safety fragment for efficient reactive synthesis	1
Assumption-based Runtime Verification	1
Formal methods: practical applications and foundations	0
2018 CAV award	0
The probabilistic termination tool amber	0
Abstraction refinement and antichains for trace inclusion of infinite state systems	0
Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking	0
Extending rely-guarantee thinking to handle real-time scheduling	0
Towards efficient verification of population protocols	0
Synbit: synthesizing bidirectional programs using unidirectional sketches	0
Functional synthesis via input–output separation	0
Automated repair for timed systems	0
Termination of triangular polynomial loops	0
Incremental design-space model checking via reusable reachable state approximations	0
Cut-off theorems for the PV-model	0
On monitoring linear temporal properties	0
Church synthesis on register automata over linearly ordered data domains	0
Global guidance for local generalization in model checking	0
Parameterized verification of leader/follower systems via first-order temporal logic	0
From LTL to unambiguous Büchi automata via disambiguation of alternating automata	0
Distributed parametric model checking timed automata under non-Zenoness assumption	0
Relational abstract interpretation of arrays in assembly code	0
Automated repair by example for firewalls	0
Fingerprinting and analysis of Bluetooth devices with automata learning	0
Memory access protocols: certified data-race freedom for GPU kernels	0
Bounded-memory runtime enforcement with probabilistic and performance analysis	0
Finite-trace and generalized-reactivity specifications in temporal synthesis	0
Information-flow control on ARM and POWER multicore processors	0
Preface for the formal methods in system design special issue on SYNT 2021	0
Preface of the special issue on the Conference on Formal Methods in Computer-Aided Design 2017	0
Specifiable robustness in reactive synthesis	0
On multi-language abstraction: Towards a static analysis of multi-language programs	0
Colored nested words	0

Round- and context-bounded control of dynamic pushdown systems	0
Achieving high coverage in hardware equivalence checking via concolic verification	0
Machine learning and logic: a new frontier in artificial intelligence	0
Certified SAT solving with GPU accelerated inprocessing	0
Verification modulo theories	0
Compositional verification of priority systems using sharp bisimulation	0
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)	0
Correction: Parameterized verification of leader/follower systems via first-order temporal logic	0
Automatic proofs of memory deallocation for a Whiley-to-C Compiler	0
Edmund Melson Clarke, Jr. (1945–2020)	0
Preface for the formal methods in system design special issue on ‘Formal Methods 2021’	0
Hashing-based approximate counting of minimal unsatisfiable subsets	0
Dissecting ltlsynt	0
Static analysis for detecting high-level races in RTOS kernels	0
Special Issue on Syntax-Guided Synthesis Preface	0
Runtime verification of real-time event streams using the tool HStriver	0
Partial bounding for recursive function synthesis	0
Preface of the special issue on the conference on computer-aided verification 2018	0
From LTL to rLTL monitoring: improved monitorability through robust semantics	0
Porous invariants for linear systems	0
Enhancing active model learning with equivalence checking using simulation relations	0
Concise outlines for a complex logic: a proof outline checker for TaDA	0
Parameter synthesis for Markov models: covering the parameter space	0
Formal methods: practical applications and foundations	0
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification	0