A non-linear arithmetic procedure for control-command software verification

DOI10.1007/978-3-319-89963-3_8zbMath1423.68469OpenAlexW2798585073MaRDI QIDQ2324228

Pierre Roux, Sylvain Conchon, Mohamed Iguernlala

Publication date: 16 September 2019

Full work available at URL: https://doi.org/10.1007/978-3-319-89963-3_8

zbMATH Keywords

convex optimizationpolynomial inequalitiesSMTnonlinear real arithmetic

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Convex programming (90C25) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Uses Software

• CSDP
• SDPA
• VSDP
• Why3
• Mosek
• Frama-C
• z3
• Alt-Ergo
• dReal
• CalCS
• Cubicle

This page was built for publication: A non-linear arithmetic procedure for control-command software verification