A transformational approach for generating nonlinear invariants

DOI10.1007/978-3-540-45099-3_4MaRDI QIDQ2722048zbMATH OpenFDO

Authors Saddek Bensalem, Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Yassine Lakhnech

Publication date 11 July 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-45099-3_4

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Numerical invariants via abstract machines
• Automatic generation of non-linear loop invariants
• Generating invariants for non-linear loops by linear algebraic methods
• Polynomial invariants by linear algebra
• Petri net analysis using invariant generation

Cited in

(8)

• Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems
• Constructing invariants for hybrid systems
• Computing invariants with transformers: experimental scalability and accuracy
• Formal modelling, analysis and verification of hybrid systems
• Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
• Computer Aided Verification
• Analysis of a biphase mark protocol with Uppaal and PVS
• Generating invariants for non-linear loops by linear algebraic methods

This page was built for publication: A transformational approach for generating nonlinear invariants

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2722048)