Markov Automata with Multiple Objectives
Abstract elided by the publisher.
2,069 papers · page 35 of 104
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…
Compositional Model Checking with Incremental Counter-Example Construction
Abstract elided by the publisher.
Starling: Lightweight Concurrency Verification with Views
Abstract elided by the publisher.
Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses
Abstract elided by the publisher.
Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution
In permission logics such as separation logic, the iterated separating conjunction is a quantifier denoting access permission to an unbounded set of heap locations. In contrast to recursive predicates, iterated separating conjunctions do not prescribe a structure on the locations…
Stateless Model Checking for POWER
We present the first framework for efficient application of stateless model checking (SMC) to programs running under the relaxed memory model of POWER. The framework combines several contributions. The first contribution is that we develop a scheme for systematically deriving ope…