Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers
Abstract elided by the publisher.
2,069 papers · page 60 of 104
Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints
Abstract elided by the publisher.
MCMAS: A Model Checker for the Verification of Multi-Agent Systems
Abstract elided by the publisher.
Reducing Test Inputs Using Information Partitions
Abstract elided by the publisher.
Generalizing DPLL to Richer Logics
Abstract elided by the publisher.
On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure
We consider the decision problem for quantifier-free formulas whose atoms are linear inequalities interpreted over the reals or rationals. This problem may be decided using satisfiability modulo theory (SMT), using a mixture of a SAT solver and a simplex-based decision procedure …
TASS: Timing Analyzer of Scenario-Based Specifications
Abstract elided by the publisher.
Cardinality Abstraction for Declarative Networking Applications
Abstract elided by the publisher.
Translation Validation: From Simulink to C
Translation validation is a technique for formally establishing the semantic equivalence of the source and the target of a code generator. In this work we present a translation validation tool for the Real-Time Workshop code generator that receives as input Simulink models and ge…
Component-Based Construction of Real-Time Systems in BIP
Abstract elided by the publisher.
VS3: SMT Solvers for Program Verification
Abstract elided by the publisher.
Regression Verification: Proving the Equivalence of Similar Programs
Abstract elided by the publisher.
PAT: Towards Flexible Verification under Fairness
Abstract elided by the publisher.
Reducing Context-Bounded Concurrent Reachability to Sequential Reachability
Abstract elided by the publisher.
Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences
Abstract elided by the publisher.
A Concurrent Portfolio Approach to SMT Solving
Abstract elided by the publisher.
Monotonic Abstraction for Programs with Dynamic Memory Heaps
Abstract elided by the publisher.
Ranking Automata and Games for Prioritized Requirements
Abstract elided by the publisher.
The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis
Abstract elided by the publisher.
Implied Set Closure and Its Application to Memory Consistency Verification
Abstract elided by the publisher.