swMATH4949MaRDI QIDQ17099FDOQ17099
Author name not available (Why is that?)
Official website: http://www7.in.tum.de/~rybal/armc/
Cited In (36)
- 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
- QuBE++
- Dagger
- Specialization with constrained generalization for software model checking
- TRACER
- SPEED
- HSF
- SLAB
- SIMP
- CSSV
- Ctrl
- EigenCFA
- Loop Summarization and Termination Analysis
- KITTeL
- IDLVALID
- VeriMAP
- 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
