Verification, Model Checking, and Abstract Interpretation
From MaRDI portal
Recommendations
- Recent advances in program verification through computer algebra
- Validating numerical semidefinite programming solvers for polynomial invariants
- Validating numerical semidefinite programming solvers for polynomial invariants
- Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
- Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
Cited in
(31)- Applications of polyhedral computations to the analysis and verification of hardware and software systems
- Synthesizing ranking functions for loop programs via SVM
- Refutation-based synthesis in SMT
- Template polyhedra and bilinear optimization
- Discovering non-terminating inputs for multi-path polynomial programs
- Witness to non-termination of linear programs
- Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
- Static analysis by abstract interpretation: a mathematical programming approach
- Synthesizing switching controllers for hybrid systems by generating invariants
- Mathematical programming based debugging
- Certificate size reduction in abstraction-carrying code
- Improving strategies via SMT solving
- Recent advances in program verification through computer algebra
- All-Termination(T)
- Generating exact nonlinear ranking functions by symbolic-numeric hybrid method
- On invariant checking
- Global optimization of polynomials restricted to a smooth variety using sums of squares
- Proving termination of nonlinear command sequences
- Efficient solution of a class of quantified constraints with quantifier prefix exists-forall
- scientific article; zbMATH DE number 7559471 (Why is no real title available?)
- Proving properties on PWA systems using copositive and semidefinite programming
- Invariant Synthesis for Combined Theories
- Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
- Validating numerical semidefinite programming solvers for polynomial invariants
- Validating numerical semidefinite programming solvers for polynomial invariants
- Constraint solving for interpolation
- Inductive termination proofs with transition invariants and their relationship to the size-change abstraction
- A new look at the automatic synthesis of linear ranking functions
- A minimalistic look at widening operators
- Generating invariants for non-linear loops by linear algebraic methods
- Property-directed incremental invariant generation
This page was built for publication: Verification, Model Checking, and Abstract Interpretation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5711486)
