ARMC
From MaRDI portal
Software:17099
swMATH4949MaRDI QIDQ17099FDOQ17099
Author name not available (Why is that?)
Cited In (24)
- Loop summarization using state and transition invariants
- Non-monotonic Refinement of Control Abstraction for Concurrent Programs
- Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL
- Summarization for termination: No return!
- Quantitative separation logic and programs with lists
- Title not available (Why is that?)
- Abstraction Refinement for Quantified Array Assertions
- Slicing Concurrent Real-Time System Specifications for Verification
- Constraint solving for interpolation
- Ranking Function Synthesis for Bit-Vector Relations
- Software Model Checking by Program Specialization
- Model checking duration calculus: a practical approach
- Loop Summarization and Termination Analysis
- Ranking function synthesis for bit-vector relations
- Proving Termination Through Conditional Termination
- Refining abstract interpretations
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Distributed and Predictable Software Model Checking
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- Shortest Paths in One-Counter Systems
- Specialization with Constrained Generalization for Software Model Checking
- 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