SLAM

swMATH3136MaRDI QIDQ15668FDOQ15668

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• Loop summarization using state and transition invariants
• Title not available (Why is that?)
• On the Satisfiability of Modular Arithmetic Formulae
• Computer Aided Verification
• Title not available (Why is that?)
• Title not available (Why is that?)
• Combining Model Checking and Data-Flow Analysis
• EUFORIA: complete software model checking with uninterpreted functions
• A saturation method for the modal \(\mu \)-calculus over pushdown systems
• Model Checking Software
• Verification, Model Checking, and Abstract Interpretation
• Static Analysis
• Static Analysis
• Title not available (Why is that?)
• Tools and Algorithms for the Construction and Analysis of Systems
• Runtime Verification Based on Register Automata
• From Under-Approximations to Over-Approximations and Back
• Solving games via three-valued abstraction refinement
• Algorithmic Analysis of Array-Accessing Programs
• Abstraction Refinement for Quantified Array Assertions
• Data structures for symbolic multi-valued model-checking
• Computer Aided Verification
• An Introduction to Practical Formal Methods Using Temporal Logic
• A model checking-based approach for security policy verification of mobile systems
• An integrated approach to high integrity software verification
• An extension of lazy abstraction with interpolation for programs with arrays
• Automatic decidability and combinability
• Context-aware counter abstraction
• Model Checking Software
• Dependent types from counterexamples
• Modular strategies for recursive game graphs
• Generating models of infinite-state communication protocols using regular inference with abstraction
• Behavioral interface specification languages
• Whale: An Interpolation-Based Algorithm for Inter-procedural Verification
• A divide-and-conquer approach for analysing overlaid data structures
• A general framework for types in graph rewriting
• Computer aided verification. 16th international conference, CAV 2004, Boston, MA, USA, July 13--17, 2004. Proceedings.
• Computer Aided Verification
• Toward compositional verification of interruptible OS kernels and device drivers
• Tools and Algorithms for the Construction and Analysis of Systems
• Model Checking Software
• Tools and Algorithms for the Construction and Analysis of Systems
• A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes
• Compositionality Entails Sequentializability
• Symmetry and Completeness in the Analysis of Parameterized Systems
• Verification and falsification of programs with loops using predicate abstraction
• Model checking RAISE applicative specifications
• C-SHORe
• Automatic Termination Verification for Higher-Order Functional Programs
• Refinement of Trace Abstraction
• CONCUR 2004 - Concurrency Theory
• On model checking multiple hybrid views
• Model Checking Procedural Programs
• Predicate Abstraction for Program Verification
• Software Model Checking: Searching for Computations in the Abstract or the Concrete
• Refining abstract interpretations
• Winning Regions of Pushdown Parity Games: A Saturation Method
• Model Checking Multithreaded Programs with Asynchronous Atomic Methods
• Specification and Verification of Multi-Agent Systems
• Monitoring and recovery for web service applications
• Static Analysis
• Proving Termination of Tree Manipulating Programs
• An Automata-Theoretic Approach to Infinite-State Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Programming Languages and Systems
• Title not available (Why is that?)
• Counterexample-guided abstraction refinement for symmetric concurrent programs
• Title not available (Why is that?)
• Correctness kernels of abstract interpretations
• Tools and Algorithms for the Construction and Analysis of Systems
• FM 2005: Formal Methods
• Verification: Theory and Practice
• A unifying view on SMT-based software verification
• Refinement-Based CFG Reconstruction from Unstructured Programs
• Generalized Property Directed Reachability
• Automatically Refining Abstract Interpretations
• Verification, Model Checking, and Abstract Interpretation
• A Lightweight Approach for Loop Summarization
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• Model Checking Higher-Order Programs
• Fluid Updates: Beyond Strong vs. Weak Updates
• Loop Invariants from Counterexamples
• Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
• Efficient strategies for CEGAR-based model checking
• Establishing local temporal heap safety properties with applications to compile-time memory management
• Verify heaps via unified model checking
• Verifying Reference Counting Implementations
• ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
• Splitting via Interpolants
• Programming Languages and Systems
• Automated Inference of Library Specifications for Source-Sink Property Verification
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal Methods for Components and Objects
• Verifying Parallel Algorithms and Programs Using Coloured Petri Nets
• Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation
• Automated formal analysis and verification: an overview
• A semantic framework for the abstract model checking of tccp programs
• Highly dependable concurrent programming using design for verification

This page was built for software: SLAM