ARMC
From MaRDI portal
Software:17099
swMATH4949MaRDI QIDQ17099FDOQ17099
Author name not available (Why is that?)
Cited In (23)
- Loop summarization using state and transition invariants
- Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL
- Summarization for termination: No return!
- Quantitative separation logic and programs with lists
- Ranking function synthesis for bit-vector relations
- Title not available (Why is that?)
- Abstraction Refinement for Quantified Array Assertions
- Proving termination through conditional termination
- Distributed and predictable software model checking
- Slicing Concurrent Real-Time System Specifications for Verification
- Constraint solving for interpolation
- Non-monotonic refinement of control abstraction for concurrent programs
- Model checking duration calculus: a practical approach
- Specialization with constrained generalization for software model checking
- Loop Summarization and Termination Analysis
- Ranking function synthesis for bit-vector relations
- Refining abstract interpretations
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- Software model checking by program specialization
- Automatically Refining Abstract Interpretations
- Automatic verification of combined specifications: an overview
- Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
This page was built for software: ARMC