Entity usage

This page lists pages that use the given entity (e.g. Q42). The list is sorted by descending page ID, so that newer pages are listed first.

Showing below up to 50 results in range #1 to #50.

A verified durable transactional mutex lock for persistent x86-TSO: Label: en
Formally understanding Rust's ownership and borrowing system at the memory level: Label: en
The hexatope and octatope abstract domains for neural network verification: Label: en
Runtime verification of partially-synchronous distributed system: Label: en
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification: Label: en
Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker: Label: en
Distributed bounded model checking: Label: en
Extended bounded response LTL: a new safety fragment for efficient reactive synthesis: Label: en
Porous invariants for linear systems: Label: en
Introducing robust reachability: Label: en
Partial bounding for recursive function synthesis: Label: en
Memory access protocols: certified data-race freedom for GPU kernels: Label: en
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version): Label: en
Global guidance for local generalization in model checking: Label: en
Stochastic games with lexicographic objectives: Label: en
Hashing-based approximate counting of minimal unsatisfiable subsets: Label: en
Preface of the special issue on the conference on computer-aided verification 2020 and 2021: Label: en
Dynamic dependability analysis of shuffle-exchange networks: Label: en
Mining of extended signal temporal logic specifications with ParetoLib 2.0: Label: en
Parameter synthesis for Markov models: covering the parameter space: Label: en
Bounded-memory runtime enforcement with probabilistic and performance analysis: Label: en
Extending rely-guarantee thinking to handle real-time scheduling: Label: en
Certified SAT solving with GPU accelerated inprocessing: Label: en
Round- and context-bounded control of dynamic pushdown systems: Label: en
Compositional verification of priority systems using sharp bisimulation: Label: en
Integrating ADTs in KeY and their application to history-based reasoning about collection: Label: en
Fingerprinting and analysis of Bluetooth devices with automata learning: Label: en
Runtime verification of real-time event streams using the tool HStriver: Label: en
Preface for the formal methods in system design special issue on `Formal Methods 2021': Label: en
Symbolic encoding of LL(1) parsing and its applications: Label: en
Church synthesis on register automata over linearly ordered data domains: Label: en
Dissecting \texttt{ltlsynt}: Label: en
\textsc{Synbit}: synthesizing bidirectional programs using unidirectional sketches: Label: en
Enhancing active model learning with equivalence checking using simulation relations: Label: en
Finite-trace and generalized-reactivity specifications in temporal synthesis: Label: en
Preface for the formal methods in system design special issue on SYNT 2021: Label: en
Concise outlines for a complex logic: a proof outline checker for TaDA: Label: en
The probabilistic termination tool amber: Label: en
Reluplex: a calculus for reasoning about deep neural networks: Label: en
Static detection of uncoalesced accesses in GPU programs: Label: en
Distributed parametric model checking timed automata under non-zenoness assumption: Label: en
Compositional runtime enforcement revisited: Label: en
From LTL to rLTL monitoring: improved monitorability through robust semantics: Label: en
Automated repair for timed systems: Label: en
Relational abstract interpretation of arrays in assembly code: Label: en
Equivalence checking and intersection of deterministic timed finite state machines: Label: en
Bridging the gap between single- and multi-model predictive runtime verification: Label: en
Cut-off theorems for the \textit{PV}-model: Label: en
The complexity gap in the static analysis of cache accesses grows if procedure calls are added: Label: en
Correction to: ``Parameterized verification of leader/follower systems via first-order temporal logic: Label: en