The following pages link to SLAM (Q15668):
Displaying 50 items.
- A model checking-based approach for security policy verification of mobile systems (Q432137) (← links)
- Model checking RAISE applicative specifications (Q470000) (← links)
- An extension of lazy abstraction with interpolation for programs with arrays (Q479820) (← links)
- Monitoring and recovery for web service applications (Q488218) (← links)
- A saturation method for the modal \(\mu \)-calculus over pushdown systems (Q532393) (← links)
- Automatic decidability and combinability (Q549666) (← links)
- Context-aware counter abstraction (Q600978) (← links)
- Horn clause verification with convex polyhedral abstraction and tree automata-based refinement (Q681335) (← links)
- Refining abstract interpretations (Q765513) (← links)
- An integrated approach to high integrity software verification (Q861714) (← links)
- Data structures for symbolic multi-valued model-checking (Q862857) (← links)
- On model checking multiple hybrid views (Q947781) (← links)
- Verification and falsification of programs with loops using predicate abstraction (Q968302) (← links)
- Solving games via three-valued abstraction refinement (Q979079) (← links)
- Toward compositional verification of interruptible OS kernels and device drivers (Q1663225) (← links)
- A unifying view on SMT-based software verification (Q1703012) (← links)
- Computer aided verification. 16th international conference, CAV 2004, Boston, MA, USA, July 13--17, 2004. Proceedings. (Q1763061) (← links)
- A local approach for temporal model checking of Java bytecode (Q1776379) (← links)
- Verify heaps via unified model checking (Q1986561) (← links)
- Generating models of infinite-state communication protocols using regular inference with abstraction (Q2018056) (← links)
- Efficient strategies for CEGAR-based model checking (Q2209549) (← links)
- Predicate extension of symbolic memory graphs for the analysis of memory safety correctness (Q2226974) (← links)
- Loop summarization using state and transition invariants (Q2248058) (← links)
- Correctness kernels of abstract interpretations (Q2252528) (← links)
- EUFORIA: complete software model checking with uninterpreted functions (Q2287098) (← links)
- Modular strategies for recursive game graphs (Q2368953) (← links)
- System-level state equality detection for the formal dynamic verification of legacy distributed applications (Q2413022) (← links)
- A divide-and-conquer approach for analysing overlaid data structures (Q2441710) (← links)
- Counterexample-guided abstraction refinement for symmetric concurrent programs (Q2441711) (← links)
- Rule-based static analysis of network protocol implementations (Q2482438) (← links)
- Embedded software verification using symbolic execution and uninterpreted functions (Q2506297) (← links)
- Establishing local temporal heap safety properties with applications to compile-time memory management (Q2568456) (← links)
- A semantic framework for the abstract model checking of tccp programs (Q2576949) (← links)
- A general framework for types in graph rewriting (Q2581012) (← links)
- Predicate diagrams for the verification of real-time systems (Q2642985) (← links)
- Highly dependable concurrent programming using design for verification (Q2643127) (← links)
- Generalized Property Directed Reachability (Q2843329) (← links)
- Stochastic modelling of communication protocols from source code (Q2870288) (← links)
- Automated formal analysis and verification: an overview (Q2871577) (← links)
- Behavioral interface specification languages (Q2875082) (← links)
- Whale: An Interpolation-Based Algorithm for Inter-procedural Verification (Q2891400) (← links)
- Splitting via Interpolants (Q2891411) (← links)
- From Under-Approximations to Over-Approximations and Back (Q2894271) (← links)
- Taking Satisfiability to the Next Level with Z3 (Q2908472) (← links)
- Automated Inference of Library Specifications for Source-Sink Property Verification (Q2937794) (← links)
- An Introduction to Practical Formal Methods Using Temporal Logic (Q2996923) (← links)
- A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes (Q3000614) (← links)
- Compositionality Entails Sequentializability (Q3000634) (← links)
- (Q3021914) (← links)
- An Assume Guarantee Approach for Checking Quantified Array Assertions (Q3067480) (← links)
