SPeeDI - A Verification Tool for Polygonal Hybrid Systems
Abstract elided by the publisher.
2,069 papers · page 76 of 104
Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking
Abstract elided by the publisher.
Symbolic Localization Reduction with Reconstruction Layering and Backtracking
Abstract elided by the publisher.
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT
Abstract elided by the publisher.
Property Checking via Structural Analysis
Abstract elided by the publisher.
PathFinder: A Tool for Design Exploration
Abstract elided by the publisher.
Semi-formal Bounded Model Checking
Abstract elided by the publisher.
State Space Reduction by Proving Confluence
Abstract elided by the publisher.
Extrapolating Tree Transformations
Abstract elided by the publisher.
IF-2.0: A Validation Environment for Component-Based Real-Time Systems
Abstract elided by the publisher.
Algorithmic Verification of Invalidation-Based Protocols
Abstract elided by the publisher.
Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions
Abstract elided by the publisher.
Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification
Abstract elided by the publisher.
Interface Compatibility Checking for Software Modules
Abstract elided by the publisher.
Synchronous and Bidirectional Component Interfaces
Abstract elided by the publisher.
Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking
Abstract elided by the publisher.
chi-Chek: A Multi-valued Model-Checker
Abstract elided by the publisher.
Automated Unbounded Verification of Security Protocols
Abstract elided by the publisher.
NuSMV 2: An OpenSource Tool for Symbolic Model Checking
Abstract elided by the publisher.
SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques
We describe new techniques for model checking in the counterexample guided abstraction/refinement framework. The abstraction phase ‘hides’ the logic of various variables, hence considering them as inputs. This type of abstraction may lead to ‘spurious’ counterexamples, i.e. trace…