Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints
Abstract elided by the publisher.
Related papers
- Automating Induction for Solving Horn Clauses CAV 2017
- Linear Invariant Generation Using Non-linear Constraint Solving CAV 2003
- VeriLHyS: a Framework for LTL Specification and Verification of Hybrid Systems TACAS 2026
- Symbolic bounds analysis of pointers, array indices, and accessed memory regions PLDI 2000
- Symbolic bounds analysis of pointers, array indices, and accessed memory regions TOPLAS 2005
- Model-Checking for Hybrid Systems by Quotienting and Constraints Solving CAV 2000
- Model Checking Gene Regulatory Networks TACAS 2015
- Synthesizing MILP Constraints for Efficient and Robust Optimization PLDI 2023