ARMC
From MaRDI portal
Cited in
(38)- Loop summarization using state and transition invariants
- Summarization for termination: No return!
- Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL
- Quantitative separation logic and programs with lists
- Ranking function synthesis for bit-vector relations
- scientific article; zbMATH DE number 7453193 (Why is no real title available?)
- Abstraction Refinement for Quantified Array Assertions
- Proving termination through conditional termination
- Distributed and predictable software model checking
- Constraint solving for interpolation
- Slicing Concurrent Real-Time System Specifications for Verification
- QuBE++
- TREX
- ACSAR
- Dagger
- TRACER
- SPEED
- HSF
- SLAB
- SIMP
- CSSV
- Ctrl
- EigenCFA
- KITTeL
- IDLVALID
- VeriMAP
- 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
