Bounded Synthesis for Streett, Rabin, and \text CTL^*
Abstract elided by the publisher.
26,098 papers · page 455 of 1,305
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
Abstract elided by the publisher.
Cutoff Bounds for Consensus Algorithms
Abstract elided by the publisher.
Synchronization Synthesis for Network Programs
Abstract elided by the publisher.
A Correct-by-Decision Solution for Simultaneous Place and Route
Abstract elided by the publisher.
Markov Automata with Multiple Objectives
Abstract elided by the publisher.
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification
Abstract elided by the publisher.
STLInspector: STL Validation with Guarantees
Abstract elided by the publisher.
Minimization of Symbolic Transducers
Abstract elided by the publisher.
Runtime Monitoring with Recovery of the SENT Communication Protocol
Abstract elided by the publisher.
Maximum Satisfiability in Software Analysis: Applications and Techniques
Abstract elided by the publisher.
E-QED: Electrical Bug Localization During Post-silicon Validation Enabled by Quick Error Detection and Formal Methods
During post-silicon validation, manufactured integrated circuits are extensively tested in actual system environments to detect design bugs. Bug localization involves identification of a bug trace (a sequence of inputs that activates and detects the bug) and a hardware design blo…
Abstract Interpretation with Unfoldings
We present and evaluate a technique for computing path-sensitive interference conditions during abstract interpretation of concurrent programs. In lieu of fixed point computation, we use prime event structures to compactly represent causal dependence and interference between sequ…
On Expansion and Resolution in CEGAR Based QBF Solving
A quantified Boolean formula (QBF) is a propositional formula extended with universal and existential quantification over propositions. There are two methodologies in CEGAR based QBF solving techniques, one that is based on a refinement loop that builds partial expansions and a m…
Ascertaining Uncertainty for Efficient Exact Cache Analysis
Abstract elided by the publisher.
Model Counting for Recursively-Defined Strings
Abstract elided by the publisher.
Montre: A Tool for Monitoring Timed Regular Expressions
We present Montre, a monitoring tool to search patterns specified by timed regular expressions over real-time behaviors. We use timed regular expressions as a compact, natural, and highly-expressive pattern specification language for monitoring applications involving quantitative…
Automating Induction for Solving Horn Clauses
Verification problems of programs in various paradigms can be reduced to problems of solving Horn clause constraints on predicate variables that represent unknown inductive invariants. This paper presents a novel Horn constraint solving method based on inductive theorem proving: …
Program Verification Under Weak Memory Consistency Using Separation Logic
Abstract elided by the publisher.
Logical Clustering and Learning for Time-Series Data
In order to effectively analyze and build cyberphysical systems (CPS), designers today have to combat the data deluge problem, i.e., the burden of processing intractably large amounts of data produced by complex models and experiments. In this work, we utilize monotonic parametri…