Sciweavers

Share
CADE
2007
Springer

Combining Deduction and Algebraic Constraints for Hybrid System Analysis

11 years 4 months ago
Combining Deduction and Algebraic Constraints for Hybrid System Analysis
We show how theorem proving and methods for handling real algebraic constraints can be combined for hybrid system verification. In particular, we highlight the interaction of deductive and algebraic reasoning that is used for handling the joint discrete and continuous behaviour of hybrid systems. We illustrate proof tasks that occur when verifying scenarios with cooperative traffic agents. From the experience with these examples, we analyse proof strategies for dealing with the practical challenges for integrated algebraic and deductive verification of hybrid systems, and we propose an iterative background closure strategy.
André Platzer
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors André Platzer
Comments (0)
books