Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement
Abstract elided by the publisher.
2,069 papers · page 50 of 104
Delayed Continuous-Time Markov Chains for Genetic Regulatory Circuits
Abstract elided by the publisher.
On Decidability of Prebisimulation for Timed Automata
Abstract elided by the publisher.
Synchronisation- and Reversal-Bounded Analysis of Multithreaded Programs with Counters
Abstract elided by the publisher.
When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way
Abstract elided by the publisher.
Secure Programming via Visibly Pushdown Safety Games
Abstract elided by the publisher.
Incremental, Inductive CTL Model Checking
Abstract elided by the publisher.
Exercises in Nonstandard Static Analysis of Hybrid Systems
Abstract elided by the publisher.
Hector: An Equivalence Checker for a Higher-Order Fragment of ML
Abstract elided by the publisher.
TRACER: A Symbolic Execution Tool for Verification
Abstract elided by the publisher.
Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking
Statistical model checking avoids the exponential growth of states associated with probabilistic model checking by estimating probabilities from multiple executions of a system and by giving results within confidence bounds. Rare properties are often important but pose a particul…
Lock Removal for Concurrent Trace Programs
Abstract elided by the publisher.
APEX: An Analyzer for Open Probabilistic Programs
Abstract elided by the publisher.
Assume-Guarantee Abstraction Refinement for Probabilistic Systems
We describe an automated technique for assume-guarantee style checking of strong simulation between a system and a specification, both expressed as non-deterministic Labeled Probabilistic Transition Systems (LPTSes). We first characterize counterexamples to strong simulation as s…
Automatic Quantification of Cache Side-Channels
Abstract elided by the publisher.
Deterministic Automata for the (F, G)-Fragment of LTL
When dealing with linear temporal logic properties in the setting of e.g. games or probabilistic systems, one often needs to express them as deterministic omega-automata. In order to translate LTL to deterministic omega-automata, the traditional approach first translates the form…
SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs
Abstract elided by the publisher.
A Solver for Reachability Modulo Theories
Abstract elided by the publisher.
Termination Analysis with Algorithmic Learning
Abstract elided by the publisher.
An Axiomatic Memory Model for POWER Multiprocessors
Abstract elided by the publisher.