Integrating Physical Systems in the Static Analysis of Embedded Control Software

Interpretation interpretation is a theory of effective abstraction and/or approximation of discrete mathematical structures as found in the semantics of programming languages, modelling program executions, hence program properties, at various f abstraction [3,7,8,10,12]. nalysis by Abstract Interpretation inent practical application of abstract interpretation has been to static program analysis, that is the automatic (without any human intervention), static (at compile time) determination of dynamic program properties (that always runtime) involving complex abstractions of the infinite state operational semantics (e.g. [4,5,9,11]). Abstract interpretation fights undecidability and complexity by approximation of the program execution model which may lead to false alarms in correctness proofs. This happens whenever the combination of ract domains involved in the analyzer is not precise enough to express any inductive argument necessary in the correctness proof. Hence, among other poss...

• Type: Conference
• Year: 2005
• Where: APLAS
• Authors: Patrick Cousot
• Keywords: Abstract Interpretation, APLAS 2005, Correctness Proof, Static Analyzer