Cited in
(38)- scientific article; zbMATH DE number 7453193 (Why is no real title available?)
- Loop summarization using state and transition invariants
- Proving correctness of imperative programs by linearizing constrained Horn clauses
- Software model checking by program specialization
- Refining abstract interpretations
- Loop Summarization and Termination Analysis
- Slicing Concurrent Real-Time System Specifications for Verification
- Proving termination through conditional termination
- Ranking function synthesis for bit-vector relations
- Abstraction Refinement for Quantified Array Assertions
- Horn clause verification with convex polyhedral abstraction and tree automata-based refinement
- Automatically proving termination and memory safety for programs with pointer arithmetic
- QuBE++
- Constraint solving for interpolation
- TREX
- ACSAR
- Dagger
- TRACER
- SPEED
- HSF
- SLAB
- SIMP
- CSSV
- Ctrl
- EigenCFA
- KITTeL
- IDLVALID
- VeriMAP
- Distributed and predictable software model checking
- Summarization for termination: No return!
- Non-monotonic refinement of control abstraction for concurrent programs
- Quantitative separation logic and programs with lists
- Automatic verification of combined specifications: an overview
- Using Predicate Abstraction to Generate Heuristic Functions in UPPAAL
- Ranking function synthesis for bit-vector relations
- Specialization with constrained generalization for software model checking
- Automatically Refining Abstract Interpretations
- Model checking duration calculus: a practical approach
This page was built for software: ARMC
