The following pages link to Computer Aided Verification (Q5900703):
Displaying 46 items.
- Recent advances in program verification through computer algebra (Q351971) (← links)
- On invariant checking (Q394493) (← links)
- Discovering invariants via simple component analysis (Q435979) (← links)
- SAT modulo linear arithmetic for solving polynomial constraints (Q438576) (← links)
- From invariant checking to invariant inference using randomized search (Q518404) (← links)
- A search-based procedure for nonlinear real arithmetic (Q518407) (← links)
- Reflexive transitive invariant relations: A basis for computing loop functions (Q604384) (← links)
- Modular inference of subprogram contracts for safety checking (Q604392) (← links)
- Constraint solving for interpolation (Q604394) (← links)
- Toward automatic verification of quantum programs (Q667515) (← links)
- Automatic synthesis of \(k\)-inductive piecewise quadratic invariants for switched affine control programs (Q681342) (← links)
- Invariants for time-series constraints (Q823762) (← links)
- Lower-bound synthesis using loop specialization and Max-SMT (Q832313) (← links)
- Deaccumulation techniques for improving provability (Q882487) (← links)
- A quantifier-elimination based heuristic for automatically generating inductive assertions for programs (Q882517) (← links)
- Property-directed incremental invariant generation (Q939166) (← links)
- Mathematics for reasoning about loop functions (Q1044182) (← links)
- A unifying view on SMT-based software verification (Q1703012) (← links)
- Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration (Q2031413) (← links)
- Selectively-amortized resource bounding (Q2145338) (← links)
- A learning-based approach to synthesizing invariants for incomplete verification engines (Q2208307) (← links)
- Template polyhedra and bilinear optimization (Q2322312) (← links)
- Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems (Q2402231) (← links)
- Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods (Q2418665) (← links)
- Constructing invariants for hybrid systems (Q2475635) (← links)
- Static analysis by abstract interpretation: a mathematical programming approach (Q2814107) (← links)
- Speeding up the Constraint-Based Method in Difference Logic (Q2818021) (← links)
- Formal Modelling, Analysis and Verification of Hybrid Systems (Q2948232) (← links)
- Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration (Q2949859) (← links)
- Improving Strategies via SMT Solving (Q3000582) (← links)
- Subsequence Invariants (Q3541017) (← links)
- Inferring Loop Invariants Using Postconditions (Q3586008) (← links)
- Algorithm to find invariant linear inequality constraints in programs (Q3741026) (← links)
- Elimination Techniques for Program Analysis (Q4916078) (← links)
- O-Minimal Invariants for Discrete-Time Dynamical Systems (Q5002799) (← links)
- Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints (Q5039515) (← links)
- Sharper and Simpler Nonlinear Interpolants for Program Verification (Q5056007) (← links)
- Loop invariants (Q5176169) (← links)
- Invariant Synthesis for Combined Theories (Q5452621) (← links)
- Verification, Model Checking, and Abstract Interpretation (Q5711496) (← links)
- Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (Q6487312) (← links)
- Affine Loop Invariant Generation via Matrix Algebra (Q6487319) (← links)
- Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (Q6487320) (← links)
- MDPs as distribution transformers: affine invariant synthesis for safety objectives (Q6535681) (← links)
- \textsc{Sorcar}: property-driven algorithms for learning conjunctive invariants (Q6536295) (← links)
- Invariant relations for affine loops (Q6592111) (← links)
